This article examines the implementation of mathematical concepts in
set theory
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
. The implementation of a number of basic mathematical concepts is carried out in parallel in
ZFC (the dominant set theory) and in
NFU, the version of Quine's
New Foundations
In mathematical logic, New Foundations (NF) is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of ''Principia Mathematica''. Quine first proposed NF in a 1937 article titled "New Foundations ...
shown to be consistent by
R. B. Jensen
Ronald Björn Jensen (born April 1, 1936) is an American mathematician who lives in Germany, primarily known for his work in mathematical logic and set theory.
Career
Jensen completed a BA in economics at American University in 1959, and a Ph.D. ...
in 1969 (here understood to include at least axioms of
Infinity
Infinity is that which is boundless, endless, or larger than any natural number. It is often denoted by the infinity symbol .
Since the time of the ancient Greeks, the philosophical nature of infinity was the subject of many discussions amo ...
and
Choice
A choice is the range of different things from which a being can choose. The arrival at a choice may incorporate motivators and models. For example, a traveler might choose a route for a journey based on the preference of arriving at a giv ...
).
What is said here applies also to two families of set theories: on the one hand, a range of theories including
Zermelo set theory
Zermelo set theory (sometimes denoted by Z-), as set out in a seminal paper in 1908 by Ernst Zermelo, is the ancestor of modern Zermelo–Fraenkel set theory (ZF) and its extensions, such as von Neumann–Bernays–Gödel set theory (NBG). It be ...
near the lower end of the scale and going up to ZFC extended with
large cardinal
In the mathematical field of set theory, a large cardinal property is a certain kind of property of transfinite cardinal numbers. Cardinals with such properties are, as the name suggests, generally very "large" (for example, bigger than the least ...
hypotheses such as "there is a
measurable cardinal
In mathematics, a measurable cardinal is a certain kind of large cardinal number. In order to define the concept, one introduces a two-valued measure on a cardinal , or more generally on any set. For a cardinal , it can be described as a subdivisio ...
"; and on the other hand a hierarchy of extensions of NFU which is surveyed in the
New Foundations
In mathematical logic, New Foundations (NF) is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of ''Principia Mathematica''. Quine first proposed NF in a 1937 article titled "New Foundations ...
article. These correspond to different general views of what the set-theoretical universe is like, and it is the approaches to implementation of mathematical concepts under these two general views that are being compared and contrasted.
It is not the primary aim of this article to say anything about the relative merits of these theories as foundations for mathematics. The reason for the use of two different set theories is to illustrate that multiple approaches to the implementation of mathematics are feasible. Precisely because of this approach, this article is not a source of "official" definitions for any mathematical concept.
Preliminaries
The following sections carry out certain constructions in the two theories
ZFC and
NFU and compare the resulting implementations of certain mathematical structures (such as the
natural numbers
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''cardinal n ...
).
Mathematical theories prove theorems (and nothing else). So saying that a theory allows the construction of a certain object means that it is a theorem of that theory that that object exists. This is a statement about a definition of the form "the x such that
exists", where
is a
formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwee ...
of our
language
Language is a structured system of communication. The structure of a language is its grammar and the free components are its vocabulary. Languages are the primary means by which humans communicate, and may be conveyed through a variety of met ...
: the theory proves the existence of "the x such that
" just in case it is a theorem that "there is one and only one x such that
". (See
Bertrand Russell's theory of descriptions
The theory of descriptions is the philosopher Bertrand Russell's most significant contribution to the philosophy of language. It is also known as Russell's theory of descriptions (commonly abbreviated as RTD). In short, Russell argued that the ...
.) Loosely, the theory "defines" or "constructs" this object in this case. If the statement is not a theorem, the theory cannot show that the object exists; if the statement is provably false in the theory, it proves that the object cannot exist; loosely, the object cannot be constructed.
ZFC and NFU share the language of set theory, so the same formal definitions "the x such that
" can be contemplated in the two theories. A specific form of definition in the language of set theory is
set-builder notation
In set theory and its applications to logic, mathematics, and computer science, set-builder notation is a mathematical notation for describing a set by enumerating its elements, or stating the properties that its members must satisfy.
Defining ...
:
means "the set A such that for all x,
" (A cannot be
free
Free may refer to:
Concept
* Freedom, having the ability to do something, without having to obey anyone/anything
* Freethought, a position that beliefs should be formed only on the basis of logic, reason, and empiricism
* Emancipate, to procur ...
in
). This notation admits certain conventional extensions:
is synonymous with
;
is defined as
, where
is an expression already defined.
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
fails to refer to anything in ''any'' set theory with classical logic; in
class
Class or The Class may refer to:
Common uses not otherwise categorized
* Class (biology), a taxonomic rank
* Class (knowledge representation), a collection of individuals or objects
* Class (philosophy), an analytical concept used differentl ...
theories like
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 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
In set theory, an ordinal number, or ordinal, is a generalization of ordinal numerals (first, second, th, etc.) aimed to extend enumeration to infinite sets.
A finite set can be enumerated by successively labeling each element with the least n ...
s) cannot be shown to exist in NFU. The usual definition of
in NFU is (in purely set theoretical language) the set of all infinite
well-ordering
In mathematics, a well-order (or well-ordering or well-order relation) on a set ''S'' is a total order on ''S'' with the property that every non-empty subset of ''S'' has a least element in this ordering. The set ''S'' together with the well-o ...
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
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
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
Zermelo set theory (sometimes denoted by Z-), as set out in a seminal paper in 1908 by Ernst Zermelo, is the ancestor of modern Zermelo–Fraenkel set theory (ZF) and its extensions, such as von Neumann–Bernays–Gödel set theory (NBG). It be ...
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
ur-elements yet to become members of a set, the
empty set
In mathematics, the empty set is the unique set having no elements; its size or cardinality (count of elements in a set) is zero. Some axiomatic set theories ensure that the empty set exists by including an axiom of empty set, while in other ...
is the unique ''set'' with no members:
:
For each object
, there is a set
with
as its only element:
:
For objects
and
, there is a set
containing
and
as its only elements:
:
The
union
Union commonly refers to:
* Trade union, an organization of workers
* Union (set theory), in mathematics, a fundamental operation on sets
Union may also refer to:
Arts and entertainment
Music
* Union (band), an American rock group
** ''Un ...
of two sets is defined in the usual way:
:
This is a recursive definition of unordered
-tuples for any concrete
(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
In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of pairing is one of the axioms of Zermelo–Fraenkel set theory. It was introduced by as a special case of his axiom of elementary se ...
, the existence of the empty set follows by
Separation from the existence of any set, and the binary union of two sets exists by the axioms of Pairing and
Union
Union commonly refers to:
* Trade union, an organization of workers
* Union (set theory), in mathematics, a fundamental operation on sets
Union may also refer to:
Arts and entertainment
Music
* Union (band), an American rock group
** ''Un ...
(
).
Ordered pair
First, consider the ordered pair. The reason that this comes first is technical: ordered pairs are needed to implement
relations and
functions, which are needed to implement other concepts which may seem to be prior.
The first definition of the ordered pair was the definition
proposed by
Norbert Wiener
Norbert Wiener (November 26, 1894 – March 18, 1964) was an American mathematician and philosopher. He was a professor of mathematics at the Massachusetts Institute of Technology (MIT). A child prodigy, Wiener later became an early researcher i ...
in 1914 in the context of the type theory of
Principia Mathematica
The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. ...
. Wiener observed that this allowed the elimination of types of ''n''-ary relations for ''n'' > 1 from the system of that work.
It is more usual now to use the definition
, due to
Kuratowski
Kazimierz Kuratowski (; 2 February 1896 – 18 June 1980) was a Polish mathematician and logician. He was one of the leading representatives of the Warsaw School of Mathematics.
Biography and studies
Kazimierz Kuratowski was born in Warsaw, (th ...
.
Either of these definitions works in either ZFC or 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
which is the same type as its
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
of ordered pair, the thing that matters is that it satisfies the defining condition
:
…and that it be reasonably easy to collect ordered pairs into sets.
Relations
Relations are sets whose members are all
ordered pair
In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In con ...
s. Where possible, a relation
(understood as a
binary predicate) is implemented as
(which may be written as
). When
is a relation, the notation
means
.
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
Proper may refer to:
Mathematics
* Proper map, in topology, a property of continuous function between topological spaces, if inverse images of compact subsets are compact
* Proper morphism, in algebraic geometry, an analogue of a proper map for ...
es). In NFU, some relations (such as the membership relation) are not sets because their definitions are not stratified: in
,
and
would
need to have the same type (because they appear as projections of the same pair), but also
successive types (because
is considered as an element of
).
Related definitions
Let
and
be given
binary relation
In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over Set (mathematics), sets and is a new set of ordered pairs consisting of ele ...
s. Then the following concepts are useful:
The
converse
Converse may refer to:
Mathematics and logic
* Converse (logic), the result of reversing the two parts of a definite or implicational statement
** Converse implication, the converse of a material implication
** Converse nonimplication, a logical c ...
of
is the relation
.
The domain of
is the set
.
The range of
is the domain of the converse of
. That is, the set
.
The field of
is the
union
Union commonly refers to:
* Trade union, an organization of workers
* Union (set theory), in mathematics, a fundamental operation on sets
Union may also refer to:
Arts and entertainment
Music
* Union (band), an American rock group
** ''Un ...
of the domain and range of
.
The
preimage
In mathematics, the image of a function is the set of all output values it may produce.
More generally, evaluating a given function f at each element of a given subset A of its domain produces a set, called the "image of A under (or through) ...
of a member
of the field of
is the set
(used in the definition of 'well-founded' below.)
The downward closure of a member
of the field of
is the smallest set
containing
, and containing each
for each
(i.e., including the preimage of each of its elements with respect to
as a subset.)
The
relative product
In the mathematics of binary relations, the composition of relations is the forming of a new binary relation from two given binary relations ''R'' and ''S''. In the calculus of relations, the composition of relations is called relative multiplic ...
of
and
is the relation
.
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
with codomain
as
, but our development will not require this.
In ZFC, any relation whose domain is a subset of a set
and whose range is a subset of a set
will be a set, since the
Cartesian product
In mathematics, specifically set theory, the Cartesian product of two sets ''A'' and ''B'', denoted ''A''×''B'', is the set of all ordered pairs where ''a'' is in ''A'' and ''b'' is in ''B''. In terms of set-builder notation, that is
: A\ti ...
is a set (being a subclass of
), and ''Separation'' provides for the existence of
. In NFU, some relations with global scope (such as equality and subset) can be implemented as sets. In NFU, bear in mind that
and
are three types lower than
in
(one type lower if a type-level ordered pair is used).
Properties and kinds of relations
A binary relation
is:
*
Reflexive if
for every
in the field of
.
*
Symmetric
Symmetry (from grc, συμμετρία "agreement in dimensions, due proportion, arrangement") in everyday language refers to a sense of harmonious and beautiful proportion and balance. In mathematics, "symmetry" has a more precise definiti ...
if
.
*
Transitive if
.
*
Antisymmetric if
.
*
Well-founded
In mathematics, a binary relation ''R'' is called well-founded (or wellfounded) on a class ''X'' if every non-empty subset ''S'' ⊆ ''X'' has a minimal element with respect to ''R'', that is, an element ''m'' not related by ''s& ...
if for every set
which meets the field of
,
whose preimage under
does not meet
.
* Extensional if for every
in the field of
,
if and only if
and
have the same preimage under
.
Relations having certain combinations of the above properties have standard names. A binary relation
is:
* An
equivalence relation
In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive. The equipollence relation between line segments in geometry is a common example of an equivalence relation.
Each equivalence relation ...
if
is reflexive, symmetric, and transitive.
* A
partial order
In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary ...
if
is reflexive, antisymmetric, and transitive.
* A
linear order
In mathematics, a total or linear order is a partial order in which any two elements are comparable. That is, a total order is a binary relation \leq on some set X, which satisfies the following for all a, b and c in X:
# a \leq a ( reflexive ...
if
is a partial order and for every
in the field of
, either
or
.
* A
well-ordering
In mathematics, a well-order (or well-ordering or well-order relation) on a set ''S'' is a total order on ''S'' with the property that every non-empty subset of ''S'' has a least element in this ordering. The set ''S'' together with the well-o ...
if
is a linear order and well-founded.
* A set picture if
is well-founded and extensional, and the field of
either equals the downward closure of one of its members (called its ''top element''), or is empty.
Functions
A functional relation is a
binary predicate such that
Such a
relation
Relation or relations may refer to:
General uses
*International relations, the study of interconnection of politics, economics, and law on a global level
*Interpersonal relationship, association or acquaintance between two or more people
*Public ...
(
predicate
Predicate or predication may refer to:
* Predicate (grammar), in linguistics
* Predication (philosophy)
* several closely related uses in mathematics and formal logic:
**Predicate (mathematical logic)
**Propositional function
**Finitary relation, o ...
) is implemented as a relation (set) exactly as described in the previous section. So the predicate
is implemented by the set
. A relation
is a function if and only if
It is therefore possible to define the value function
as the unique object
such that
– i.e.:
is
-related to
such that the relation
holds between
and
– or as the unique object
such that
. The presence in both theories of functional predicates which are not sets makes it useful to allow the notation
both for sets
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.
Outside of formal set theory, we usually specify a function in terms of its domain and codomain, as in the phrase "Let
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
to
if its domain equals
and its range ''is contained in''
. In this way, every function is a function from its domain to its range, and a function
from
to
is also a function from
to
for any set
containing
.
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
, where
is a functional relation and
is its codomain, but we do not take this approach in this article (more elegantly, if one first defines ordered triples - for example as
- then one could define a function as the ordered triple
so as to also include the domain). Note that the same issue exists for relations: outside of formal set theory we usually say "Let
be a binary relation", but formally
is a set of ordered pairs such that
and
.
In NFU,
has the same type as
, and
is three types higher than
(one type higher, if a type-level ordered pair is used). To solve this problem, one could define