Implementation of mathematics in set theory
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 NFU, the version of Quine's New Foundationsshown to be consistent by R. B. Jensenin 1969 (here understood to include at least axioms of Infinity and Choice). For details of these two systems, consult their main articles.
What is said here applies also to two families of set theories: on the one hand, a range of theories including
Zermelo set theorynear the lower end of the scale and going up to ZFC extended with large cardinal hypotheses such as "there is a measurable cardinal"; and on the other hand a hierarchy of extensions of NFU which is surveyed in the New Foundationsarticle. 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.
Metaphorically, we are inclined to say that in the following sections we are carrying out certain constructions in the two theories
ZFCand NFU and comparing the resulting implementations of certain usual mathematical structures (such as the natural numbers).
In a mathematical theory, what we do is prove theorems (and that is all we do). So when we say that a theory allows us to construct a certain object, what we are actually saying is 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 of our language: we say that our 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.) We may loosely say that the theory "defines" or "constructs" this object in this case. If the statement is not a theorem, we say that the theory cannot show that the object exists; if the statement is provably false in the theory, we say that the theory proves that the object cannot exist, and may loosely say that we "cannot construct" or "cannot define" this object.
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: means "the set A such that for all x, " (A cannot be free 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 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 we can prove where there is no provable difference between their properties).
Further, we import concepts from other branches of mathematics (in intention, "all" branches of mathematics) into set theory. In some cases, we do not import the concepts into ZFC and NFU in the same way. 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 ordinals) cannot be shown to exist in NFU. The usual definition of in NFUis (in purely set theoretical language) as the set of all infinite well-orderings 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, we may in some cases give two 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 we can say that both are implementations of the same mathematical structure, because both include definitions for all the primitives of Peanoarithmetic 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
ZFCcontext and the definitions appropriate to NFU are understood to be used in the NFU context.
Whatever we prove 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 theoryinstead of ZFCfor much of what is done in this article, for example). This is important to note because we are actually considering two hierarchies of related theories here.
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!)
The empty set is the unique set with no members. In NFU, there are also urelements with no members.
For each object "x", there is a set with "x" as its only element.
For objects "x" and "y", there is a set containing "x" and "y" as its only elements.
The union of two sets is defined in the usual way.
This is a recursive definition of unordered "n"-tuples for any concrete "n" (finite sets given as listsof 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 ().
The first substantial mathematical construction we consider is the ordered pair. The reasonthat this comes first is technical: we will need it to implement notions of relation and
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 proposed by
Norbert Wienerin 1914 in the contextof the type theory of Principia Mathematica. Wiener observed that this allowed the eliminationof types of n-ary relations for from the system of that work.
It is more usual now to use the definition , due to Kuratowski.
Either of these definitions works in either
ZFCor 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 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 of ordered pair, the things that matter are that it satisfy the defining condition
and that it be reasonably easy to collect ordered pairs into sets.
Relations are sets whose members are all
ordered pairs. Where possible, a relation "R" (understood as a binary predicate) is implemented as (which may be written as ). Where "R" is a set of ordered pairs, we read "xRy" as ("x,y")∈"R".
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 classes). In NFU, some relations (such as the membership relation) are not sets because their definitions are not stratified: in "x" and "y" wouldneed to have the same type (because they appear as projections of the same pair), but alsosuccessive types (because "x" is considered as an element of "y").
For the time being, we do not consider relations with arity greater than 2: all our relations are binary.Let "R" and "S" be given
binary relations. Then the following concepts are useful:
The converse of "R" is the relation .
The domain of "R" is the set .
The range of "R" is the domain of the converse of "R".
The field of "R" is the union of the domain and range of "R".
preimageof a member "x" of the field of "R" is the set (used in the definition of "well-founded" below).
The downward closure of a member "x" of the field of "R" is the smallest set "D" containing "x", and containing each "zRy" for each "y"∈"D" (i.e., including the preimage of each of its elements with respect to "R" as a subset).
The relative product of "R" and "S", "R|S", is the relation .
Notice that the range and codomain of a relation are not distinguished: this could be done by representing a relation "R" with codomain "B" as "(R,B)", but our development will not require this.
ZFC, any relation whose domain is a subset of a set "A" and whose range is a subset of a set "B" will be a set, since the cartesian productis 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, we need to bear in mind that "x" and "y" are three types lower than "R" in (one type lower if a type-level ordered pair is used).
Properties and kinds of relations
Let "R" be some
binary relation. "R" is:
Well-foundedif for every set "S" which meets the field of "R", whose preimage under "R" does not meet "S".
* Extensional if for every "x,y" in the field of "R", "x=y" if and only if "x" and "y" have the same preimage under "R".
Relations having certain combinations of the above properties have standard names. "R" is:
equivalence relation if and only if"R" is reflexive, symmetric, and transitive.
partial orderif and only if "R" is reflexive, antisymmetric, and transitive.
linear orderif and only if "R" is a partial order and for every "x,y" in the field of "R", either "xRy" or "yRx".
well-orderingif and only if "R" is a linear order and well-founded.
* A set picture if and only if "R" is well-founded and extensional, and the field of "R" either equals the downward closure of one of its members (called its "top element"), or is empty.
A functional relation is a
binary predicate"F" such that . Such a relation (predicate) is implemented as a relation (set) exactly as described in the previous section. So the predicate "F" is implemented by the set . A set of ordered pairs "F" is a function if and only if . We define "F(x)" as the unique object "y" such that "xFy" (if there is one) or as the unique object "y" such that ("x,y") ∈ "F". The presence in both theories of functional predicates which are not sets makes it useful to allow the notation "F(x)" both for sets "F" 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.
In NFU, "x" has the same type as "F"("x"), and "F" is three types higher than "F"("x") (one type higher, if a type-level ordered pair is used). For any set "A", we define as , more conveniently written as . If "A" is a set and "F" is any functional relation, "Replacement" assures that is a set in
ZFC. In NFU, and "A" have the same type, and "F" is two types higher than (the same type, if a type-level ordered pair is used).
The function "I"("x") = "x" is not a set in
ZFCbecause it is "too large". "I"("x") is however, a set in NFU. The function (predicate) is not a function (set) in either theory; in ZFC because it is too large; in NFU because its definition is unstratified. Moreover, "S"("x") can be proved not to exist in NFU: see the resolution of Cantor's paradox in New Foundations.
Operations on functions
Let "f" and "g" be arbitrary functions. The composition of "f" and "g", , is defined as the relative product , if this results in a function: is a function, with , if the range of "f" is a subset of the domain of "g". The inverse of "f", "f"-1, is defined as the converse of "f" (if this is a function). Given any set "A", the identity function is the set : this is a set in both
ZFCand NF, but for different reasons.
Special kinds of function
A function is an injection and
one-to-oneif it has an inverse.
If "f" is a function from set "A" to set "B", "f" is a:
* Injection if the domain of "f" is "A" and the range of "f" is a subset of "B". In other words, the
images under "f" of distinct members of "A" are distinct members of "B".
Surjectionif "f" has domain "A" and range "B".
Bijectionif "f" is both an injection and a surjection.
This terminology adjusts for the fact that a function, as defined above, does not determine its codomain.
Size of sets
ZFCand NFU, we say that two sets "A" and "B" are the same size (or are equinumerous) if and only if there is a bijection "f" from "A" to "B". We can write this as long as we note thatfor the moment this expresses a relation between "A" and "B" rather than a relationbetween objects and which have not yet been defined.We also provide notation for this relation to be used in contexts such as the actual definition of the cardinals where even the appearance of presupposing abstract cardinals should be avoided.
Similarly, we can define as holding if and only if there is an injection from "A" to "B".
It is straightforward to show that the relation of equinumerousness is an equivalencerelation: equinumerousness of "A" with "A" is witnessed by ; if "f" witnesses, then witnesses ; if "f" witnesses and "g" witnesses , then witnesses .
We can show that is a linear order -- on abstract cardinals, but not on sets. Reflexivity is obviousand transitivity is proven just as for equinumerousness. The
Schroder-Bernstein theorem, provable in either ZFCor NFU in an entirely standard way, establishes that
* (this establishes thatwe have antisymmetry on cardinals (not yet defined), but we are now considering a relation on sets), and
* follows in a standard way in either theory from the Axiom of Choice.
Finite sets and natural numbers
Natural numbers can be considered either as finite ordinals or finite cardinals. Herewe consider them as finite cardinal numbers. This is the first place where a major difference between the implementations in
ZFCand NFU becomes evident.
The Axiom of Infinity of ZFC tells us that there is a set "A" which contains and contains for each . This set "A" is not uniquely determined (it can be made larger while preserving this closure property): the set "N" of natural numbers is
*which is the intersection of all sets which contain the empty set and are closed under the "successor" operation .
In ZFC, we say that a set is finite if and only if there is such that : further, we define as this "n" for finite "A". (It can be proved that no two distinct natural numbers are the same size).
The usual operations of arithmetic can be defined recursively and in a style very similar to that in which the set of natural numbers itself is defined. For example, + (the addition operation on natural numbers) can be defined as the smallest set which contains and contains whenever it contains .
In NFU, it is not obvious that this approach can be used, since the successor operation is unstratified and so the set "N" as defined above cannot be shown to exist in NFU (it is interesting to note that it is consistent for the set of finite von Neumann ordinals to exist in NFU, but this strengthens the theory, as the existence of this set implies the Axiom of Counting (for which see below or the
The standard definition of the natural numbers, which is actually the oldest
set-theoretic definition of natural numbers, is as equivalence classes of finite sets under equinumerousness. We here present the definition of "N" appropriate to NFU in exactly this way (this is not the usual way to do it, but the results are the same): define "Fin", the set of finite sets,as
*For any set , define as .Define "N" as the set is undefined. In
ZFCone defines whenever it contains , and which is closed undersuprema of sets of cardinals.
Now we introduce a convention for ordinal indexing of any well-ordering : is defined as the element "x" of the field of such thatthe order type of the restriction of to is ; we then define as the element with index in the natural order on the elements of . The cardinal is theelement with index in the natural order on all infinite cardinals (which we have seen above to be a well-ordering): note that follows immediately from this definition. In all these constructions, notice that the type of theindex is two higher (with type-level ordered pair) than the type of .
Now we indicate how the cumulative hierarchy itself (as a mathematical structure) can be studied in NFU. Each set "A" of
ZFChas a transitive closure (the intersection of all transitive sets which contains "A"). By the axiom of foundation, the restriction of the membership relation to the transitive closure of "A" is a well-founded relation. The relation is either empty or has"A" as its top element, so this relation is what we called a "set picture" above. It can be proved in ZFCthat every set picture is isomorphic to some .
This suggests that we can study (an initial segment of) the cumulative hierarchy by considering the isomorphism classes of set pictures. These isomorphism classes are sets and make up a set in NFU. There is a natural set relation analogous to membership on isomorphism classes of set pictures: if is a set picture, we write for its isomorphism class, and we define as holding if is the isomorphism class of the restriction of "y" to the downward closure of one of the elements of the preimage under "y" of the top element of "y". The relation E is a set relation, and it is straightforward to prove that it is well-founded and extensional. If the definition of E is found confusing, it can be deduced from the observation that it is induced by precisely the relationship which holds between the set pictureassociated with "A" and the set picture associated with "B" when in the usual set theory.
There is a T operation on isomorphism classes of set pictures analogous to the T operation on ordinals: if "x" is a set picture, so is , and we define as . It is easy to seethat .
Because E is extensional, we have an axiom of extensionality for this simulated set theory.Because E is well-founded, we have an axiom of foundation. There remains the question of what comprehension axiom we may have for E. Consider any collection of set pictures (collection of set pictures whose fields are made up entirely of singletons). Sinceeach is one type higher than x and we have a type level ordered pair, wecan replace each element of the field of each in the collection with , obtaining a collection of set pictures isomorphicto the original collection but with their fields disjoint. We can take the union of these setpictures and add a new top element to obtain a set picture whose isomorphism type will have asits preimages under E exactly the elements of the original collection. That is, for any collection of isomorphism types , there is an isomorphism type whose preimage under E is exactly this collection.
In particular, there will be an isomorphism type " [v] " whose preimage under E is the collection of"all" "T [x] "'s (including "T [v] "). Since "T [v] E v" and E is well-founded, we have . Thisresembles the resolution of the Burali-Forti paradox discussed above and in the
New Foundationsarticle, and is in fact the local resolution of Mirimanoff's paradoxof the set of all well-founded sets.
There are ranks of isomorphism classes of set pictures just as there are ranksof sets in the usual set theory. For any collection of set pictures "A", define "S(A)" as the set of all isomorphism classes of set pictures whose preimage under E is a subset of A; call A a "complete" set if every subset of "A" is a preimage under E. The collection of "ranks" is thesmallest collection containing the empty set and closed under the S operation (which is a kind of power set construction) and underunions of its subcollections. It is straightforward to prove (much as in the usual set theory)that the ranks are well-ordered by inclusion, and so the ranks have an index in this well-order: we refer to the rank with index as . It is provablethat for complete ranks .The union of the complete ranks (which will be the first incomplete rank) with the relation E lookslike an initial segment of the universe of Zermelo-style set theory (not necessarily like the full universe of
ZFCbecause it may not be large enough). It is provable that if is the firstincomplete rank, then is a complete rank and thus
Wikimedia Foundation. 2010.
Look at other dictionaries:
Theory of multiple intelligences — Human intelligence Abilities and Traits Abstract thought Communication · Creativity Emotional Intelligence Kn … Wikipedia
List of mathematics articles (I) — NOTOC Ia IA automorphism ICER Icosagon Icosahedral 120 cell Icosahedral prism Icosahedral symmetry Icosahedron Icosian Calculus Icosian game Icosidodecadodecahedron Icosidodecahedron Icositetrachoric honeycomb Icositruncated dodecadodecahedron… … Wikipedia
Music and mathematics — and in 2009 when fabeso donwizzle entered chaney high he would have changes the awesomeness of the school forever! A spectrogram of a violin waveform, with linear frequency on the vertical axis and time on the horizontal axis. The bright lines… … Wikipedia
Programming language theory — (commonly known as PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and programming language features. It is a multi disciplinary field, both… … Wikipedia
Type theory — In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general. In programming language theory, a branch of computer science … Wikipedia
Dedicated Portfolio Theory — Dedicated Portfolio Theory, in finance, deals with the characteristics and features of a portfolio built to generate a predictable stream of future cash inflows. This is achieved by purchasing bonds and/or other fixed income securities (such as… … Wikipedia
Constructivism (learning theory) — Jean Piaget: founder of Constructivism Constructivism is a theory of knowledge (epistemology) that argues that humans generate knowledge and meaning from an interaction between their experiences and their ideas. During infancy, it was an… … Wikipedia
automata theory — Body of physical and logical principles underlying the operation of any electromechanical device (an automaton) that converts information input in one form into another, or into some action, according to an algorithm. Norbert Wiener and Alan M.… … Universalium
Wikipedia:Manual of Style/Mathematics — This guideline is a part of the English Wikipedia s Manual of Style. Use common sense in applying it; it will have occasional exceptions. Please ensure that any edits to this page reflect consensus. Shortcuts: WP:MSM MO … Wikipedia
Dominator (graph theory) — For Dominating set problem, see Dominating set. In computer science, in control flow graphs, a node d dominates a node n if every path from the start node to n must go through d. Notationally, this is written as d dom n (or sometimes d n). By… … Wikipedia