Implementation of mathematics in set theory: Difference between revisions

Revision as of 05:54, 19 August 2014

Revision as of 23:25, 18 March 2016

Line 77:

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

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

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

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

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

Line 91 ⟶ 86:

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

* A '''[[partial order]]''' if <math>R</math> is reflexive, antisymmetric, and transitive.

* A '''[[linear order]]''' if <math>R</math> is a partial order and for every <math>x, y</math> in the field of <math>R</math>, either <math>xRy</math> or <math>yRx</math>.

* A '''[[well-ordering]]''' if <math>R</math> is a linear order and well-founded.

* A '''set picture''' if <math>R</math> is well-founded and extensional, and the field of <math>R</math> either equals the downward closure of one of its members (called its ''top element''), or is empty.

Line 105 ⟶ 96:

In [[New Foundations|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]]' 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\!\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]].)

=== Operations on functions ===

Line 332 ⟶ 323:

*[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—by Thomas Forster.

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

* Randall Holmes: [http://math.boisestate.edu/~holmes/holmes/nf.html New Foundations Home Page]