Are the natural numbers definable in the (2nd-order) theory of complete ordered fields?

Question

I read that the natural numbers are not definable in the theory of real closed fields (RCF), which captures the 1st-order properties of the real numbers. That's why decidability of RCF doesn't contradict Gödel's theorem.

But are the natural numbers definable in the 2nd-order theory of complete ordered fields (COF), which categorically captures the real numbers?

Edit : Looks like the answer was simple, after some thinking. Since COF is a 2nd-order theory, we can quantify over subsets of $\mathbb R$. Then expressing that $\mathbb N$ is the smallest inductive subset of $\mathbb R$ should do.

Essentially, for a subset $S\subseteq\mathbb R$, define the (meta-)property $I(S)$ of being inductive : $$I(S) := (0\in S \wedge (\forall x\in\mathbb R : x\in S\rightarrow x+1\in S))$$ Define the (meta-)property $N(S)$ of being the smallest inductive set : $$N(S) := (I(S) \wedge (\forall T\subseteq\mathbb R : I(T)\rightarrow S\subseteq T))$$ Then $\mathbb N$ is the unique subset $S$ of $\mathbb R$ such that $N(S)$.

I hope there is no mistake.

Answer 1

This was answered in the comments; I'm posting an answer here to move this off the unanswered queue. I've made this CW to avoid reputation gain, and if one of the original commenters posts an answer of their own I'll delete this one.

In second-order logic (with the standard semantics) we can define $\mathbb{N}$ in the ordered field $(\mathbb{R};+,\times,0,1,<)$ as the smallest inductive set: $n$ is a natural number iff $n$ is in every inductive set.

Note that this is a "universal-second-order" characterization. It's natural to ask whether this is necessary:

Is there a formula of the form $\exists X\theta(x,X)$ with $\theta$ involving only first-order quantifiers such that $\{r: \mathbb{R}\models\exists X\theta(r,X)\}=\mathbb{N}$?

In many ways existential second-order logic is tamer than its universal counterpart (e.g. only the former satisfies an appropriate compactness property), so it's plausible that the answer is negative. However, the answer is in fact positive:

$n$ is a natural number iff there is some set $X$ containing only nonnegative reals such that $0\in X$, $m\in X\implies m+1\in X$, and $m\in X$ and $0<\epsilon<1$ implies $m+\epsilon\not\in X$.