Interpreting PA2 in second-order logic + existence of infinitely many objects

Question

I've heard that if you assume the existence of (Dedekind) infinitely many objects, you can derive -- in second-order logic, given suitable definitions -- the (second-order) Peano axioms for arithmetic. I was wondering how much second-order logic is actually needed for that result, and how exactly the natural numbers are defined in that context. The obvious way would be to start by an application of (countable) Choice, to get representatives for the natural numbers. How much second-order comprehension is then needed subsequently? And is it possible to get this result without Choice? Any advice on relevant literature or a sketch of the proof would be highly appreciated.

Answer 1

First note that monadic second-order logic (i.e. the variant of second-order logic with second-order quantifiers only over unary predicates) isn't sufficient. This is implied by the fact that the monadic theory $\mathsf{MSO}(\mathbb{N},0,S)$ is decidable. Thus further I consider second-order logic with quantifiers $\forall X^n$ and $\exists X^n$ over predicates of arbitrary arity $n$.

Before discussing interpretation of natural numbers, let me discuss the correspondence between second-order logic and positive inductive definitions. Any formula $\varphi(X^1,x)$ defines operator $F_\varphi\colon X^1\longmapsto \{x\mid \varphi(X^1,x\}$. If $X^1$ appears only positively in $\varphi$, then $F_\varphi$ is a monotone operator, i.e. $X^1\subseteq Y^1\Rightarrow F_\varphi(X^1)\subseteq F_\varphi(Y^1)$. In this situation, as usual $F_\varphi$ has the least fixed point $L_\varphi$, i.e. $F_\varphi(L_\varphi)=L_\varphi$ and $\forall X^1(F_\varphi(X^1)\subseteq X^1\to L_\varphi\subseteq X^1)$. In fact we will be interested only in the case when $\varphi$ is a first-order formula. And in order to construct $L_\varphi$ for first-order $\varphi$ in second-order logic, it is enough to use $\Pi^1_1$-comprehension (here $\Pi^1_1$ formulas are formulas that start with a universal second-order prenex followed by a first-order formula).

Naturally this is generalized to joint positive inductive definitions of several predicates of arbitrary arities. Namely formulas $\varphi_1(X^{k_1}_1,\ldots,X^{k_n}_n,x_1,\ldots,x_{k_1})$, $\ldots$, $\varphi_n(X^{k_1}_1,\ldots,X^{k_n}_n,x_1,\ldots,x_{k_n})$ determine monotone operator $$F_{\vec{\varphi}}\colon \langle X^{k_1}_1,\ldots,X^{k_n}_n\rangle\longmapsto \langle \{\langle x_1,\ldots,x_{k_1}\rangle \mid \varphi_1( X^{k_1}_1,\ldots,X^{k_n}_n,x_1,\ldots,x_{k_1})\},\ldots\rangle.$$ And for it we have the least fixed point $L_{\vec{\varphi}}=\langle L_{\vec{\varphi},1},\ldots,L_{\vec{\varphi},n}\rangle$. Again, for first-order $\varphi_i$'s $L_{\vec{\varphi}}$ could be constructed using $\Pi^1_1$-comprehension.

In order to simplify consideration, I will formalize Dedekind infiniteness by a first-order sentence $\mathsf{DInf}$ $$\forall x,y\;(f(x)\ne f(y))\land \exists x\forall y\;(f(y)\ne x)$$ in the signature with one unary symbol. Note that we could have considered second-order axiom stating the existence of function $f$ with the desired properties (or binary predicate giving graph of $f$).

Consider the following interpretation of first-order arithmetic with defined equality (i.e. individual natural numbers will be interpreted by equivalence classes of individual objects in second-order logic). The idea is to represent $0$ by the equivalence class $U_0=\{x\mid \forall y\; (x\ne f(y))\}$, and represent $n+1$ by the equivalence class $U_{n+1}=\{x\mid \forall y\in U_{n}\;(x\ne f(y))\}$. Formally our interpretation will consist of second-order formulas $(x=y)^*$, $(S(x)=y)^*$, $(x+y=z)^*$, $(xy=z)^*$ (the domain of interpretation is $\{x\mid (x=x)^*\}$). It is possible to define all this predicates by a joint positive inductive definition. It will be fairly long to give explicitly. The idea is to make the corresponding monotone operator to update partially defined equality and arithmetical operations, that are thought as covering only numbers up to $n$, to cover numbers up to $n+1$.

It is easy to see that $\Pi^1_1\mbox{-}\mathsf{CA}+\mathsf{DInf}$ could construct this interpretation and in fact prove any instance of the scheme of first-order induction for it, giving an interpretation of first-order arithmetic $\mathsf{PA}$. But in fact here we got more than just first-order Peano arithmetic, we interpret second-order arithmetic with $\Pi^1_1$-comprehension. More close examination of the argument shows that this interpretation will give first-order Peano arithmetic even in $\Pi^0_\infty\mbox{-}\mathsf{CA}+\Pi^1_1\mbox{-}\mathsf{CA}^{\mathsf{pf}}+\mathsf{DInf}$ (here $\Pi^1_1\mbox{-}\mathsf{CA}^{\mathsf{pf}}$ is parameter-free $\Pi^1_1$-comprehension scheme and $\Pi^0_\infty\mbox{-}\mathsf{CA}$ is the scheme of comprehension for first-order formulas with second-order parameters). My conjecture is that this should be best optimal in the sense that $\Pi^0_\infty\mbox{-}\mathsf{CA}+\Pi^1_1\mbox{-}\mathsf{CA}^{\mathsf{pf}}+\mathsf{DInf}$ proves precisely the same sentences of first-order arithmetic as $\mathsf{PA}$ and that the two theories are equiconsistent over $\mathsf{PRA}$.