In Davis' Applied nonstandard analysis a proof of the following, often seen, proposition is presented:
For a sequence $S_n$
$S_n \rightarrow L$ iff $S_n \approxeq L$ for all infinite n.
He then states that 'let us choose some $\epsilon \in R^+$, corresponding to this there exist some $n_0$' and then he gives the following formula for defining the limit in the usual way: $(\forall n\in N)(n>N\implies |s_n - L|<\epsilon)$.
He then say that using the transfer theorem one gets that for any $n\in *N$ for which we have $n>n_0$ we have that $|s_n - L|<\epsilon$.
Then he says that since $n_0$ is finite this inequality holds forall infinite *N. And tells us to note that epsilon was any real positive number so we can conclude $S_n \approxeq L$ for any integer $n$.
Going the other way he tells us to let $S_n \approxeq L$ and again choose $\epsilon \in R^+$ then proceeds to reconstruct the classical definition written in $*R$.
My question is why in applying the transfer theorem hasn't $\epsilon$ become an element of $*R^+$ and similairly why is $n_0$ finite? Surely after the application of the transfer theorem one has $n_0$ as an element of *N so there is no reason to assume it's finite.
I just can't see why the reasoning isn't revolving around manipulating the elements of *R, and why standard elements like $\epsilon$ have escaped being transferred.
Furthermore I note when he goes the other way he constructs the statement $(\exists n_0\in *N)(\forall n\in N)(n>N\implies |s_n - L|<\epsilon)$ so the $(\exists n_0\in *N)$ term has now appeared this time as an element of the hypernaturals but the reference to $\epsilon \in R^+$ remains.
I have found I've similar issues in other proofs so I suspect I have misunderstood some crucial point. Any help would be greatly appreciated.
Your confusion is one that lots of people have when they first deal with "formulas with parameters". I wouldn't say you necessarily misunderstood any crucial point: nonstandard analysis requires some logical sophistication, and I suspect that your textbook does not put adequate emphasis on crucial points related to logic.
Imagine that you want to infer $\forall x \in \!\!~^\star\mathbb{R}. |x| > -5$ from $\forall x \in \mathbb{R}. |x| > -5$ via the Transfer principle. This happens to be a valid inference. You can think about the situation in two different ways:
What I call the big language perspective: your language already contains a predicate with one free variable $\phi(y)$ which means $|y| > -5$. In this case you can just use the following Transfer principle: $$(\forall x \in \mathbb{R}. \phi(x)) \rightarrow (\forall x \in \!\!~^\star\mathbb{R}. \phi(x)).$$
What I call the quantified parameters perspective: you assert a Transfer principle of the form $$\forall k \in \mathbb{R}. (\forall x \in \mathbb{R}. |x| > k) \rightarrow (\forall y \in \!\!~^\star\mathbb{R}. |y| > k)$$ where you call $k$ a standard parameter. Since $k$ is universally quantified, this remains valid if you set $k = -5$. All Transfer principles with standard parameters are indeed provable.
When people do mathematics fully formally* (e.g. formalized in ZFC Set Theory), the latter perspective is much more useful: as a matter of fact, one would normally avoid having term languages and parameters altogether, and do every formal manipulation using variables and quantifiers only.
When people do mathematics informally, they prefer to think in terms of parameters: we would say that the expression $|x| > -5$ has $-5$ as a standard parameter, and Transfer is valid in the presence of standard parameters, so wecan conclude $\forall x \in \!\!~^\star\mathbb{R}. |x| > -5$ from $\forall x \in \mathbb{R}. |x| > -5$.
With this in mind, here's how the first part of that proof should go:
Assume that $s_n \rightarrow L$ according to the conventional $\varepsilon$-$\delta$ definition of limit. Pick any $\varepsilon \in \mathbb{R}$ satisfying $\varepsilon > 0$. According to the conventional definition, we can find some $n_0 \in \mathbb{N}$ such that the following holds: $\forall n \in \mathbb{N}. n > n_0 \rightarrow |L - S_n| < \varepsilon$. Now, we shall take $L,n_0,S$ and $\varepsilon$ as standard parameters of this formula. We have to check that they are standard: this follows because they are all either real numbers or sequences of real numbers. Applying Transfer with these parameters, we infer $\forall n \in \!\!~^\star\mathbb{N}. n > n_0 \rightarrow |L - S_n| < \varepsilon$.
Was this a valid inference? We can see that it was, using the quantified parameters viewpoint: we can think of it as an application of the Transfer principle $$\forall K: \mathbb{N} \rightarrow \mathbb{R}. \forall k_1 \in \mathbb{R}. \forall k_2 \in \mathbb{R}. \forall k_3 \in \mathbb{R}. \\ (\forall n \in \mathbb{N}. n > k_1 \rightarrow |k_2 - K_n| < k_3) \rightarrow (\forall n \in \!\!~^\star\mathbb{N}. n > k_1 \rightarrow |k_2 - K_n| < k_3)$$ after we substituted the number $\varepsilon \in \mathbb{R}$ for $k_3$, the sequence $S: \mathbb{N} \rightarrow \mathbb{R}$ for $K$ and so on.