Implementation of mathematics in set theory: Difference between revisions

Revision as of 01:22, 9 April 2016

Revision as of 18:06, 31 October 2016

Line 34:

== Ordered pair ==

{{main article|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.

Line 212:

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.

The operations of cardinal arithmetic are defined in a set-theoretically motivated way in both theories. <math>|A| + |B| = \{C \cup D \mid C \sim A \wedge D \sim B \wedge C \cap D = \emptyset\}</math>. One would like to define <math>|A|\cdot|B|</math> as <math>|A \times B|</math>, and one does this in [[ZFC]], but there is an obstruction in [[New Foundations|NFU]] when using the Kuratowski pair: one defines <math>|A|\cdot|B|</math> as <math>T^{-2}(|A \times B|)</math> because of the type displacement of 2 between the pair and its projections, which implies a type displacement of two between a cartesian product and its factors. It is straightforward to prove that the product always exists (but requires attention because the inverse of T is not total).