(The original text has been edited to render it in pure HTML; thus
\mathbb font is replaced by large bold and membership is either written in
text or denoted by \in. The original can be seen in the ps version)
In the aftermath of the discoveries in foundations of mathematics there
was surprisingly little effect on mathematics as a whole. If one looks at
standard textbooks in different mathematical disciplines, especially those
closer to what is referred to as applied mathematics, there is little trace
of those developments outside of mathematical logic and model theory. But
it seems fair to say that there is a widespread conviction that the principles
embodied in the Zermelo - Fraenkel theory with Choice (ZFC) are
a correct description of the set theoretic underpinnings of mathematics.
In most textbooks of the kind referred to above, there is, of course, no discussion of these matters, and set theory is assumed informally, although more advanced principles like Choice or sometimes Replacement are often mentioned explicitly. This implicitly fixes a point of view of the mathematical universe which is at odds with the results in foundations. For example most mathematicians still take it for granted that the real number system is uniquely determined up to isomorphism, which is a correct point of view as long as one does not accept to look at ``unnatural'' interpretations of the membership relation.
One of the crucial discoveries in foundations was that the structures studied in mathematics do have nonstandard models. Starting with A.Robinson, this gave rise to a new mathematical discipline, nonstandard analysis, which has made important contributions to different branches of pure mathematics. The earliest practice of nonstandard analysis, concentrated on a variety of different nonstandard extensions of ``standard'' mathematical structures, was codified by Robinson and Zakon in the late 60s. They suggested 1 a system, of type-theoretic character, which reduced methods of nonstandard analysis to a few principles, which, once established, allow to develop nonstandard analysis without paying much attention to details related to the construction of nonstandard extensions. The key concept of this direction of foundations of nonstandard analysis 2 , which we shall call ``model-theoretic foundations'', is that of a nonstandard superstructure, or nonstandard universe, actually, a type-theoretic superstructure over a nonstandard extension of a chosen mathematical structure.
Despite its great success in applications since the early 70s, the model-theoretic approach has, from a philosophical point of view, the disadvantage that set theory becomes in some sense dissociated from mathematical practice. It becomes the substrate for the construction of a variety of non-isomorphic ``nonstandard'' models related to various fields of mathematics. This leads naturally to the idea to modify the axiomatic system for set theory in such a way that it restores the essential uniqueness of fundamental mathematical structures. For instance, Keisler wrote in his survey 3 that the unique existence of the pair consisting of the real and hyperreal number systems should be ensured by the underlying set theory. Such a system can be intended for two distinct purposes. It may be conceived either as a subject of foundational studies, which is a legitimate purpose in itself, or as a tool for the ``working mathematician'' which would be used in much the same way as ZFC is used.
Given the remarkable unity of mathematics, such a system should be equivalent to ZFC in a metamathematical sense. Usually this is understood as the requirement that the theory should possess, within the ``universe of discourse'' of all sets, a class -- let us denote it by S and call the standard universe -- informally seen as a copy of the ``real universe of sets'' described by ZFC, and that the theory should prove those and only those theorems about S which ZFC proves about all sets. In this sense, the theory may be viewed as equivalent to ZFC.
Notice that the latter requirement, called conservativity, only ensures that ``provable'' truths are reproduced. But we would like to relate all true sentences of the non-standard theory to the truth in ZFC. This is a stronger requirement; indeed, a conservative nonstandard extension of ZFC, although it proves nothing about S beyond the theorems of ZFC, may well shut some ``windows'' which are implicitly open in ZFC. This could be dealt with by stipulating that the extended theory be interpretable in the ZFC universe in such a way that the class S in the sense of interpretation is isomorphic to the ground ZFC universe. Such an interpretation may be thought of as an extension of the ground ZFC universe to the ``universe of discourse'' of the theory. (This extension is rather an embedding of the ZFC universe V into a definable class-size structure in V, which is a model of the extended theory.) We call ``realistic'' 4 theories which admit such an interpretation in ZFC. This is a reasonable demarcation line between non-standard theories which respect mathematical reality as described by ZFC from purely syntactical deduction schemes, be the latter even conservative.
Although speculations in this direction of modifying the axiomatic set-up itself can be traced to the late 60s 5 , it was only in mid-70s when Hrbacek and Nelson 6 independently proposed satisfactory nonstandard set theories of this kind 7, of which Nelson's internal set theory IST gained a lot of support among practitioners of nonstandard methods.
The universe of IST is arranged in a remarkably simple way. It includes a class S called the universe of all standard sets, distinguished by the standardness predicate st, an atomic predicate. S is postulated to fulfill the axioms of ZFC while the ``universe of discourse'' is postulated, by a special axiom scheme called Transfer, to be an elementary extension of S in the membership language. Additional axioms of Standardization and Idealization provide some regularity for the interactions between standard and nonstandard sets, as well as the existence of truly ``nonstandard'' objects like infinitesimals.
The price one has to pay for this nice image is very high indeed. The predicate st, being independent from the membership relation, does not always form sets in IST. For instance the collection of all standard natural numbers is not a set in IST. Thus certain things which were done in model theory and its nonstandard analysis branch cannot be reproduced in IST, at least not directly. But as Keisler noted ``... mathematics in IST looks more like traditional mathematics ...'' (see Footnote 3). This was probably the reason that quite a number of mathematicians outside of logic and foundations took up this approach.
Hrbacek proposed 8 several theories which incorporate more of the set theoretic instrumentarium one is accustomed to from the model-theoretic development of nonstandard analysis. In these systems the predicate st can participate in definitions of sets, subsequently, in addition to the standard universe S and the internal universe I(quite similar to the set universe of IST) there is now a larger underlying universe H of ``external sets'', including in particular standard and internal sets, sets like the collection of all standard natural numbers, and many more. Unlike the situation in IST, I consists of all sets which are elements of standard sets. This means that the standard universe exerts a tighter control over internal sets than is possible in IST. As axioms there are again the ZFC axioms in S, Transfer between the standard and internal universes, an axiom which says that I is a transitive class in H. In addition, H is postulated to be well-founded over I 9 and to satisfy quite a big fragment of ZFC including Replacement for all formulas (even those in which the predicate st occurs). Saturation for families (of internal sets) of standard size 10 is included: as usual, it is a general source of getting various internal nonstandard objects like infinitesimal or infinitely large numbers.
Later Kawaï 11 extended IST to a theory similar to those introduced by Hrbacek, and very well equipped technically.
Hrbacek, Nelson, and Kawaï showed that their theories are equiconsistent and conservative extensions of ZFC. Thus as far as proving theorems is concerned, they would be admissible as a tool replacing ZFC. But, as one of the authors 12 has shown, IST transcends ZFC in another sense. For instance, IST does not admit an interpretation in ZFC of the kind discussed above, moreover, not every model of ZFC can be embedded, as the class of all standard sets, in a model of IST. Furthermore there exists a sentence in the st-\in-language which is not equivalent in IST to an \in-sentence. Thus, IST ``knows'' something about the standard universe which ZFC itself does not ``know'' about sets. (This ``something'' is not a first-order property, of course.) We can conclude that IST and Kawaï's theories considered as a working tool represent a definite step away from ZFC.
As the authors demonstrated 13, a minor modification of one of the theories of Hrbacek is a perfect candidate for the stronger requirements mentioned above. In some sense this theory also improves upon IST as it is an external extension of bounded set theory BST, essentially, the theory of those sets of IST which are elements of standard sets. If one scrutinizes known applications of IST none of them makes any essential use of those internal sets which are not of this type. Moreover, BST admits without any restriction a very useful algorithm of conversion of formulas (known as Nelson's reduction algorithm), valid in IST only for special types of formulas, and has some other advantages, especially in a fair treatment of ``external sets'' (that is, definable subclasses of sets, which are not necessarily sets themselves in internal theories like IST or BST) causing so much trouble for IST practitioners.
We call this nonstandard set theory Hrbacek set theory, HST. Its axioms, stated in a very convenient way, allow to deduce, in quite a straightforward manner and even using the same technical notation (``asterisks'') known from the model-theoretic development of nonstandard analysis, many substantial results in nonstandard mathematics. On the other hand, since the internal universe I of HST models bounded set theory, an improved version of IST, ``internal'' forms of reasoning, well known to IST practitioners, can also be carried out in HST. Metamathematically, unlike IST and IST-based theories, HST admits an interpretation in the ZFC universe, of the kind mentioned above. In addition, it poses deep set theoretic problems and admits such advanced foundational tools as constructibility and forcing to find solutions.
This book was written with the goal to systematize recent development in the domain of axiomatic foundations of nonstandard analysis, including metamathematical, applied, and, to less extent, philosophical issues, in particular, with the following three general aims in mind:
Acknowledgement. The authors are thankful to David Ballard and Karel Hrbacek for their patience in reading through several consecutive drafts and many remarks and corrections. One of the authors (V.Kanovei) acknowledges the support of RFFI in 1998-2000 and 2003-2004. Both authors are grateful to the DFG for the continued support of their cooperation without which this book would not have been written.
Wuppertal, May 2004
Vladimir Kanovei, Michael Reeken
This document was generated using the LaTeX2HTML translator Version 99.2beta8 (1.43)
Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer
Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department,
Macquarie University, Sydney.
The command line arguments were:
latex2html -no_subdir -split 0 -show_section_numbers
/tmp/lyx_tmpdir828qv0t3h/lyx_tmpbuf0/pref.tex
The translation was initiated by Michael Reeken on 2004-06-01
Another early nonstandard axiomatic system, alternative set theory AST of Vopenka, appeared, in published form, even somewhat earlier, ``The alternative set theory'' of A.Sochor in Lecture Notes in Math. 537 (1976), 259-273, is, perhaps, the first really relevant publication, although the origins go back to P.Vopenka and P.Hájek, The theory of Semisets, North-Holland, 1972, and earlier. AST is closer, in its spirit, to Hrbacek's approach, in particular, in that it directly involves ``external sets'' (called semisets in the AST vocabulary), but differs from both Nelson's and Hrbacek's theories in that its ``standard universe'' consists of hereditarily finite sets rather than all sets of ZFC, and in this sense AST is a nonstandard extension of Peano arithmetic (or ZFC where the Infinity axiom is replaced by its negation) rather than full ZFC, which implies affinities rather with the model-theoretic version of foundations.
These three initial attempts to fully axiomatize nonstandard mathematics can hardly be linearly ordered in any reasonable sense, with any sort of preference assigned in some sound manner. It is fair to assert, on the base of available records, that all three were undertaken independently of each other and led to results of comparable quality (although not of comparable impact on the practice of nonstandard mathematics, where IST has preference), in addition, all three were based upon earlier development in foundations of nonstandard analysis.
It must be pointed out that at least some axioms of Nelson's, Hrbacek's, and other systems of the same kind have direct or implicit predecessors elaborated within model-theoretic foundations. ``Bounded internal set theory'' of Diener and Stroyan in Nonstandard analysis and its applications (N.Cutland ed.), Cambridge Univ. Press, 1988, 258-281, demonstrates the transmission of ideas from principles valid in nonstandard superstructures to axioms of IST.