Implementation of mathematics in set theory: Difference between revisions

Revision as of 18:46, 25 October 2019

Latest revision as of 22:58, 2 May 2025

(23 intermediate revisions by 10 users not shown)

Line 1:

{{Short description|none}}

This article examines the implementation of mathematical concepts in [[set theory]]. The implementation of a number of basic mathematical concepts is carried out in parallel in [[ZFC]] (the dominant set theory) and in [[New Foundations|NFU]], the version of Quine's [[New Foundations]] shown to be consistent by [[R. B. Jensen]] in 1969 (here understood to include at least axioms of [[Axiom of infinity|Infinity]] and [[Axiom of choice|Choice]]).

Line 15 ⟶ 16:

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 (set theory)|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).

Further, set theory imports concepts from other branches of mathematics (in intention, ''all'' branches of mathematics). In some cases, there are different ways to import the concepts into ZFC and NFU. For example, the usual definition of the first infinite [[Ordinal number|ordinal]] <math>\omega</math> in ZFC is not suitable for NFU because the object (defined in purely set theoretical language as the set of all finite [[von Neumann ordinal]]s) cannot be shown to exist in NFU. The usual definition of <math>\omega</math> in NFU is (in purely set theoretical language) the set of all infinite [[well-ordering]]s all of whose proper initial segments are finite, an object which can be shown not to exist in ZFC. In the case of such imported objects, there may be different definitions, one for use in ZFC and related theories, and one for use in NFU and related theories. For such "implementations" of imported mathematical concepts to make sense, it is necessary to be able to show that the two parallel interpretations have the expected properties: for example, the implementations of the natural numbers in ZFC and NFU are different, but both are implementations of the same mathematical structure, because both include definitions for all the primitives of [[Peano arithmetic]] and satisfy (the translations of) the Peano axioms. It is then possible to compare what happens in the two theories as when only set theoretical language is in use, as long as the definitions appropriate to ZFC are understood to be used in the [[ZFC]] context and the definitions appropriate to NFU are understood to be used in the NFU context.

Whatever is proven to exist in a theory clearly provably exists in any extension of that theory; moreover, analysis of the proof that an object exists in a given theory may show that it exists in weaker versions of that theory (one may consider [[Zermelo set theory]] instead of ZFC for much of what is done in this article, for example).

== Empty set, singleton, unordered pairs and tuples ==

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]] is the unique ''set'' with no members:

:<math>\left.\varnothing\right. \, \overset{\mathrm{def.}}{=} \left\{x : x \neq x\right\}</math>

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

:<math>\left.\varnothing\right. \overset{\mathrm{def.}}{=} \left\{x : x \neq x\right\}</math>

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

:<math>\left\{x\right\} \overset{\mathrm{def.}}{=} \left\{y : y = x\right\}</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>\left\{x,y\right\} \overset{\mathrm{def.}}{=} \left\{z : z=x \vee z = y\right\}</math>

The [[Union (set theory)|union]] of two sets is defined in the usual way:

:<math>\left.x \cup y\right. \, \overset{\mathrm{def.}}{=} \left\{z : z \in x \vee z \in y\right\}</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>\left\{x_1, \ldots, x_n, x_{n+1}\right\} \overset{\mathrm{def.}}{=} \left\{x_1, \ldots, x_n\right\} \cup \left\{x_{n+1}\right\}</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[[Axiom of pairing|Axiom of Pairing]], the existence of the empty set follows by [[Axiom schema of separation|Separation]] from the existence of any set, and the booleanbinary union of two sets exists by the axioms of Pairing and [[Axiom of union|Union]] (<math>x \cup y = \bigcup\{x,y\}</math>).

== 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 implementatimplement 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, these two definitions have a technical disadvantage: the Kuratowski ordered pair is two types higher than its projections, while the Wiener ordered pair is three types higher. 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 thingsthing that mattermatters areis that it satisfysatisfies the defining condition:

* :<math>(x,y)=(z,w) \ \equiv \ x=z \wedge y=w</math>

…and that it be reasonably easy to collect ordered pairs into sets.

== Relations ==

