Internal set theory: proof that limited integers are standard I'm following this pdf from Edward Nelson about internal set theory: https://web.math.princeton.edu/~nelson/books/1.pdf 
I'm at page 6. Only two axiom schemes have been introduced so far.
The transfer principle (writing here the dual version using existential quantifiers):
\begin{equation}
\forall^{st}{t_1}...\forall^{st}{t_n} [ \exists{x} A \leftrightarrow \exists^{st}{x} A ]
\end{equation}
where $A$ must be an internal formula with no other free variables than $x, t_1, ..., t_n$
And the idealization principle:
\begin{equation}
\forall^{stfin}{x'}\exists{y}\forall{x}A \leftrightarrow \exists{y}\forall^{st}{x}A
\end{equation}
where $A$ must be an internal formula.
The definition of a limited real number is: any real number whose absolute value is inferior or equal to a standard real.
The theorem 1 on page 6 is the following:
There does not exist $S_1$, $S_2$, $S_3$, $S_4$, or $S_5$ such that, for all $n$ in $\mathbb{N}$ and $x$ in $\mathbb{R}$, we have $n \in S_1 \leftrightarrow$ n is standard, $n \in S_2 \leftrightarrow n$ is nonstandard, $x \in S_3 \leftrightarrow x$ is limited, $x \in S_4 \leftrightarrow x$ is unlimited, or $x \in S_5 \leftrightarrow x$ is infinitesimal
I have no problem proving the parts about $S_1$ and $S_2$. However the part about $S_3$ seems less obvious. In the pdf, Nelson writes this as a proof: if $S_3$ existed we could take $S_1 = \mathbb{N} \cap S_3$. It seems to me that to make this reasoning work, you need to prove that an integer is standard if and only if it is limited. Hence my question: how do you prove that if an integer is limited, then it is standard, using only the transfer principle and the idealization principle?
 A: $x$ unlimited by definition means it is greater in magnitude than all standard integers, so if $x$ is unlimited it is necessarily nonstandard. This proves that if $x$ is standard then $x$ is limited.
Suppose $x$ is limited, then by definition there exists a standard $y>0$ s.t. $\lvert x\rvert\leq y$. By Dual transfer the finite integer interval $[-y,y]$ is standard (it's a classical formula with fixed standard parameters $y$). The interval is standard and finite so it contains only standard elements.
n.b. this last point is probably introduced in your book sometime around this point as a basic IST concept, but you don't need standardization to prove it. Comment if you need help outlining a proof of it.
A: I offer two proofs that work over the natural numbers (as opposed to the integers) and show that if a natural number is limited then it is standard. They both avoid appeals to Theorem 2 (although you can prove Theorem 2 independently of Theorem 1), and the first one uses only Idealization and Transfer.
I. The first one is a variant of GPhys' proof. If a natural number $m$ is limited, then by definition $m < x$ for some standard $x \in \mathbb{R}$. By applying Transfer to $\forall x \in \mathbb{R}. \exists y \in \mathbb{N}. y = \left\lceil x \right\rceil$ we get that the ceiling of $x$ is a standard natural number, and we have $m < x \leq \left\lceil x \right\rceil$ . In what follows let $n$ denote $\left\lceil x \right\rceil$.
It's clear that there exists a finite set $\mathcal{F}$ such that $\forall y < n. \exists x \in \mathcal{F}. x = y$, namely $\mathcal{F} = \{ x \in \mathbb{N} \:|\: x < n \}$. But then by (the logical dual of) Idealization, we get that $\forall y < n. \exists^{st} x. x = y$. This is equivalent to $\forall y < n. \mathrm{st}(y)$. Since $m < n$, it follows that $m$ is standard.
II. Jumping ahead a little, you can prove this using external induction (Section 1.4, Exercise 4) on the formula $\forall m. m \leq n \rightarrow \mathrm{st}(m)$ as well. This variant proof occasionally comes in handy in constructive and type-theoretic analogues of Internal Set Theory.
The base case is $\forall m. m \leq 0 \rightarrow \mathrm{st}(m)$, which is true since $\mathrm{st}(0)$.
The inductive case allows us to assume that all $m \leq k$ are standard, and requires us to prove that all $n \leq k+1$ are standard. This amounts to proving that if $k$ is standard, then so is $k+1$. This is immediate by Transfer applied to $\forall x. \exists y. y = x+1$.
By the principle of external induction we get that for all standard $n \in \mathbb{N}$, it is the case that $\forall m. m \leq n \rightarrow \mathrm{st}(m)$. Setting $n=\left\lceil x \right\rceil$, we have that $m<n$ and so we can conclude that $m$ standard.
Keep in mind that external induction requires Standardization and Transfer (but not Idealization), so this second solution is definitely not the intended solution.
Dual idealization. Idealization says that if $\varphi$ is internal, we have the equivalence $$\forall^{st fin} \mathcal{F}. \exists y. \forall x \in \mathcal{F}. \varphi \:\leftrightarrow\: \exists y. \forall^{st} x. \varphi.$$
But if $A \leftrightarrow B$ then $\neg A \leftrightarrow \neg B$, so we also have
$$\exists^{st fin} \mathcal{F}. \forall y. \exists x \in \mathcal{F}. \psi \:\leftrightarrow\: \forall y. \exists^{st} x. \psi$$
where $\psi$ is equivalent to $\neg \varphi$.
