You can quote me on this if you like.
This is such an old issue that I am surprised it is still up for discussion. I know you like ultra ultra-powers, etc, but I have always thought they were wrong-headed; it was LuxembourgLuxemburg who made them popular for NSA originally.
The point is that you actually really NEED the transfer theorems; so you essentially need the the logical apparatus; in most cases the compactness theorem and some form of saturation. Occasionally a type omitting argument could be used but that is rare.
The reason is that you are postulating that "all of mathematics" carries over to the non-standard model and in fact, that is the underlying intuition in the applications.
I also think that the "more concreteness" of the ultraproduct construction is just an illusion. You can not answer if the integer produced by (1,2,3,4,5, ...) is even or odd since it depends on the ultrafilter completion of e.g. any non-principleprincipal filter.
Moreover, the basic tools in almost all the proofs is dealing with the seam between "standard" and "non-standard" elements; which really depends on a feel for expressibility in the language being used. Nelson's approach was to try to help people manage without the "feel". That's a matter of taste.
Furthermore, I would differ with your point that NSA is to formalize classical mathematicians arguments. That is "cool" and Robinson greatly enjoyed it, but really he also was sure that it is a great way to prove new theorems. Since people sort of like to hear about the theorems consequence in "classical" settings; then one often had to find equivalence theorems (this was clear in the work on brownian motion etc) and in my work on inverse limits of finite groups (by the uniqueness of inverse limits, the non-standard finite groups are essentially equivalent to inverse limits of systems of finite groups and a lot of the very early work of LubotskyLubotzky on profinite groups can be easily carried out in this setting) but actually a more extreme position can be seen when you just take the position that the "standard" results are just one specific implementation and one could develop mathematics happily without them. The argument that the non-standard models are not "unique" is just a habit and not important.
Robinson himself put this viewpoint forward very nicely in his Brouwer medelmedal address "Standard and NonStandard Number Systems"
Best regards Larry Manevitz [email protected]
Regarding the use of limit ultrapowers etc; one needs to be careful there. I once proved there was no measureable cardinal by taking such a large ultrapower; but actually all the standard sets dont grow in that context :).