Implementation of mathematics in set theory: Difference between revisions

Revision as of 20:10, 25 October 2019

Latest revision as of 22:58, 2 May 2025

(13 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 46 ⟶ 47:

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 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 65 ⟶ 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. 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.

Line 93 ⟶ 94:

Outside of formal set theory, we usually specify a function in terms of its ___domain and codomain, as in the phrase "Let <math>f: A \to B</math> be a function". The ___domain of a function is just its ___domain as a relation, but we have not yet defined the codomain of a function. To do this we introduce the terminology that a function is '''from <math>A</math> to <math>B</math>''' if its ___domain equals <math>A</math> and its range ''is contained in'' <math>B</math>. In this way, every function is a function from its ___domain to its range, and a function <math>f</math> from <math>A</math> to <math>B</math> is also a function from <math>A</math> to <math>C</math> for any set <math>C</math> containing <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 AB</math>.

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\,|\,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 NFU for different reasons.

=== Special kinds of function ===

A function is an '''[[injective]]''' (also called '''[[bijection|one-to-one]]''') if it has an inverse function.

A function <math>f</math> from <math>A</math> to <math>B</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>.

Line 114 ⟶ 113:

== 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 150 ⟶ 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 199 ⟶ 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 314 ⟶ 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]]