In this question, and specifically in this answer, it is explained that $\mathbb{N}$ is not definable in $\mathbb{R}$ using the language of ordered fields (using $0$, $1$, $+$, $\cdot$, $<$) with a first-order formula. In the answer there are some words about second-order logic, but they're very brief.
So I'm wondering:
- Is it possible to use a second-order formula to define $\mathbb{N}$? What would it look like?
- Is it possible to add an axiom schema in first-order logic (adding, effectively, infinite many axioms) to define $\mathbb{N}$? What would it look like?
(I'm interested in both questions)
The same answer shows that a second-order formula like $$\forall \phi \big[\phi(0)\land\forall x\big(\phi(x)\rightarrow\phi(x+1)\big)\big]$$ defines an inductive set (although the formula there uses set notation), but I don't know if it's enough since it's still necessary to show that there is a "minimum inductive set", isn't?
$\mathbb N$ is the set of all $y\in\mathbb R$ such that $$ \forall\phi\,\big([\phi(0)\land\forall x\,(\phi(x)\to\phi(x+1))]\to\phi(y)\big); $$ in other words, every inductive set contains $y$.