I'm currently reading through Nelson's "Radically Elementary Probability Theory". I don't believe Nelson gives a construction in that book, but Herzberg makes the claim that the axioms form a subsystem of IST.
Here's the question: how exactly do the axioms of IST imply the axioms used in REPT?
In particular, I'm struggling to prove the sequence principle and external induction. I'm currently working through Nelson's 1977 paper on Internal Set Theory, but it's unclear to me whether the results proved there actually specialize to the axioms in REPT.
Welcome to Math.SE!
I'm not sure how the sequence principle goes and I don't have the means to check it right now, so answering that will have to wait (if somebody else gets here first, don't wait for me, go for it!). But you can prove external induction as follows:
Take a formula $\varphi$ in the language of Internal Set Theory (possibly with non-standard parameters). Assume that $\forall^{s} n. \varphi(n) \rightarrow \varphi(n+1)$ holds. Our goal then is to show that $\varphi(y)$ holds for all standard $y \in \mathbb{N}$.
First, use the axiom of Standardization to construct a set $P=\{x \in \mathbb{N} \mid \varphi(x)\}^{S}$ whose standard elements all satisfy $\varphi(x)$. We know from the axiom that this particular $P$ is a standard set.
Notice that for any standard $x$, we have $\varphi(x) \leftrightarrow x \in P$, and consequently $0 \in P$ and $\forall^{s} x. x \in P \rightarrow x + 1 \in P$ hold. Since $P$ is standard, Transfer applies to the latter and gives $\forall x. x \in P \rightarrow x+1 \in P$. But we know (from ordinary set theory) that there is only one subset of $\mathbb{N}$ which contains $0$ and is closed under successor: $\mathbb{N}$ itself. Consequently, $P = \mathbb{N}$. The desired conclusion, $\forall^{s} y. \varphi(y)$ follows immediately by noting that all numbers belong to $P$, and if $y \in P$ and $y$ is standard, then $y \in P \leftrightarrow \varphi(y)$.