[[Relation (mathematics)|Relations]] are sets whose members are all [[ordered pair]]s. Where possible, a relation <math>R</math> (understood as a [[binary predicate]]) is implemented as <math>\{(x,y) \mid x R y\}</math> (which may be written as <math>\{z \mid \pi_1(z) R \pi_2(z)\}</math>). WhereWhen <math>R</math> is a setrelation, of ordered pairs,the readnotation <math>xRy</math> asmeans <math>\left(x, y\right) \in R</math>.

In [[ZFC]], some relations (such as the general equality relation or subset relation on sets) are 'too large'

to be sets (but may be harmlessly reified as [[proper class]]es). In [[New Foundations|NFU]], some relations (such as the membership relation) are not sets because their definitions are not stratified: in <math>\{(x,y) \mid x \in y\}</math>, <math>x</math> and <math>y</math> would

need to have the same type (because they appear as projections of the same pair), but also

successive types (because <math>x</math> is considered as an element of <math>y</math>).

Line 58:

The '''___domain''' of <math>R</math> is the set <math>\left\{x : \exists y \left(xRy\right)\right\}</math>.

The '''range''' of <math>R</math> is the ___domain of the converse of <math>R</math>. That is, the set <math>\left\{y : \exists x \left(xRy\right)\right\}</math>.

The '''field''' of <math>R</math> is the [[union (set theory)|union]] of the ___domain and range of <math>R</math>.

Line 66:

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

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

Notice that with our formal definition of a binary relation, the range and codomain of a relation are not distinguished:. thisThis could be done by representing a relation <math>R</math> with codomain <math>B</math> as <math>\left(R, B\right)</math>, but our development will not require this.

