Content deleted Content added
No edit summary |
No edit summary |
||
Line 3:
[[ZFC]] and in [[NFU]], the version of Quine's [[New Foundations]] shown to be consistent by
R. B. Jensen in 1969. For details of these two systems, consult their main articles.
It is not the primary aim of this article to say anything about the relative merits of these
theories as foundations for mathematics.
== 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!)
<math>\emptyset \equiv_{def} \{x \mid x \neq x\}</math>
The empty set is the unique set with no members. In NFU, there are also urelements with no members.
<math>\{x\} \equiv_{def} \{y \mid y = x\}</math>
For each object x, there is a set <math>\{x\}</math> with x as its only element.
<math>\{x,y\} \equiv_{def} \{z \mid z=x \vee z=y\}</math>
For objects x and y, there is a set <math>\{x,y\}</math> containing x and y as its only elements.
<math>x \cup y \equiv_{def} \{z \mid z \in x \vee z \in y\}</math>
The union of two sets is defined in the usual way.
<math>\{x_1,\ldots,x_n,x_{n+1}\} \equiv_{def} \{x_1,\ldots,x_n\} \cup \{x_{n+1}\}</math>
This is a recursive definition of unordered n-tuples for any n (finite sets given as lists
of their elements).
In NFU, all the set definitions given work by stratified comprehension; in ZFC,
the existence of the unordered pair is given by the axiom of Pairing, the existence
of the empty set follows by Separation from the existence of any set, and the boolean
union of two sets exists by the axioms of Pairing and Union (<math>x \cup y = \bigcup\{x,y\}</math>).
== Ordered pair ==
The first mathematical construction we consider is the <strong>ordered pair</strong>. The reason
that this comes first is technical: we will need it to implement notions of [[relation (mathematics) | relation]] and
[[function (mathematics) | function]] which are needed for implementations of other concepts which may seem to be prior.
The first definition of the ordered pair was the definition <math>(x,y) \equiv_{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) \equiv_{def} \{\{x\},\{x,y\}\}</math>, due to Kuratowski.
Either of these definitions works in either [[ZFC]] or [[NFU]]. In [[NFU]], the Kuratowski pair
has a technical disadvantage: it is two types higher than its projections. 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 projections) in [[NFU]]. For the moment, we will use the Kuratowski pair in both
systems, until we can give a formal justification for the introduction of the type-level pair.
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 things that matters are
that it satisfy 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.
| |||