Basic Construction for Nonstandard Analysis

Why nonstandard analysis? Nonstandard analysis is a technique rather than a subject • • •

The subject can be claimed to be of importance insofar as it leads to simpler, more accessible expositions, or (more important) to mathematical discoveries. [14, p. 1]

The initial part of [14] dwells on how to enlarge a standard universe into a nonstandard one. While taking stock at the end of the first chapter, Martin stresses that much of the machinery developed up to there is not used in the remainder of the book; then, in recapitulating which key points the reader should remember, he underlines the three main tools of nonstandard analysis: transfer principle, concurrence, and internality.

We will now give a quick account of the elaborate ultrapower construction whose details Martin deems “quite all right”, after that turning point, “to banish from our consciousness”. We thereby undertake a formal recasting of that construction with Ref, in order to encapsulate it within Ref’s Theorys.

The standard universe is the superstructure

See [8, pp. 5-6]. In a recent personal web-page, David Aspinall (Univ. of Edinburgh) defines Proof Engineering to mean the activity on construction, maintenance, documentation and presentation of large formal proof developments. Within Proof Engineering, according to Aspinall, “Software Engineering provides the techniques to develop large, structured and well-specified repositories of computer code; proof checking provides the mechanisms to provide a complete semantics and formal correctness as an absolute quality criterion.”.

built on a set s = s₀, whose (n + 1)-st stage is s_n+1 = s_n U P(s_n) for each n e N = {0, 1, 2,...} (as customary, P designates the powerset operator). It is essential that s consists of individuals; namely that 0 ? s and that no element of any element of s pops up at any stage, viz., ^ n U s = 0. Every set w of individuals generates a superstructure w, much as we have just indicated for s; e.g., 0 consists of the entities known as hereditarily finite sets.

The superstructure ^ gets embedded into another one, w, built on a specific set w э s of individuals, by means of a function x ^ *x; in particular *s = w. A set w c W is cut out of the wider superstructure: this W, satisfying the revealing equality W = U_i eN *5;, will be the nonstandard universe paired with s'.

Such companions s', w will—in a sense—have the same properties. An unrestrained formulation of this principle would have paradoxical consequences, though, and we must postpone to Sect. 10.3 the precise formulation of criteria enabling the transferability of properties. In a major instance studied in [14, Chap. 2], s includes an Archimedean ordered field D, e.g., the field Q of rational numbers or the field R of real numbers; then 1D, included in w, will still satisfy the laws of an ordered field but will violate the Archimedean property which—roughly speaking—rejects infinitely large or infinitely small elements.⁵

Before showing how to construct w, let us make it clear which are the sets which qualify as universes:⁶

Definition 10.1 A set U is called a universe if 0eU and the following properties hold for all x, y:

Upward closure: If x, y e U, then {x, y} e U.

Downward closure: If x e U and x n U =0, then x c U

(this says that each element x of U is either an individual, hence has no element in U, or is included in U). 4

The upward closure property readily yields that a universe U is always closed with respect to the Kuratowski ordered pair formation (x, y) =_Def ^[1]; by also exploiting downward closure we get, for each function g e U such that g U dom(g) c U, that the result g fx of applying g to a set x belongs to U. (By function we mean here a single-valued set of ordered pairs; moreover, when g fails to be a function or x does not belong to its domain, g fx is meant to designate 0.) Every superstructure based on a set of individuals is a universe, so it is closed with respect to pair formation and to function application.

5In particular, when D = R, we get a field, *R, of entities called hyperreal numbers. In *R there are positive numbers lying infinitely close to zero; the reciprocals of such infinitesimals must, of course, exceed any positive integer.
6Our definition of universe marginally differs from the one given in [14, p. 15] in that we are not assuming individuals to be given beforehand. Certain proper classes can also be regarded as universes, according to a plain generalization of this definition to be seen in Fig. 10.5.

The construction of w relies on a pair ж, i such that

(1) ж c P(i) {0};
(2) x n y e ж for all x, y e ж;
(3) у e ж whenever x e ж and x c у c i;
(4) no strict superset of ж meets the filter conditions (1)-(3).
(Consequently, see [14,p.10],{x n i, i x }n ж = 0 holds for every set x .)Bywell- established terminology, ж is an ultrafilter¹ over the index set i = U ж. Momentarily we do not commit our choice of ж and i in any way; this choice is most relevant, though, for the applicability of the nonstandard techniques.

We say that a property C(j) of elements of i holds a.e. (‘almost everywhere’) if {j e i | C (j)} e ж, that is, if the indices satisfying C form a set which belongs to ж. Thus, for example, the condition gj = hj a.e. defines an equivalence relation over s', the set of all functions from the index set into standard individuals; we can then pick a representative element pg out of each equivalence class {h e s' | gj = hj a.e.}, and finally get the set

of nonstandard individuals. This is an enlargement of s, whose elements can in fact be put in natural correspondence with the representatives of a.e. constant functions (the injection of s into w is x ^ p g_x, where g_x e {x}^[2], i.e. g_x = i x {x}). We will manage to enforce the strict inclusion w D s in Sect. 10.4; our present assumptions only suffice to ensure that w 2 s.

The construction at issue continues with the specification of a function,", whose set of values will be the universe w we are after and whose domain is layered in a way mimicking the hierarchical organization

(where Ы and Щ designate disjoint unions) of the standard universe:

For each f e^ such that fj e s₀ a.e., we put f = pg, where g e s' is such that fj = gj a.e. Next, for successive numbers n e N, we define a la Mostowski the image f of each function f such that fj e P (s_n) s_n a.e., by putting

The following facts admit straightforward proofs:

• W, the set of all images f , is a universe;
• fe g if and only if fj e gj a.e.;
• f = g if and only if fj = gj a.e.

Much as before, there is a natural one-one correspondence between ^ and those functions, in the domain of", which are a.e. constant; hence the embedding * ofSinto W announced at the beginning of this section is plainly induced by ". This function

• will soon be extended by bringing into its domain many subsets of "s which do not belong to s'.

Before going any further, let us pause to recall that Martin works under the assumption that “we have available some given sufficiently large set I of true individuals (sometimes called urelemente), about which we assume nothing except that they are not sets” [14, p. 11], and he repeatedly stresses that questions as to the true ‘nature’ of such entities are irrelevant to mathematical practice.^[3] Anyway, we will have to face this issue (see Sect. 10.8) while carrying out our formalization task, because our framework will be a set theory devoid of individuals proper: our ‘individuals’ will simply be sets whose elements are ‘inaccessible’ from within the superstructure.

[1] x}, {x, y
[2] 7A slicker characterization of ultrafilters will be shown in Fig. 10.1.
[3] In a similar attitude, [11, p. 54] states that “one possible view is that the integers are atoms andshould not be viewed as sets. Even in this case, one might still wish to prevent the existence ofunrestricted atoms. In any case, for the ‘genuine’ sets, Extensionality holds and the other sets aremerely harmless curiosities.”.