In [[ZFC]], one proves that these notions all generate or apply to sets via the [[ZFC]] axioms of ''[[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.

In [[ZFC]], any relation whose ___domain is a subset of a set <math>A</math> and whose range is a subset of a set <math>B</math> will be a set, since the [[cartesianCartesian product]] <math>A \times B = \left\{\left(a, b\right) : a \in A \wedge b \in B\right\}</math> is a set (being a subclass of <math>\mathcal{P}\!\left(A \cup B\right)</math>), and ''Separation'' provides for the existence of <math>\left\{\left(x, y\right) \in A \times B : xRy\right\}</math>. In [[New Foundations|NFU]], some relations with global scope (such as equality and subset) can be implemented as sets. In NFU, bear in mind that <math>x</math> and <math>y</math> are three types lower than <math>R</math> in <math>xRy</math> (one type lower if a type-level ordered pair is used).

Notice that the range and codomain of a relation are not distinguished: this could be done by representing a relation <math>R</math> with codomain <math>B</math> as <math>\left(R, B\right)</math>, but our development will not require this.

In [[ZFC]], any relation whose ___domain is a subset of a set <math>A</math> and whose range is a subset of a set <math>B</math> will be a set, since the [[cartesian product]] <math>A \times B = \left\{\left(a, b\right) : a \in A \wedge b \in B\right\}</math> is a set (being a subclass of <math>\mathcal{P}\!\left(A \cup B\right)</math>), and ''Separation'' provides for the existence of <math>\left\{\left(x, y\right) \in A \times B : xRy\right\}</math>. In [[New Foundations|NFU]], some relations with global scope (such as equality and subset) can be implemented as sets. In NFU, bear in mind that <math>x</math> and <math>y</math> are three types lower than <math>R</math> in <math>xRy</math> (one type lower if a type-level ordered pair is used).

=== Properties and kinds of relations ===

LetA <math>R</math> be some [[binary relation]]. <math>R</math> is:

*'''[[Reflexive relation|Reflexive]]''' if <math>xRx</math> for every <math>x</math> in the field of <math>R</math>.

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

Line 83 ⟶ 81:

* '''Extensional''' if for every <math>x, y</math> in the field of <math>R</math>, <math>x = y</math> if and only if <math>x</math> and <math>y</math> have the same preimage under <math>R</math>.

Relations having certain combinations of the above properties have standard names. A binary relation <math>R</math> is:

* An '''[[equivalence relation]]''' if <math>R</math> is reflexive, symmetric, and transitive.

Line 92 ⟶ 90:

== Functions ==

A [[function (set theory)|'''functional relation]]''' is a [[binary predicate]] <math>F</math> such that <math>\forall x, y, z\,\left(xFy \wedge xFz \to y = z\right).</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 <math>F</math> is implemented by the set <math>\left\{\left(x, y\right) : xFy\right\}</math>. A set of ordered pairsrelation <math>F</math> is a '''function''' if and only if <math>\forall x, y, z\,\left(\left(x, y\right) \in F \wedge \left(x, z\right) \in F \to y = z\right).</math>. It is therefore possible to define thisthe value function <math>F\!\left(x\right)</math> as the unique object <math>y</math> such that <math>xFy</math>&thinsp;–&thinsp;i.e.: <math>x</math> is <math>F</math>-related to <math>y</math> such that the relation <math>f</math> holds between <math>x</math> and <math>y</math>&thinsp;–&thinsp;or as the unique object <math>y</math> such that <math>\left(x, y\right) \in F</math>. The presence in both theories of functional predicates which are not sets makes it useful to allow the notation <math>F\!\left(x\right)</math> both for sets <math>F</math> 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.

InOutside of [[Newformal Foundations|NFU]]set theory, <math>x</math>we hasusually thespecify samea typefunction asin <math>F\!\left(x\right)</math>,terms of its ___domain and <math>F</math>codomain, isas threein typesthe higherphrase than"Let <math>Ff: A \!\left(x\right)to B</math> (onebe typea higher,function". ifThe a___domain type-levelof ordereda pairfunction is used).just Toits solve___domain thisas problema relation, onebut couldwe definehave <math>F\left[A\right]</math>not asyet <math>\left\{ydefined :the \existscodomain x\,\left(xof \ina Afunction. \wedgeTo ydo =this F\!\left(x\right)\right)\right\}</math>we forintroduce anythe setterminology <math>A</math>,that buta thisfunction is more conveniently written as'''from <math>\left\{F\!\left(x\right) : x \in A\right\}</math>. Then, ifto <math>AB</math>''' isif aits set___domain andequals <math>FA</math> isand anyits functional relation, therange '[[axiom'is ofcontained replacement]]in'' assures that <math>F\left[A\right]B</math>. In this way, every function is a setfunction infrom [[ZFC]].its In___domain to its NFUrange, and a function <math>F\left[A\right]f</math> andfrom <math>A</math> now have the same type, andto <math>FB</math> is twoalso typesa higherfunction thanfrom <math>F\left[A\right]</math> (theto same<math>C</math> type,for ifany aset type-level<math>C</math> orderedcontaining pair is used)<math>B</math>.

Indeed, no matter which set we consider to be the codomain of a function, the function does not change as a set since by definition it is just a set of ordered pairs. That is, a function does not determine its codomain by our definition. If one finds this unappealing then one can instead define a function as the ordered pair <math>(f, B)</math>, where <math>f</math> is a functional relation and <math>B</math> is its codomain, but we do not take this approach in this article (more elegantly, if one first defines ordered triples - for example as <math>(x, y, z) = (x, (y, z))</math>- then one could define a function as the ordered triple <math>(f, A, B)</math> so as to also include the ___domain). Note that the same issue exists for relations: outside of formal set theory we usually say "Let <math>R \subseteq A \times B</math> be a binary relation", but formally <math>R</math> is a set of ordered pairs such that <math>\text{dom}\,R \subseteq A</math> and <math>\text{ran}\,R \subseteq B</math>.

The function <math>I\!\left(x\right) = x</math> is not a set in [[ZFC]] because it is 'too large.' <math>I\!\left(x\right)</math> is, however, a set in NFU. The function (predicate) <math>S\!\left(x\right) = \left\{x\right\}</math> is neither a function nor a set in either theory; in ZFC, this is true because such a set would be too large, and, in NFU, this is true because its definition would not be [[Stratified formula#In set theory|stratified]]. Moreover, <math>S\!\left(x\right)</math> can be proved not to exist in NFU (see the resolution of Cantor's paradox in [[New Foundations]].)

In NFU, <math>x</math> has the same type as <math>F\!\left(x\right)</math>, and <math>F</math> is three types higher than <math>F\!\left(x\right)</math> (one type higher, if a type-level ordered pair is used). To solve this problem, one could define <math>F\left[A\right]</math> as <math>\left\{y : \exists x\,\left(x \in A \wedge y = F\!\left(x\right)\right)\right\}</math> for any set <math>A</math>, but this is more conveniently written as <math>\left\{F\!\left(x\right) : x \in A\right\}</math>. Then, if <math>A</math> is a set and <math>F</math> is any functional relation, the [[Axiom of replacement|Axiom of Replacement]] assures that <math>F\left[A\right]</math> is a set in [[ZFC]]. In NFU, <math>F\left[A\right]</math> and <math>A</math> now have the same type, and <math>F</math> is two types higher than <math>F\left[A\right]</math> (the same type, if a type-level ordered pair is used).

The function <math>I</math> such that <math>I\!\left(x\right) = x</math> is not a set in [[ZFC]] because it is '"too large".' <math>I\!\left(x\right)</math> is, however, a set in NFU. The function (predicate) <math>S</math> such that <math>S\!\left(x\right) = \left\{x\right\}</math> is neither a function nor a set in either theory; in ZFC, this is true because such a set would be too large, and, in NFU, this is true because its definition would not be [[Stratified formula#In set theory|stratified]]. Moreover, <math>S\!\left(x\right)</math> can be proved not to exist in NFU (see the resolution of [[Cantor's paradox]] in [[New Foundations]].)

=== Operations on functions ===

Let <math>f</math> and <math>g</math> be arbitrary functions. The '''[[function composition|composition]]''' of <math>f</math> and <math>g</math>, <math>g \circ f</math>, is defined as the relative product <math>f \mid ,|\,g</math>, but only if this results in a function such that <math>g \circ f</math> is also a function, with <math>\left(g \circ f\right)\!\left(x\right) = g\!\left(f\!\left(x\right)\right)</math>, if the range of <math>f</math> is a subset of the ___domain of <math>g</math>. The '''[[inverse function|inverse]]''' of <math>f</math>, <math>f^\left(-1\right)</math>, is defined as the [[inverseconverse relation|converse]] of <math>f</math> if this is a function. Given any set <math>A</math>, the identity function <math>i_A</math> is the set <math>\left\{\left(x, x\right) \mid x \in A\right\}</math>, and this is a set in both [[ZFC]] and [[New Foundations|NF]]NFU for different reasons.

=== Special kinds of function ===

IfA function <math>f</math> is a function from <math>A</math> to <math>B</math>, <math>f</math> is a:

A function is an '''[[Injective function|injection]]''' and '''[[bijection|one-to-one]]''' if it has an inverse function.

If <math>A</math> and <math>B</math> are sets, <math>f</math> is a '''function from <math>A</math> to <math>B</math>''' if <math>f</math> is a function whose ___domain is <math>A</math>, and whose range is included in <math>B</math>.

If <math>f</math> is a function from <math>A</math> to <math>B</math>, <math>f</math> is a:

* '''[[Injective function|Injection]]''' from <math>A</math> to <math>B</math> if the [[image (mathematics)|image]]s under <math>f</math> of distinct members of <math>A</math> are distinct members of <math>B</math>.

* '''[[Surjection]]''' from <math>A</math> to <math>B</math> if the range of <math>f</math> is <math>B</math>.

* '''[[Bijection]]''' from <math>A</math> to <math>B</math> if <math>f</math> is both an injection and a surjection.

Defining functions as ordered pairs <math>(f, B)</math> or ordered triples <math>(f, A, B)</math> has the advantages that we do not have to introduce the terminology of being a function "from <math>A</math> to <math>B</math>", and that we can speak of "being surjective" outright as opposed to only being able to speak of "being surjective onto <math>B</math>".

This terminology adjusts for the fact that a function, as defined above, does not determine its codomain.

== Size of sets ==

In both [[ZFC]] and [[New Foundations|NFU]], two sets ''A'' and ''B'' are the same size (or are '''[[equinumerous]]''') if and only if there is a [[Bijective function|bijection]] ''f'' from ''A'' to ''B''. This can be written as <math>|A|=|B|</math>, but note that (for the moment) this expresses a relation between ''A'' and ''B'' rather than a relation between yet-undefined objects <math>|A|</math> and <math>|B|</math>. Denote this relation by <math>A \sim B</math> in contexts such as the actual definition of the [[Cardinal number|cardinals]] where even the appearance of presupposing abstract cardinals should be avoided.

Similarly, define <math>|A| \leq |B|</math> as holding if and only if there is an [[Injective function|injection]] from ''A'' to ''B''.

It is straightforward to show that the relation of equinumerousness is an [[equivalence relation]]: equinumerousness of ''A'' with ''A'' is witnessed by <math>i_A</math>; if ''f'' witnesses <math>|A|=|B|</math>, then <math>f^{-1}</math> witnesses <math>|B|=|A|</math>; and if ''f'' witnesses <math>|A|=|B|</math> and ''g'' witnesses <math>|B|=|C|</math>, then <math>g\circ f</math> witnesses <math>|A|=|C|</math>.

It can be shown that <math>|A| \leq |B|</math> is a [[linear order]] on abstract cardinals, but not on sets. Reflexivity is obvious and transitivity is proven just as for equinumerousness. The [[Cantor–Bernstein–Schroeder theorem|Schröder–Bernstein theorem]], provable in [[ZFC]] and [[New Foundations|NFU]] in an entirely standard way, establishes that

*<math>|A| \leq |B| \wedge |B| \leq |A| \rightarrow |A| = |B|</math>

(this establishes antisymmetry on cardinals), and

Line 151 ⟶ 149:

(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).

The two implementations are quite different. In ZFC, choose a [[representative (mathematics)|representative]] of each finite cardinality (the equivalence classes themselves are too large to be sets); in NFU the equivalence classes themselves are sets, and are thus an obvious choice for objects to stand in for the cardinalities. However, the arithmetic of the two theories is identical: the same abstraction is implemented by these two superficially different approaches.

== Equivalence relations and partitions ==

Line 200 ⟶ 198:

Cardinal numbers are defined in [[New Foundations|NFU]] in a way which generalizes the definition of natural

number: for any set ''A'', <math>|A| =_\,\overset{\mathrm{def}}{=} \left\{B \mid B \sim A\right\}</math>.

In [[ZFC]], these equivalence classes are too large as usual. Scott's trick could be used (and indeed is used in [[Zermelo–Fraenkel set theory|ZF]]), <math>|A|</math> is usually defined as the smallest order type (here a von Neumann ordinal) of a well-ordering of ''A'' (that every set can be well-ordered follows from

Line 315 ⟶ 313:

==References==

*[[Keith Devlin]], 1994. ''The Joy of Sets'', 2nd ed. Springer-Verlag.

*Holmes, Randall, 1998. ''[httphttps://mathrandall-holmes.boisestategithub.edu/~holmes/holmesio/head.pdf Elementary Set Theory with a Universal Set]''. Academia-Bruylant. The publisher has graciously consented to permit diffusion of this introduction to NFU via the web. Copyright is reserved.

*Potter, Michael, 2004. ''Set Theory and its Philosophy'', 2nd ed. Oxford Univ. Press.

*Suppes, Patrick, 1972. ''Axiomatic Set Theory''. Dover.

*Tourlakis, George, 2003. ''Lectures in Logic and Set Theory, Vol. 2''. Cambridge Univ. Press.

== External links ==

* [http://us.metamath.org/ Metamath:] A web site devoted to an ongoing derivation of mathematics from the axioms of ZFC and [[first-order logic]].

* [[Stanford Encyclopedia of Philosophy]]:

** [http://plato.stanford.edu/entries/quine-nf Quine's New Foundations]—by Thomas Forster.

** [http://setis.library.usyd.edu.au/stanford/entries/settheory-alternative/ Alternative axiomatic set theories]—by Randall Holmes.

* Randall Holmes: [httphttps://mathrandall-holmes.boisestategithub.edu/~holmes/holmesio/nf.html New Foundations Home Page]

{{Mathematical logic}}

[[Category:Large-scale mathematical formalization projects]]

[[Category:Formalism (deductive)]]

[[Category:Mathematical logic]]

[[Category:Set theory]]

[[Category:Formalism (deductive)]]

[[Category:Large-scale mathematical formalization projects]]