# "$\Sigma_1^1$-Peano arithmetic" - does it pin down $\mathbb{N}$?

Let $$\mathsf{PA}_{\Sigma^1_1}$$ be the theory in second-order logic gotten by extending the usual first-order Peano axioms to include arbitrary $$\Sigma^1_1$$ formulas in the induction scheme. My question is:

Does $$\mathsf{PA}_{\Sigma^1_1}$$ have any nonstandard models?

Note that a model of $$\mathsf{PA}_{\Sigma^1_1}$$ is exactly a model of $$\mathsf{PA}$$ with no (nontrivial proper) $$\Sigma^1_1$$-definable cuts.

If we replace $$\Sigma^1_1$$ with $$\Pi^1_1$$ the answer is immediately negative, since the set of standard elements of a model of $$\mathsf{PA}$$ is $$\Pi^1_1$$. However, nothing similar seems to work for $$\Sigma^1_1$$ (although I could easily be missing something obvious).

One quick observation is that $$\mathsf{PA}_{\Sigma^1_1}$$ does entail true first-order arithmetic. Given a first-order formula $$\varphi(x)$$, let $$\hat{\varphi}(x)$$ be the $$\Sigma^1_1$$ formula "There is a cut containing $$x$$ such that every element of the cut satisfies $$\varphi$$." If $$M\models\mathsf{PA}_{\Sigma^1_1}$$ we trivially have $$\hat{\varphi}^M\in\{\emptyset,M\}$$; by induction on the complexity of $$\varphi$$ we can show that if every standard natural number satisfies $$\varphi$$ then $$0\in\hat{\varphi}^M$$ and consequently $$M\models\forall x\varphi(x)$$ (which then gives $$M\equiv\mathbb{N}$$). However, I don't see how to use this to get categoricity. In fact, as far as I know it's possible that e.g. every nontrivial ultrapower of $$\mathbb{N}$$ satisfies $$\mathsf{PA}_{\Sigma^1_1}$$. (Note that $$\Sigma^1_1$$ sentences are preserved under taking ultrapowers; however, an instance of induction for a $$\Sigma^1_1$$ formula is $$\Sigma^1_1\vee\Pi^1_1$$ and $$\Pi^1_1$$ sentences are not preserved under taking ultrapowers, so this doesn't seem to help.)

If you allow your $$\Sigma^1_1$$ formulas to have parameters, then PA$$_{\Sigma^1_1}$$ has only the standard model. To prove it, use the $$\Pi^1_1$$ definition of standardness to produce a $$\Sigma^1_1$$ formula $$\sigma(x,y)$$ saying that $$x and $$y-x$$ is not standard, i.e., $$x$$ is infinitely far below $$y$$. It's easy to show that $$\sigma(x,y)$$ implies $$\sigma(x+1,y)$$. So, by $$\Sigma^1_1$$ induction, if $$\sigma(0,y)$$ then $$\forall x\,\sigma(x,y)$$ and, in particular, $$\sigma(y,y)$$, which is absurd. So $$\neg\sigma(0,y)$$. But that means $$y$$ is standard.