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

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.

• It's kinda weird talking about Peano and first-order while quantifying over subsets (second-order) and referring to $\Bbb N$ in the formula. Mar 18, 2019 at 11:15
• @AsafKaragila Well he did say all the axioms "expect" the induction axiom - if you assume "expect" was a typo for "except" it makes sense.... Mar 18, 2019 at 14:45

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$$.