Internal set theory: Encyclopedia II - Internal set theory - Formal axioms for IST

Internal set theory - Formal axioms for IST

There are three axioms of IST to add to the established ZFC set theoretic axioms (note that use of the ZFC axiom schemas is restricted: the axiom schemas of separation and replacement can only be used with classical formulas, just as in ZFC proper) - conveniently one for each letter in the name: Idealisation, Standardisation, and Transfer. All the principles described above can be formally derived from these three additional axiom schemes.

Internal set theory - I : Idealisation

• For every classical relation R, and for arbitrary values for all other free variables, we have that if for each standard, finite set F, there exists a g such that R( g, f ) holds for all f in F, then there is a particular G such that for any standard f we have R( G, f ), and conversely, if there exists G such that for any standard f, we have R( G, f ), then for each finite set F, there exists a g such that R( g, f ) holds for all f in F.

This very general axiom scheme upholds the existence of 'ideal' elements in appropriate circumstances. Three particular applications demonstrate important consequences.

If S is standard and finite, we take for the relation R ( g , f ) : g and f are in S but are not equal. Since the intersection of two standard finite sets is standard (by Transfer - see below) and finite, and since "For every standard, finite subset F of S there is an element g in S such that g ≠ f for all f in F." is false (since no such g exists in the case where F = S), then we may use Idealisation to tell us that "There is a G in S such that G ≠ f for all standard f in S " is also false, i.e. all the elements of S are standard.

The power set of a standard finite set is standard (by Transfer) and finite, so that all the subsets of a standard finite set are standard and finite.

If S is infinite, then we take for the relation R ( g, f ) : g and f are in S but are not equal. Since "For every standard, finite subset F of S there is an element g in S such that g ≠ f for all f in F." - say by choosing g as any element of S not in F - we may use Idealisation to derive "There is a G in S such that G ≠ f for all standard f in S ." In other words, every infinite set contains a non-standard element (many, in fact).

If S is non-standard, we take for the relation R ( g, f ) : g and f are in S but are not equal. Since "For every standard, finite subset F of S there is an element g in S such that g ≠ f for all f in F." - say by choosing g as any element of S not in F (F cannot be equal to S since F is standard and S is non-standard) - we may use Idealisation to derive "There is a G in S such that G ≠ f for all standard f in S ." In other words, every non-standard set contains a non-standard element.

As a consequence of all these results, all the elements of S are standard iff S is standard and finite.

Since "For every standard, finite set of natural numbers F there is a natural number g such that g > f for all f in F." - say, g = maximum( F ) + 1 - we may use Idealisation to derive "There is a natural number G such that G > f for all standard natural numbers f." In other words, there exists a natural number greater than any standard natural number.

More precisely we take for R ( g, f ) : g is a finite set containing element f. Since "For every standard, finite set F, there is a finite set g such that f ∈ g for all f in F." - say by choosing g = F itself - we may use Idealisation to derive "There is a finite set G such that f ∈ G for all standard f." For any set S, the intersection of S with the set G is a finite subset of S which contains every standard element of S.

Internal set theory - S : Standardisation

• If A is a standard set and P any property, classical or otherwise, then there is a unique, standard subset B of A whose standard elements are precisely the standard elements of A satisfying P (but the behaviour of B's non-standard elements is not prescribed).

Internal set theory - T : Transfer

• If all the parameters A, B, C, ..., W of a classical formula F have standard values then F( x, A, B,..., W ) holds for all x's as soon as it holds for all standard xs.

From which it follows that all uniquely defined concepts or objects within classical mathematics are standard.

Adapted from the Wikipedia article "Formal axioms for IST", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki