Implementation of mathematics in set theory: Difference between revisions

Revision as of 16:21, 2 June 2022

Latest revision as of 22:58, 2 May 2025

(4 intermediate revisions by 4 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 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 97 ⟶ 98:

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 ===

Line 103 ⟶ 104:

=== 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 319 ⟶ 318:

*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.

Line 326:

* Randall Holmes: [https://randall-holmes.github.io/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]]