Finite sets and infinite sets in weak intuitionistic arithmetic

In this paper, we consider, for a setAof natural numbers, the following notions of finiteness There are a natural number and a bijection between and ; lfThere is an upper bound for ; There is such that ; lIt is not the case that ; It is not the case that , and infiniteness There are not a natural number and a bijection between and ; lfThere is no upper bound for ; There is no such that ; l; . In this paper, we systematically compare them in the method of constructive reverse mathematics. We show that the equivalence among them can be characterized by various combinations of induction axioms and non-constructive principles, including the axiom of bounded comprehension.