Implementation of mathematics in set theory: Difference between revisions

Revision as of 19:59, 14 January 2013

Revision as of 18:56, 17 January 2013

Line 11:

Mathematical theories prove theorems (and nothing else). So saying that a theory allows the construction of a certain object means that it is a theorem of that theory that that object exists. This is a statement about a definition of the form "the x such that <math>\phi</math> exists", where <math>\phi</math> is a formula of our language: the theory proves the existence of "the x such that <math>\phi</math>" just in case it is a theorem that "there is one and only one x such that <math>\phi</math>". (See [[Bertrand Russell]]'s [[theory of descriptions]].) Loosely, the theory "defines" or "constructs" this object in this case. If the statement is not a theorem, the theory cannot show that the object exists; if the statement is provably false in the theory, it proves that the object cannot exist; loosely, the object cannot be constructed.

ZFC and NFU share the language of set theory, so the same formal definitions "the x such that <math>\phi</math>" can be contemplated in the two theories. A specific form of definition in the language of set theory is set-builder notation: <math>\{x \mid \phi\}</math> means "the set A such that for all x, <math>x \in A \leftrightarrow \phi</math>" (A cannot be free in <math>\phi</math>). This notation admits certain conventional extensions: <math>\{x \in B \mid \phi\}</math> is synonymous with <math>\{x \mid x \in B \wedge \phi\}</math>; <math>\{f(x_1,\ldots,x_n) \mid \phi\}</math> is defined as <math>\{z \mid \exists x_1,\ldots,x_n.\,(z=f(x_1,\dots,x_n) \wedge \phi)\}</math>, where <math>f(x_1,\ldots,x_n)</math> is an expression already defined.

Expressions definable in set-builder notation make sense in both ZFC and NFU: it may be that both theories prove that a given definition succeeds, or that neither do (the expression <math>\{x \mid x\not\in x\}</math> fails to refer to anything in ''any'' set theory with classical logic; in class theories like [[Von Neumann–Bernays–Gödel set theory|NBG]] this notation does refer to a class, but it is defined differently), or that one does and the other doesn't. Further, an object defined in the same way in ZFC and NFU may turn out to have different properties in the two theories (or there may be a difference in what can be proved where there is no provable difference between their properties).

Line 22:

These constructions appear first because they are the simplest constructions in set theory, not because they are the first constructions that come to mind in mathematics (though the notion of finite set is certainly fundamental!)

Even though NFU also allows the construction of set [[Urelement|ur-elements]] yet to become members of a set, the [[Empty set|empty set]] is the unique ''set'' with no members:

:<math>\emptyset \, \overset{\mathrm{def.}}{=} \{x \mid x \neq x\}</math>

For each object <math>x</math>, there is a set <math>\{x\}</math> with <math>x</math> as its only element:

:<math>\displaystyle\{x\} \overset{\mathrm{def.}}{=} \{y \mid y = x\}</math>

For objects <math>x</math> and <math>y</math>, there is a set <math>\{x,y\}</math> containing <math>x</math> and <math>y</math> as its only elements:

:<math>\{x,y\} \overset{\mathrm{def.}}{=} \{z \mid z=x \vee z=y\}</math>

The union of two sets is defined in the usual way:

:<math>x \cup y \overset{\mathrm{def.}}{=} \{z \mid z \in x \vee z \in y\}</math>

This is a recursive definition of unordered <math>n</math>-tuples for any concrete <math>n</math> (finite sets given as lists of their elements:)

:<math>\{x_1,\ldots,x_n,x_{n+1}\} \overset{\mathrm{def.}}{=} \{x_1,\ldots,x_n\} \cup \{x_{n+1}\}</math>

In [[New Foundations|NFU]], all the set definitions given work by stratified comprehension; in [[ZFC]], the existence of the unordered pair is given by the axiom of Pairing, the existence of the empty set follows by Separation from the existence of any set, and the boolean union of two sets exists by the axioms of Pairing and Union (<math>x \cup y = \bigcup\{x,y\}</math>).

Line 36:

{{main|Ordered pair}}

First, consider the '''ordered pair'''. The reason that this comes first is technical: ordered pairs are needed to implement [[Relation (mathematics)|relations]] and [[Function (mathematics)|functions]] which are needed to implementat other concepts which may seem to be prior.

The first definition of the ordered pair was the definition <math>(x,y) \overset{\mathrm{def.}}{=} \{\{\{x\},\emptyset\},\{\{y\}\}\}</math> proposed by [[Norbert Wiener]] in 1914 in the context of the type theory of [[Principia Mathematica]]. Wiener observed that this allowed the elimination of types of n-ary relations for <math>n>1</math> from the system of that work.

It is more usual now to use the definition <math>(x,y) \overset{\mathrm{def.}}{=} \{\{x\},\{x,y\}\}</math>, due to [[Kazimierz Kuratowski|Kuratowski]].

Either of these definitions works in either [[ZFC]] or [[New Foundations|NFU]]. In NFU, the Kuratowski pair has a technical disadvantage: it is two types higher than its projections. It is common to postulate the existence of a type-level ordered pair (a pair <math>(x,y)</math> which is the same type as its [[Projection (mathematics)|projections]]) in NFU. It is convenient to use the Kuratowski pair in both systems until the use of type-level pairs can be formally justified.

The internal details of these definitions have nothing to do with their actual mathematical function. For any notion <math>(x,y)</math> of ordered pair, the things that matter are that it satisfy the defining condition:

Line 56:

The '''[[inverse relation|converse]]''' of ''R'' is the relation <math>\{(y,x) \mid x R y\}</math>.

The '''___domain''' of ''R'' is the set <math>\{x \mid (\exists y.\,(x R y)\}</math>.

The '''range''' of ''R'' is the ___domain of the converse of ''R''.

Line 66:

The '''downward closure''' of a member ''x'' of the field of ''R'' is the smallest set ''D'' containing ''x'', and containing each ''zRy'' for each ''y''∈''D'' (i.e., including the preimage of each of its elements with respect to ''R'' as a subset).

The '''[[relation composition|relative product]]''' of ''R'' and ''S'', ''R|S'', is the relation <math>\{(x,z) \mid (\exists y.\,(xRy \wedge ySz)\}</math>.

In [[ZFC]], proving that these notions are all sets follows from ''[[axiom of union|Union]]'', ''[[axiom of separation|Separation]]'', and ''[[axiom of power set|Power Set]]''. In [[New Foundations|NFU]], it is easy to check that these definitions give rise to stratified formulas.

Line 76:

=== Properties and kinds of relations ===

Let ''R'' be some [[binary relation]]. ''R'' is:

*'''[[Reflexive relation|Reflexive]]''' if <math> \forall x \exist y . \,((xRy \vee yRx) \leftrightarrow xRx)</math>.

* '''[[Symmetric relation|Symmetric]]''' if <math>\forall xy .x,y \,(xRy \leftrightarrow yRx)</math>.

* '''[[Transitive relation|Transitive]]''' if <math>\forall xyz .x,y,z \,(xRy \wedge yRz \rightarrow xRz)</math>.

* '''[[Antisymmetric relation|Antisymmetric]]''' if <math>\forall xy .x,y \,(xRy \wedge yRx \rightarrow x=y)</math>.

* '''[[Well-founded relation|Well-founded]]''' if for every set ''S'' which meets the field of ''R'', <math>\ \exists x \in S</math> whose preimage under ''R'' does not meet ''S''.

Line 101:

== Functions ==

A [[function (set theory)|functional relation]] is a [[binary predicate]] ''F'' such that <math>(\forall xyz.x,y,z\,(x F y \wedge x F z \rightarrow y=z)</math>. Such a [[Relation (mathematics)|relation]] ([[Predicate (logic)|predicate]]) is implemented as a relation (set) exactly as described in the previous section. So the predicate ''F'' is implemented by the set <math>\{(x,y) \mid x F y\}</math>. A set of ordered pairs ''F'' is a function if and only if <math>(\forall xyz.x,y,z\,((x,y) \in F \wedge (x,z) \in F \rightarrow y=z)</math>. Define ''F''(''x)'') as the unique object ''y'' such that ''xFy'' (if there is one) or as the unique object ''y'' such that (''x,y'') ∈ ''F''. The presence in both theories of functional predicates which are not sets makes it useful to allow the notation ''F(x)'' both for sets ''F'' and for important functional predicates. As long as one does not quantify over functions in the latter sense, all such uses are in principle eliminable.

In [[New Foundations|NFU]], ''x'' has the same type as ''F''(''x''), and ''F'' is three types higher than ''F''(''x'') (one type higher, if a type-level ordered pair is used). For any set ''A'', define <math>F[A]</math> as <math>\{y \mid (\exists x.\,(x \in A \wedge y=F(x))\}</math>, more conveniently written as <math>\{F(x) \mid x \in A\}</math>. If ''A'' is a set and ''F'' is any functional relation, ''[[axiom of replacement|Replacement]]'' assures that <math>F[A]</math> is a set in [[ZFC]]. In NFU, <math>F[A]</math> and ''A'' have the same type, and ''F'' is two types higher than <math>F[A]</math> (the same type, if a type-level ordered pair is used).

The function ''I''(''x'') = ''x'' is not a set in [[ZFC]] because it is "too large". ''I''(''x'') is however, a set in NFU. The function (predicate) <math>S(x) = \{x\}</math> is not a function (set) in either theory; in ZFC because it is too large; in NFU because its definition is unstratified. Moreover, ''S''(''x'') can be proved not to exist in NFU: see the resolution of Cantor's paradox in [[New Foundations]].

Line 141:

The Axiom of Infinity of ZFC tells us that there is a set ''A'' which contains <math>\emptyset</math> and contains <math>y \cup \{y\}</math> for each <math>y \in A</math>. This set ''A'' is not uniquely determined (it can be made larger while preserving this closure property): the set ''N'' of natural numbers is

*<math>\{x \in A \mid (\forall B.\,(\emptyset \in B \wedge (\forall y.\,(y \in B \rightarrow y \cup \{y\} \in B) \rightarrow x \in B)\}</math>

which is the intersection of all sets which contain the empty set and are closed under the "successor" operation <math>y \mapsto y \cup \{y\}</math>.

Line 151:

The standard definition of the natural numbers, which is actually the oldest [[set-theoretic definition of natural numbers]], is as equivalence classes of finite sets under equinumerousness. Essentially the same definition is appropriate to [[New Foundations|NFU]] (this is not the usual definition, but the results are the same): define ''Fin'', the set of finite sets, as

:<math>\{A \mid (\forall F.\,(\emptyset \in F \wedge (\forall xy.x,y\,(x \in F \rightarrow x \cup \{y\} \in F)) \rightarrow A \in F)\}</math>

For any set <math>A \in Fin</math>, define <math>|A|</math> as <math>\{B \mid A \sim B\}</math>. Define ''N'' as the set <math>\{|A| \mid A \in Fin\}</math>.

Line 157:

The operations of arithmetic can be defined in a style similar to the style given above (using the definition of successor just given). They can also be defined in a natural set theoretical way: if A and B are disjoint finite sets, define |A|+|B| as <math>|A \cup B|</math>. More formally, define ''m+n'' for ''m'' and ''n'' in ''N'' as

:<math>\{A \mid (\exists BC.B,C\,(B \in m \wedge C \in n \wedge B \cap C = \emptyset \wedge A = B \cup C)\}</math>

(But note that this style of definition is feasible for the ZFC numerals as well, but more circuitous: the form of the [[New Foundations|NFU]] definition facilitates set manipulations while the form of the ZFC definition facilitates recursive definitions, but either theory supports either style of definition).

Line 168:

For any set ''A'', a set <math>P</math> is a '''partition''' of ''A'' if all elements of ''P'' are nonempty, any two distinct elements of ''P'' are disjoint, and <math>A=\bigcup P</math>.

For every equivalence relation ''R'' with field ''A'', <math>\{[x]_R \mid x \in A\}</math> is a partition of ''A''. Moreover, each partition ''P'' of ''A'' determines an equivalence relation <math>\{(x,y) \mid (\exists A \in P.\,(x \in A \wedge y \in A)\}</math>.

This technique has limitations in both [[ZFC]] and [[New Foundations|NFU]]. In ZFC, since the universe is not a set, it seems possible to abstract features only from elements of small domains. This can be circumvented using a trick due to [[Dana Scott]]: if ''R'' is an equivalence relation on the universe, define <math>[x]_R</math> as the set of all ''y'' such that <math>y R x</math> and the [[rank (set theory)|rank]] of ''y'' is less than or equal to the rank of any <math>z R x</math>. This works because the ranks are sets. Of course, there still may be a proper class of <math>[x]_R</math>'s. In NFU, the main difficulty is that <math>[x]_R</math> is one type higher than x, so for example the "map" <math>x \mapsto [x]_R</math> is not in general a (set) function (though <math>\{x\} \mapsto [x]_R</math> is a set). This can be circumvented by the use of the Axiom of Choice to select a representative from each equivalence class to replace <math>[x]_R</math>, which will be at the same type as ''x'', or by choosing a canonical representative if there is a way to do this without invoking Choice (the use of representatives is hardly unknown in ZFC, either). In NFU, the use of equivalence class constructions to abstract properties of general sets is more common, as for example in the definitions of cardinal and ordinal number below.

Line 219:

With each infinite cardinal, many order types are associated for the usual reasons (in either set theory).

Cantor's theorem shows (in both theories) that there are nontrivial distinctions between infinite cardinal numbers. In [[ZFC]], one proves <math>|A|<|P(A)|.</math> In [[New Foundations|NFU]], the usual form of Cantor's theorem is false (consider the case A=V), but Cantor's theorem is an ill-typed statement. The correct form of the theorem in [[New Foundations|NFU]] is <math>|P_1(A)|<|P(A)|</math>, where <math>P_1(A)</math> is the set of one-element subsets of A. <math>|P_1(V)|<|P(V)|</math> shows that there are "fewer" singletons than sets (the obvious bijection <math>x \mapsto \{x\}</math> from <math>P_1(V)</math> to ''V'' has already been seen not to be a set). It is actually provable in NFU + Choice that <math>|P_1(V)|<|P(V)|<<\ll|V|</math> (where <math>\ll</math> signals the existence of many intervening cardinals; there are many, many urelements!). Define a type-raising T operation on cardinals analogous to the T operation on ordinals: <math>T(|A|) = |P_1(A)|</math>; this is an external endomorphism of the cardinals just as the T operation on ordinals is an external endomorphism of the ordinals.

A set ''A'' is said to be <strong>cantorian</strong> just in case <math>|A| = |P_1(A)| = T(|A|)</math>; the cardinal <math>|A|</math> is also said to be a cantorian cardinal. A set ''A'' is said to be <strong>strongly cantorian</strong> (and its cardinal to be strongly cantorian as well) just in case the restriction of the singleton map to ''A'' (<math>(x \mapsto \{x\})\lceil A</math>) is a set. Well-orderings of strongly cantorian sets are always strongly cantorian ordinals; this is not always true of well-orderings of cantorian sets (though the shortest well-ordering of a cantorian set will be cantorian). A cantorian set is a set which satisfies the usual form of Cantor's theorem.

Line 247:

Any subset of a strongly cantorian set is strongly cantorian. The power set of a strongly cantorian set is strongly cantorian. The cartesian product of two strongly cantorian sets is strongly cantorian.

Introducing the Axiom of Counting means that types need not be assigned to variables restricted to ''N'' or to ''P''(''N)''), ''R'' (the set of reals) or indeed any set ever considered in classical mathematics outside of set theory.

There are no analogous phenomena in [[ZFC]]. See the main [[New Foundations]] article for stronger axioms that can be adjoined to NFU to enforce "standard" behavior of familiar mathematical objects.

Line 309:

pictures with a new top element yields a set picture whose isomorphism type will have as its preimages under E exactly the elements of the original collection. That is, for any collection of isomorphism types <math>[x^{\iota}] = T([x])</math>, there is an isomorphism type <math>[y]</math> whose preimage under E is exactly this collection.

In particular, there will be an isomorphism type ''[v]'' whose preimage under E is the collection of ''all'' ''T''[''x]'']'s (including ''T''[''v]'']). Since ''T''[''v''] ''E'' ''v'' and E is well-founded, <math>T[v] \neq v</math>. This resembles the resolution of the Burali-FortiBurali–Forti paradox discussed above and in the [[New Foundations]] article, and is in fact the local resolution of [[Mirimanoff's paradox]] of the set of all well-founded sets.

There are ranks of isomorphism classes of set pictures just as there are ranks of sets in the usual set theory. For any collection of set pictures ''A'', define ''S''(''A)'') as the set of all isomorphism classes of set pictures whose preimage under E is a subset of A; call A a "complete" set if every subset of ''A'' is a preimage under E. The collection of "ranks" is the smallest collection containing the empty set and closed under the S operation (which is a kind of power set construction) and under unions of its subcollections. It is straightforward to prove (much as in the usual set theory) that the ranks are well-ordered by inclusion, and so the ranks have an index in this well-order: refer to the rank with index <math>\alpha</math> as <math>R_{\alpha}</math>. It is provable that <math>|R_{\alpha}|=\beth_{\alpha}</math> for complete ranks <math>R_{\alpha}</math>. The union of the complete ranks (which will be the first incomplete rank) with the relation E looks like an initial segment of the universe of Zermelo-style set theory (not necessarily like the full universe of [[ZFC]] because it may not be large enough). It is provable that if <math>R_{\alpha}</math> is the first incomplete rank, then <math>R_{T(\alpha)}</math> is a complete rank and thus <math>T(\alpha)<\alpha</math>. So there is a "rank of the cumulative hierarchy" with an "external automorphism" T moving the rank downward, exactly the condition on a nonstandard model of a rank in the cumulative hierarchy under which a model of NFU is constructed in the [[New Foundations]] article. There are technical details to verify, but there is an interpretation not only of a fragment of [[ZFC]] but of [[New Foundations|NFU]] itself in this structure, with <math>[x]\in_{NFU}[y]</math> defined as <math>T([x]) E [y] \wedge [y] \in R_{T(\alpha)+1}</math>: this "relation" <math>E_{NFU}</math> is not a set relation but has the same type displacement between its arguments as the usual membership relation <math>\in</math>.

So there is a natural construction inside NFU of the cumulative hierarchy of sets which internalizes the natural construction of a model of NFU in Zermelo-style set theory.