The syntax of nonstandard analysis (Q1101109)

The author continuous in this paper his influential study, started with the paper ``Internal set theory: a new approach to nonstandard analysis'' [Bull. Am. Math. Soc. 83, 1165-1198 (1977; Zbl 0373.02040)], of formalizations of principles of nonstandard analysis. While the aim of the first paper was to construct a formal system, Internal Set Theory (IST), which codified a large part of existing mathematical practice of n.a., in the present paper the author shows that ``... the proofs in IST may be regarded as abbreviations of proofs within conventional mathematics...''. In this purely syntactical approach, the author follows one of A. Robinson's original approaches which is characteristic by emphasizing new deductive procedures rather than new entities. The core of the paper is a reduction procedure for formulas and proofs of a theory \({\mathcal A}\) * \((=IST\) on a language enriched by the language of a model of a first order theory \({\mathcal A})\) into formulas and proofs of a theory \(\tilde {\mathcal A}\) \((=adequately\) enriched ZFC). This reduction procedure gives a solution to a problem posed by \textit{A. Robinson} [J. Symb. Logic 38, 500-516 (1973; Zbl 0289.02002), problem No.11] which consisted of finding ``... a purely syntactical transformation which correlates standard and nonstandard proofs of the same theorems in a large area...''.