[FOM] links between nonstandard analysis and formal logic and set theory

[Ben Crowell]

I've been trying to learn about nonstandard analysis, and
one thing that's bugging me is the relationship between the notion of an
internal set in nonstandard analysis and internal set theory in general.
In the ultrapower approach, basically internal sets are those that are
ultrapowers of real sets. (There's also an allowance made for constructing
internal sets like {x | |x|<epsilon}, where epsilon is an infinitesimal.)
What's not clear to me is how this relates to the internal sets of IST.
I'd be grateful for any explanations, or pointers to what to read in order
to understand these connections between  nonstandard analysis and formal
logic and set theory. I've read Keisler's Elementary Calculus, and
ch. I-III of Robinson's Non-Standard Analysis.

I'm also interested in trying to absorb the paper by Kanovei
and Shelah, "A definable nonstandard model of the reals,"
http://shelah.logic.at/files/825.pdf , but it seems like I need to bone
up on my formal logic and set theory, since there are a lot of terms
on the first page of the paper that I don't know. Can anyone recommend
a good book that a nonspecialist could read for background?

Finally, I'd be interested in what people on this list think of Robinson's
claim that ZFC might not be "the appropriate underlying set theory for the
hyperreal number system. Set theory might have taken a different direction
if it had been developed with the hyperreal line in mind. What is needed
is an underlying set theory which proves the unique existence of the
hyperreal number system."