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

Question

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

Answer 1

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