Peano axioms and first-order logic with $\exists^{\infty}$

Question

All Peano axioms except the induction axiom are statements in first-order logic. The induction axiom is written as $\forall X(0 \in X \land \forall n(n \in \mathbb{N} \rightarrow (n \in X \land n' \in X)) \rightarrow \mathbb{N} \subseteq X$, where $n'$ is the successor of $n$.

Now I want to look at an extension of first-order logic. I also allow $\exists^{\infty}$ [exists infinity many]. My notes states that the induction axiom can be rewritten only using this extension of first-order logic.

My question is: How?

Since I look at first-order logic I am not allowed to have a set $X$. Here I am allready stuck, because I think I can not just say $\exists{^\infty} x$ to have something like a set ... I think the solution requires two steps: First get rid of the set and then use $\exists^{\infty}$ to make it well-defined in my case.

Answer 1

Note that induction is equivalent to well-ordering (more generally to well-foundedness). Namely, removing the induction axiom, a model of $\sf PA$ is well-ordered if and only if it satisfies the (second-order) induction axiom.

But well-ordering is equivalent to "there is no infinite decreasing chain". Finally, since in $\sf PA$ every non-zero element has a predecessor, this means that well-ordering is equivalent to stating that no element has infinitely many elements smaller than itself.

And this should be fairly straightforward to state using $\exists^\infty$.