Finite sets and infinite sets in weak intuitionistic arithmetic

Takako Nemoto, JAIST. Part of the logic seminar series.

Takako Nemoto, JAIST

We consider, for a set A of natural numbers, the following notions of finiteness:

FIN1: There are k and m_0,...,m_{k-1} such that A = {m_0,...,m_{k-1}};
FIN2: There is an upper bound for A;
FIN3: There is an m such that |B| < m for all subsets B of A;
FIN4: It is not the case that, for all x, there is y > x such that y is in A;
 FIN5: It is not the case that, for all m, there is a subset B of A such that |B| = m,

and infiniteness

INF1: There are no k and m_0,...,m_{k-1} such that A = {m_0,...,m_{k-1}};
INF2: There is no upper bound for A;
INF3: There is no m such that |B| < m for all subsets B of A;
INF4: For all x, there is a y > x such that y is in A;
INF5: For all m, there is a subset B of A such that |B| = m.

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 called bounded comprehension.