A metatheory of nonstandard analysis (Q1316505)

In a previous work [Lect. Notes Math. 1388, 203-220 (1989; Zbl 0691.03050)] of the first author, we set up a formal system \(IR\) of infinitary logic, by whose proof-theoretical properties the infinitesimal calculus can be justified. Such an attempt was started due to the first author's wish to single out the essence of the metatheory of nonstandard mathematics as a ``trick of the language'', and was concluded with the ``linkage principles'' which support the nonstandard theory. We have since pushed that thought forward and extended the result to general nonstandard analysis, with the theory of Loeb measure in mind.