FACTOID # 8: Bookworms: Vermont has the highest number of high school teachers per capita and third highest number of librarians per capita.
 
 Home   Encyclopedia   Statistics   States A-Z   Flags   Maps   FAQ   About 
   
 
WHAT'S NEW
 

SEARCH ALL

FACTS & STATISTICS    Advanced view

Search encyclopedia, statistics and forums:

 

 

(* = Graphable)

 

 


Encyclopedia > 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 for Mathematical Logic"; hence the name. Much of this entry discusses NFU, an important variant of NF due to Jensen (1969) and exposited in Holmes (1998). Mathematical logic is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation as part of the foundations of mathematics. ... This article or section is in need of attention from an expert on the subject. ... Willard Van Orman Quine (June 25, 1908 – December 25, 2000), usually cited as W.V. Quine or W.V.O. Quine but known to his friends as Van, was one of the most influential American philosophers and logicians of the 20th century. ... At the broadest level, type theory is the branch of mathematics and logic that concerns itself with classifying entities into sets called types. ... The Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910-1913. ...

Contents


The type theory TST

The primitive predicates of TST, a streamlined version of the theory of types, are equality and membership. TST has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed. For each (meta-) natural number n, type n+1 objects are sets of type n objects; sets of type n have members of type n-1. Objects connected by identity must have the same type. The following two atomic formulas succinctly describe the typing rules: xn = yn and x^{n} in y^{n+1} (notation to be improved).


The axioms of TST are:

If φ(xn) is a formula, then the set {x^n mid phi(x^n)}^{n+1} exists.
In other words, given any formula φ(xn), the set An + 1 exists such that forall x^n exists A^{n+1} [x^n in A^{n+1} leftrightarrow phi(x^n)] comes out true.

This type theory is much less complicated than the one first set out in the Principia Mathematica, which included types for relations whose arguments were not necessarily all of the same type. In 1914, Norbert Wiener showed how to code the ordered pair as a set of sets, making it possible to eliminate relation types in favor of the linear hierarchy of sets described here. In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of extensionality, or axiom of extension, is one of the axioms of Zermelo-Fraenkel set theory. ... In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom schema of specification, or axiom schema of separation, or axiom schema of restricted comprehension, is a schema of axioms in Zermelo-Fraenkel set theory. ... In logic, WFF is an abbreviation for well-formed formula. ... The Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910-1913. ... Look up Relation in Wiktionary, the free dictionary In mathematics, a relation is a generalization of arithmetic relations, such as = and <, which occur in statements, such as 5 < 6 or 2 + 2 = 4. See relation (mathematics), binary relation (of set theory and logic) and relational algebra. ... Norbert Wiener Norbert Wiener (November 26, 1894 - March 18, 1964) was a U.S. mathematician and applied mathematician, especially in the field of electronics engineering. ... An ordered pair is a collection of two objects such that one can be distinguished as the first element and the other as the second element. ...


Quinian set theory

Axioms and stratification

New Foundations (NF) is obtained from TST by abandoning the distinctions of type. The axioms of NF are:

  • Extensionality: Two objects with the same elements are the same object;
  • A comprehension schema: All instances of TST Comprehension but with type indices dropped (and without introducing new identifications between variables).

By convention, NF's Comprehension schema is stated using the concept of stratified formula and making no direct reference to types. A formula φ is said to be stratified if there exists a function f from pieces of syntax to the natural numbers, such that for any atomic subformula x in y of φ we have f(y) = f(x) + 1, while for any atomic subformula x = y of φ, we have f(x) = f(y). Comprehension then becomes: In mathematics, this usually refers to some form of the principle, going back to Leibniz, that two mathematical objects are equal if there is no test to distinguish them. ... In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom schema of specification, or axiom schema of separation, or axiom schema of restricted comprehension, is a schema of axioms in Zermelo-Fraenkel set theory. ... In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom schema of specification, or axiom schema of separation, or axiom schema of restricted comprehension, is a schema of axioms in Zermelo-Fraenkel set theory. ... In mathematical logic, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretation of a logical theory exists. ... In mathematical logic, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretation of a logical theory exists. ... Look up Function in Wiktionary, the free dictionary. ...

{x mid phi } exists for each stratified formula φ.

Even the indirect reference to types implicit in the notion of stratification can be eliminated. Hailperin showed in 1944 that Comprehension is equivalent to a finite conjunction of its instances, so that NF can be finitely axiomatized without any reference to the notion of type. In mathematical logic, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretation of a logical theory exists. ... Stratification in mathematical logic In mathematical logic, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretation of a logical theory exists. ...


Comprehension may seem inconsistent with naive set theory, but this is not the case. For example, the impossible Russell class {x mid x notin x} is not an NF set, because x notin x cannot be stratified. In abstract mathematics, naive set theory1 was the first development of set theory, which was later to be framed more carefully as axiomatic set theory. ... Russells paradox (also known as Russells antinomy) is a paradox discovered by Bertrand Russell in 1901 which shows that the naive set theory of Frege is contradictory. ...


Ordered pairs

Relations and functions are defined in TST (and in NF and NFU) as sets of ordered pairs in the usual way. The usual definition of the ordered pair, first proposed by Kuratowski in 1921, has a serious drawback for NF and related theories: the resulting ordered pair necessarily has a type two higher than the type of its arguments (its left and right projections). Hence for purposes of determining stratification, a function is three types higher than the members of its field. Look up Relation in Wiktionary, the free dictionary In mathematics, a relation is a generalization of arithmetic relations, such as = and <, which occur in statements, such as 5 < 6 or 2 + 2 = 4. See relation (mathematics), binary relation (of set theory and logic) and relational algebra. ... Look up Function in Wiktionary, the free dictionary. ... An ordered pair is a collection of two objects such that one can be distinguished as the first element and the other as the second element. ... An ordered pair is a collection of two objects such that one can be distinguished as the first element and the other as the second element. ... Kazimierz Kuratowski (born February 2, 1896, Warsaw, died June 18, 1980, Warsaw) was a Polish mathematician. ... The word projection can mean more than one thing. ... Look up Function in Wiktionary, the free dictionary. ... Look up field in Wiktionary, the free dictionary A green field or paddock Field may refer to: A field is an open land area, used for growing agricultural crops. ...


If one can define a pair in such a way that its type is the same type as that of its arguments (resulting in a type-level ordered pair), then a relation or function is merely one type higher than the type of the members of its field. Hence NF and related theories usually employ Quine's set-theoretic definition of the ordered pair, which yields a type-level ordered pair of type. Holmes (1998) takes the ordered pair and its left and right projections as primitive. Fortunately, whether the ordered pair is type-level by definition or by assumption (i.e., taken as primitive), usually does not matter. Look up Relation in Wiktionary, the free dictionary In mathematics, a relation is a generalization of arithmetic relations, such as = and <, which occur in statements, such as 5 < 6 or 2 + 2 = 4. See relation (mathematics), binary relation (of set theory and logic) and relational algebra. ... Look up Function in Wiktionary, the free dictionary. ... Look up field in Wiktionary, the free dictionary A green field or paddock Field may refer to: A field is an open land area, used for growing agricultural crops. ... Willard Van Orman Quine (June 25, 1908 – December 25, 2000), usually cited as W.V. Quine or W.V.O. Quine but known to his friends as Van, was one of the most influential American philosophers and logicians of the 20th century. ... An ordered pair is a collection of two objects such that one can be distinguished as the first element and the other as the second element. ... The word projection can mean more than one thing. ...


The existence of a type-level ordered pair implies Infinity, and NFU + Infinity interprets NFU + "there is a type level ordered pair" (they are not quite the same theory, but the differences are inessential). Conversely, NFU + Infinity + Choice proves the existence of a type-level ordered pair.


Admissability of useful large sets

NF (and NFU + Infinity + Choice, described below and known consistent) allow the construction of two kinds of sets that ZFC and its proper extensions disallow because "too large" (some set theories admit these entities under the heading of proper classes): The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... In set theory and its applications throughout mathematics, a class is a collection of sets (or sometimes other mathematical objects) that can be unambiguously defined by a property that all its members share. ...

In mathematical logic, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretation of a logical theory exists. ... In mathematics, and particularly in applications to set theory and the foundations of mathematics, a universe or universal class (or if a set, universal set) is, roughly speaking, a class that is large enough to contain (in some sense) all of the sets that one may wish to use. ... The word complement (with an e in the second syllable, not to be confused with a different word, compliment with an i) has a number of uses. ... Wikibooks has more about Boolean logic, under the somewhat misleading title Boolean Algebra For a basic intro to sets, Boolean operations, Venn diagrams, truth tables, and Boolean applications, see Boolean logic. ... Begging the question, in modern popular usage, is often used synonymously for raising the question. However the original meaning is quite different: it described a type of logical fallacy (also called petitio principii) in which the evidence given for a proposition as much needs to be proved as the proposition... Friedrich Ludwig Gottlob Frege Friedrich Ludwig Gottlob Frege (November 8, 1848 - July 26, 1925) was a German mathematician, logician, and philosopher who is regarded as a founder of both modern mathematical logic and analytic philosophy. ... In linguistics, cardinal numbers is the name given to number words that are used for quantity (one, two, three), as opposed to ordinal numbers, words that are used for order (first, second, third). ... In mathematics, given a set X and an equivalence relation ~ on X, the equivalence class of an element a in X is the subset of all elements in X which are equivalent to a: [a] = { x ∈ X | x ~ a } The notion of equivalence classes is useful for constructing sets out... Look up Relation in Wiktionary, the free dictionary In mathematics, a relation is a generalization of arithmetic relations, such as = and <, which occur in statements, such as 5 < 6 or 2 + 2 = 4. See relation (mathematics), binary relation (of set theory and logic) and relational algebra. ... Two sets A and B are said to be equinumerous if they have the same cardinality, i. ... A bijective function. ... Commonly, ordinal numbers, or ordinals for short, are numbers used to denote the position in an ordered sequence: first, second, third, fourth, etc. ... In mathematics, given a set X and an equivalence relation ~ on X, the equivalence class of an element a in X is the subset of all elements in X which are equivalent to a: [a] = { x ∈ X | x ~ a } The notion of equivalence classes is useful for constructing sets out... In mathematics, a well-order (or well-ordering) 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. ... Several equivalence relations in mathematics are called similarity. ...

The consistency problem and related partial results

The outstanding problem with NF is that it is not known to be relatively consistent to anything. NF disproves Choice, and so proves Infinity (Specker, 1953). But it is also known (Jensen, 1969) that the minor(?) modification of allowing urelements (objects lacking members which are distinct from the empty set and from one another) yields NFU, a theory that is consistent relative to Peano arithmetic, with and without added Infinity and Choice. (NFU corresponds to a type theory TSTU, where positive types may contain urelements.) There are other consistent variants of NF. Ronald B.Jensen. ... Definition In set theory a ur-element is something which is not a set, but may itself be an element of a set. ... In mathematics, the Peano axioms (or Peano postulates) are a set of first-order axioms proposed by Giuseppe Peano which determine the theory of Peano arithmetic (also known as first-order arithmetic). ...


Specker has shown that NF is equiconsistent with TST + Amb, where Amb is the axiom scheme of typical ambiguity which asserts phi leftrightarrow phi^+ for any formula φ, φ + being the formula obtained by raising every type index in φ by one. NF is also equiconsistent with the theory TST augmented with a "type shifting automorphism", an operation which raises type by one, mapping each type onto the next higher type, and preserves equality and membership relations (and which cannot be used in instances of Comprehension: it is external to the theory). The same results hold for various fragments of TST in relation to the corresponding fragments of NF.


In the same year (1969) that Jensen proved NFU consistent, Grishin proved NF3 consistent. NF3 is the fragment of NF with full extensionality (no urelements) and those instances of Comprehension which can be stratified using just three types. This theory is a very awkward medium for mathematics (although there have been attemtps to alleviate this awkwardness), largely because there is no obvious definition for an ordered pair. Despite this awkwardness, NF3 is very interesting because every infinite model of TST restricted to three types satisfies Amb. Hence for every such model there is a model of NF3 with the same theory. This does not hold for four types: NF4 is the same theory as NF, and we have no idea how to obtain a model of TST with four types in which Amb holds. Ronald B.Jensen. ... An ordered pair is a collection of two objects such that one can be distinguished as the first element and the other as the second element. ...


In 1983, Marcel Crabbé proved consistent a system he called NFI, whose axioms are unrestricted extensionality and those instances of Comprehension in which no variable is assigned a type higher than that of the set asserted to exist. This is a predicativity restriction, though NFI is not a predicative theory: it admits enough impredicativity to define the set of natural numbers (defined as the intersection of all inductive sets; note that the inductive sets quantified over are of the same type as the set of natural numbers being defined). Crabbé also discussed a subtheory of NFI, in which only parameters (free variables) are allowed to have the type of the set asserted to exist by an instance of Comprehension. He called the result "predicative NF" (NFP); it is, of course, doubtful whether any theory with a self-membered universe is truly predicative. Holmes has <date?> shown that NFP has the same consistency strength as the predicative theory of types of Principia Mathematica without the Axiom of Reducibility. In mathematics, a predicate is a relation. ... The Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910-1913. ... Look up Reduction in Wiktionary, the free dictionary. ...


How NF(U) avoids the set-theoretic paradoxes

NF steers clear of the three well-known paradoxes of set theory. That NFU, a {relatively} consistent theory, also avoid the paradoxes increases our confidence in this fact. Robert Boyles self-flowing flask fills itself in this diagram, but perpetual motion machines cannot exist (according to our present understanding of physics). ... Set theory is the mathematical theory of sets, which represent collections of abstract objects. ... Consistency has three technical meanings: In mathematics and logic, as well as in theoretical physics, it refers to the proposition that a formal theory or a physical theory contains no contradictions. ...


The Russell paradox: An easy matter; x notin x is not a stratified formula, so the existence of {x mid x notin x} is not asserted by any instance of Comprehension. Quine presumably constructed NF with this paradox uppermost in mind. Russells paradox (also known as Russells antinomy) is a paradox discovered by Bertrand Russell in 1901 which shows that the naive set theory of Cantor and Frege is contradictory. ...


Cantor's paradox of the largest cardinal number exploits the application of Cantor's theorem to the universal set. Cantor's theorem says (given ZFC) that the power set P(A) of any set A is larger than A (there can be no injection (one-to-one map) from P(A) into A). Now of course there is an injection from P(V) into V, if V is the universal set! The resolution requires that we observe that | A | < | P(A) | makes no sense in the theory of types: the type of P(A) is one higher than the type of A. The correctly typed version (which is a theorem in the theory of types for essentially the same reasons that the original form of Cantor's theorem works in ZF) is | P1(A) | < | P(A) | , where P1(A) is the set of one-element subsets of A. The specific instance of this theorem that interests us is | P1(V) | < | P(V) | : there are fewer one-element sets than sets (and so fewer one-element sets than general objects, if we are in NFU). The "obvious" bijection x mapsto {x} from the universe to the one-element sets is not a set; it is not a set because its definition is unstratified. Note that in all known models of NFU it is the case that | P1(V) | < | P(V) | < < | V | ; Choice allows one not only to prove that there are urelements but that there are many cardinals between | P(V) | and | V | . Cantors paradox, also known as the paradox of the greatest cardinal, demonstrates that there is no cardinal greater than all other cardinals—that the class of cardinal numbers is infinite. ... In linguistics, cardinal numbers is the name given to number words that are used for quantity (one, two, three), as opposed to ordinal numbers, words that are used for order (first, second, third). ... In Zermelo-Fränkel set theory, Cantors theorem states that the power set (set of all subsets) of any set A has a strictly greater cardinality than that of A. Cantors theorem is obvious for finite sets, but surprisingly it holds true for infinite sets as well. ... In mathematics, and particularly in applications to set theory and the foundations of mathematics, a universe or universal class (or if a set, universal set) is, roughly speaking, a class that is large enough to contain (in some sense) all of the sets that one may wish to use. ... In Zermelo-Fränkel set theory, Cantors theorem states that the power set (set of all subsets) of any set A has a strictly greater cardinality than that of A. Cantors theorem is obvious for finite sets, but surprisingly it holds true for infinite sets as well. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... In mathematics, given a set S, the power set (or powerset) of S, written or 2S, is the set of all subsets of S. In axiomatic set theory (as developed e. ... Injection has multiple meanings: In mathematics, the term injection refers to an injective function. ... Injection has multiple meanings: In mathematics, the term injection refers to an injective function. ... In Zermelo-Fränkel set theory, Cantors theorem states that the power set (set of all subsets) of any set A has a strictly greater cardinality than that of A. Cantors theorem is obvious for finite sets, but surprisingly it holds true for infinite sets as well. ... ZF may refer to: The Zermelo-Fraenkel axioms, a system of axioms in mathematical set theory. ... A bijective function. ...


We now introduce some useful notions. A set A which satisfies the intuitively appealing | A | = | P1(A) | is said to be cantorian: a cantorian set satisfies the usual form of Cantor's theorem. A set A which satisfies the further condition that (x mapsto {x})lceil A, the restriction of the singleton map to A, is not only cantorian set but strongly cantorian. In Zermelo-Fränkel set theory, Cantors theorem states that the power set (set of all subsets) of any set A has a strictly greater cardinality than that of A. Cantors theorem is obvious for finite sets, but surprisingly it holds true for infinite sets as well. ... In mathematics, a function is a relation, such that each element of a set (the domain) is associated with a unique element of another (possibly the same) set (the codomain, not to be confused with the range). ... Generally, a singleton is something which exists alone in some way. ...


The Burali-Forti paradox of the largest ordinal number goes as follows. We define (following naive set theory) the ordinals as equivalence classes of well-orderings under similarity. There is an obvious natural well-ordering on the ordinals; since it is a well-ordering it belongs to an ordinal Ω. It is straightforward to prove (by transfinite induction) that the order type of the natural order on the ordinals less than a given ordinal α is α itself. But this means that Ω is the order type of the ordinals < Ω and so is strictly less than the order type of all the ordinals -- but the latter is, by definition, Ω itself! In set theory, a field of mathematics, the Burali-Forti paradox demonstrates that naïvely constructing the set of all ordinal numbers leads to a contradiction and therefore shows an antinomy in a system that allows its construction. ... Commonly, ordinal numbers, or ordinals for short, are numbers used to denote the position in an ordered sequence: first, second, third, fourth, etc. ... In abstract mathematics, naive set theory1 was the first development of set theory, which was later to be framed more carefully as axiomatic set theory. ... In mathematics, given a set X and an equivalence relation ~ on X, the equivalence class of an element a in X is the subset of all elements in X which are equivalent to a: [a] = { x ∈ X | x ~ a } The notion of equivalence classes is useful for constructing sets out... In mathematics, a well-order (or well-ordering) 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. ... Several equivalence relations in mathematics are called similarity. ... Ordinal numbers, or ordinals for short, are numbers used to denote the position in an ordered sequence: first, second, third, fourth, etc. ... Transfinite induction is the proof technique of mathematical induction when applied to (large) well-ordered sets, for instance to sets of ordinals or cardinals, or even to the class of all ordinals. ...


The solution to the paradox in NF(U) starts with the observation that the order type of the natural order on the ordinals less than α is of a higher type than α. Hence a type level ordered pair is two, and the usual Kuratowski ordered pair, four, types higher than the type of its arguments. For any order type α, we can define an order type α one type higher: if W in alpha, then T(α) is the order type of the order W^{iota} = {({x},{y}) mid xWy}. The triviality of the T operation is only a seeming one; it is easy to show that T is a strictly monotone (order preserving) operation on the ordinals. An ordered pair is a collection of two objects such that one can be distinguished as the first element and the other as the second element. ... Monotone refers to one of: a steady chant like way of speaking on one pitch, or a monotonic function Monotone Records, a record label [1] Monotone (software), revision control software [2] This is a disambiguation page: a list of articles associated with the same title. ...


We can now restate the lemma on order types in a stratified manner: the order type of the natural order on the ordinals < α is T2(α) or T4(α) depending on which pair is used (we assume the type level pair hereinafter). From this we deduce that the order type on the ordinals < Ω is T2(Ω), from which we deduce T2(Ω) < Ω. Hence the T operation is not a function; we cannot have a strictly monotone set map from ordinals to ordinals which sends an ordinal downward! Since T is monotone, we have Omega > T^2(Omega) > T^4(Omega)ldots, a "descending sequence" in the ordinals which cannot be a set. Monotone refers to one of: a steady chant like way of speaking on one pitch, or a monotonic function Monotone Records, a record label [1] Monotone (software), revision control software [2] This is a disambiguation page: a list of articles associated with the same title. ...


Some have asserted that this result shows that no model of NF(U) is "standard", since the ordinals in any model of NFU are externally not well-ordered. We do not take a position on this, but we note that it is also a theorem of NFU that any set model of NFU has non-well-ordered "ordinals"; NFU does not conclude that the universe V is a model of NFU, despite V being a set, because the membership relation is not a set relation.


For a further development of mathematics in NFU, with a comparison to the development of the same in ZFC, see implementation of mathematics in set theory. NFU is a TLA which may stand for: National Farmers Union New Foundations with Urelements This is a disambiguation page — a list of articles associated with the same title. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... This article examines the implementation of mathematical concepts in set theory. ...


The set theory of the 1940 first edition of Quine's Mathematical Logic married NF to the proper classes of NBG set theory, and included an axiom schema of unrestricted comprehension for proper classes. In 1942, J. Barkley Rosser proved that Quine's set theory was subject to the Burali-Forti paradox. Rosser's proof does not go through for NF(U). In 1950, Hao Wang showed how to amend Quine's axioms so as to avoid this problem, and Quine included the resulting axiomatization in the 1951 second and final edition of Mathematical Logic. In computing, a quine is a program (a form of metaprogram) that produces its complete source code as its only output. ... In set theory and its applications throughout mathematics, a class is a collection of sets (or sometimes other mathematical objects) that can be unambiguously defined by a property that all its members share. ... In foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiom system for set theory designed to yield the same results as Zermelo-Fraenkel set theory, together with the axiom of choice (ZFC), but with only a finite number of axioms, that is without axiom schemas. ... John Barkley Rosser Sr. ... Hao Wang 王浩 (1921 – 1995) was a Chinese-American logician, philosopher and mathematician. ...


Models of NFU

There is a fairly simple method for producing models of NFU in bulk. Using well-known techniques of model theory, one can construct a nonstandard model of Zermelo set theory (nothing nearly as strong as full ZFC is needed for the basic technique) on which there is an external automorphism j (not a set of the model) which moves a rank Vα of the cumulative hierarchy of sets. We may suppose without loss of generality that j(α) < α. We talk about the automorphism moving the rank rather than the ordinal because we do not want to assume that every ordinal in the model is the index of a rank. In mathematics, model theory is the study of the representation of mathematical concepts in terms of set theory, or the study of the models which underlie mathematical systems. ... Zermelo set theory, as set out in an important paper in 1908 by Ernst Zermelo, is the ancestor of modern set theory. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... In mathematical set theory, the rank of a set is recursively defined as the smallest ordinal number greater than the rank of any member of the set. ... For the various types of hierarchy, see hierarchy (disambiguation) A hierarchy (in Greek: Ιεραρχία, it is derived from ιερός-hieros, sacred, and άρχω-arkho, rule) is a system of ranking and organizing things or people, where each element of the system (except for the top element) is subordinate to a single other element. ... In mathematics, an automorphism is an isomorphism from a mathematical object to itself. ...


The domain of the model of NFU will be the nonstandard rank Vα. The membership relation of the model of NFU will be

  • x in_{NFU} y equiv_{def} j(x) in y wedge y in V_{j(alpha)+1}.

We now prove that this actually is a model of NFU. Let φ be a stratified formula in the language of NFU. Choose an assignment of types to all variables in the formula which witnesses the fact that it is stratified. Choose a natural number N greater than all types assigned to variables by this stratification.


Expand the formula φ into a formula φ1 in the language of the nonstandard model of Zermelo set theory with automorphism j using the definition of membership in the model of NFU. Application of any power of j to both sides of an equation or membership statement preserves its truth value because j is an automorphism. Make such an application to each atomic formula in φ1 in such a way that each variable x assigned type i occurs with exactly Ni applications of j. This is possible thanks to the form of the atomic membership statements derived from NFU membership statements, and to the formula being stratified. Each quantified sentence (forall x in V_{alpha}.psi(j^{N-i}(x))) can be converted to the form (forall x in j^{N-i}(V_{alpha}).psi(x)) (and similarly for existential quantifiers). Carry out this transformation everywhere and obtain a formula φ2 in which j is never applied to a bound variable. Zermelo set theory, as set out in an important paper in 1908 by Ernst Zermelo, is the ancestor of modern set theory. ... In mathematics, an automorphism is an isomorphism from a mathematical object to itself. ... In mathematical logic, an atomic formula, or atom, is a formula that has no subformulas. ... In predicate logic, existential quantification is an attempt to formalize the notion that something (a logical predicate) is true for something, or at least one relevant thing. ...


Choose any free variable y in φ assigned type i. Apply jiN uniformly to the entire formula to obtain a formula φ3 in which y appears without any application of j. Now {y in V_{alpha} mid phi_3} exists (because j appears applied only to free variables and constants), belongs to Vα + 1, and contains exactly those y which satisfy the original formula φ in the model of NFU. j({y in V_{alpha} mid phi_3}) has this extension in the model of NFU (the application of j corrects for the different definition of membership in the model of NFU). This establishes that Stratified Comprehension holds in the model of NFU.


To see that weak Extensionality holds is straightforward: each nonempty element of Vj(α) + 1 inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements.


The basic idea is that the automorphism j codes the "power set" Vα + 1 of our "universe" Vα into its externally isomorphic copy Vj(α) + 1 inside our "universe." The remaining objects not coding subsets of the universe are treated as urelements. Definition In set theory a ur-element is something which is not a set, but may itself be an element of a set. ...


If α is a natural number n, we get a model of NFU which claims that the universe is finite (it is externally infinite, of course). If α is infinite and the Choice holds in the nonstandard model of ZFC, we obtain a model of NFU + Infinity + Choice. In mathematics, the axiom of choice, or AC, is an axiom of set theory. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...


Self-sufficiency of mathematical foundations in NFU

For philosophical reasons, it is important to note that it is not necessary to work in ZFC or any related system to carry out this proof. A common argument against the use of NFU as a foundation for mathematics is that our reasons for relying on it have to do with our intuition that ZFC is correct. We claim that it is sufficient to accept TST (in fact TSTU). We outline the approach: take the type theory TSTU (allowing urelements in each positive type) as our metatheory and consider the theory of set models of TSTU in TSTU (these models will be sequences of sets Ti (all of the same type in the metatheory) with embeddings of each P(Ti) into P1(Ti + 1) coding embeddings of the power set of Ti into
Ti + 1 in a type-respecting manner). Given an embedding of T0 into T1 (identifying elements of the base "type" with subsets of the base type), one can define embeddings from each "type" into its successor in a natural way. This can be generalized to transfinite sequences Tα with care. The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...


Note that the construction of such sequences of sets is limited by the size of the type in which they are being constructed; this prevents TSTU from proving its own consistency (TSTU + Infinity can prove the consistency of TSTU; to prove the consistency of TSTU+Infinity one needs a type containing a set of cardinality beth_{omega}, which cannot be proved to exist in TSTU+Infinity without stronger assumptions). Now the same results of model theory can be used to build a model of NFU and verify that it is a model of NFU in much the same way, with the Tα's being used in place of Vα in the usual construction. The final move is to observe that since NFU is consistent, we can drop the use of absolute types in our metatheory, bootstrapping the metatheory from TSTU to NFU.


Facts about the automorphism j

The automorphism j of a model of this kind is closely related to certain natural operations in NFU. For example, if W is a well-ordering in the nonstandard model (we suppose here that we use Kuratowski pairs so that the coding of functions in the two theories will agree to some extent) which is also a well-ordering in NFU (all well-orderings of NFU are well-orderings in the nonstandard model of Zermelo set theory, but not vice versa, due to the formation of urelements in the construction of the model), and W has type α in NFU, then j(W) will be a well-ordering of type T(α) in NFU. In mathematics, an automorphism is an isomorphism from a mathematical object to itself. ... In mathematics, an automorphism is an isomorphism from a mathematical object to itself. ... In mathematics, a well-order (or well-ordering) 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. ... An ordered pair is a collection of two objects such that one can be distinguished as the first element and the other as the second element. ... Definition In set theory a ur-element is something which is not a set, but may itself be an element of a set. ...


In fact, j is coded by a function in the model of NFU. The function in the nonstandard model which sends the singleton of any element of Vj(α) to its sole element, becomes in NFU a function which sends each singleton {x}, where x is any object in the universe, to j(x). Call this function Endo and let it have the following properties: Endo is an injection from the set of singletons into the set of sets, with the property that Endo( {x} ) = {Endo( {y} ) | yx} for each set x. This function can define a type level "membership" relation on the universe, one reproducing the membership relation of the original nonstandard model. Injection has multiple meanings: In mathematics, the term injection refers to an injective function. ...


Strong axioms of Infinity

In this section we mainly discuss the effect of adding various "strong axioms of infinity" to our usual base theory, NFU + Infinity + Choice. This base theory, known consistent, has the same strength as TST + Infinity, or Zermelo set theory with Separation restricted to bounded formulas (Mac Lane set theory).


One can add to this base theory strong axioms of infinity familar from the ZFC context, such as "there exits an inaccessible cardinal," but it is more natural to consider assertions about cantorian and strongly cantorian sets. Such assertions not only bring into being large cardinals of the usual sorts, but strengthen the theory on its own terms. The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... In mathematics, a cardinal is called a large cardinal if it belongs to a class of cardinals, the existence of which provably cannot be proved within the standard axiomatic set theory ZFC, if one assumes ZFC itself is consistent. ...


The weakest of the usual strong principles is:

  • Rosser's Axiom of Counting. The set of natural numbers is a strongly cantorian set.

To see how natural numbers are defined in NFU, see set-theoretic definition of natural numbers. The original form of this axiom given by Rosser was "the set {m|1≤mn} has n members", for each natural number n". This intuitively obvious assertion is unstratified: what is provable in NFU is "the set {m|1≤mn} has T2(n) members" (where the T operation on cardinals is defined by T( | A | ) = | P1(A) | ; this raises the type of a cardinal by one). For any cardinal number (including natural numbers) to assert T( | A | ) = | A | is equivalent to asserting that the sets A of that cardinality are cantorian (by a usual abuse of language, we refer to such cardinals as "cantorian cardinals"). It is straightforward to show that the assertion that each natural number is cantorian is equivalent to the assertion that the set of all natural numbers is strongly cantorian. Several ways have been proposed to define the natural numbers using set theory. ...


Counting is consistent with NFU, but increases its consistency strength noticeably; not, as one would expect, in the area of arithmetic, but in higher set theory. NFU + Infinity proves that each beth_n exists, but not that beth_{omega} exists; NFU + Counting (easily) proves Infinity, and further proves the existence of beth_{beth_n} for each n, but not the existence of beth_{beth_{omega}}. (See beth numbers). In mathematics, the Hebrew letter (aleph) with various subscripts represents various infinite cardinal numbers (see aleph number). ...


Counting implies immediately that one does not need to assign types to variables restricted to the set N of natural numbers for purposes of stratification; it is a theorem that the power set of a strongly cantorian set is strongly cantorian, so it is further not necessary to assign types to variables restricted to any iterated power set of the natural numbers, or to such familiar sets as the set of real numbers, the set of functions from reals to reals, and so forth. The set-theoretical strength of Counting is less important in practice than the convenience of not having to annotate variables known to have natural number values (or related kinds of values) with singleton brackets, or to apply the T operation in order to get stratified set definitions. In mathematics, given a set S, the power set (or powerset) of S, written or 2S, is the set of all subsets of S. In axiomatic set theory (as developed e. ...


Counting implies Infinity; each of the axioms below needs to be adjoined to NFU + Infinity to get the effect of strong variants of Infinity; Ali Enayat has investigated the strength of some of these axioms in models of NFU + "the universe is finite".


A model of the kind constructed above satisfies Counting just in case the automorphism j fixes all natural numbers in the underlying nonstandard model of Zermelo set theory.


The next strong axiom we consider is the

  • Axiom of strongly cantorian separation: For any strongly cantorian set A and any formula φ (not necessarily stratified!) the set {xA|φ} exists.

Immediate consequences include Mathematical Induction for unstratified conditions (which is not a consequence of Counting; many but not all unstratified instances of induction on the natural numbers follow from Counting).


This axiom is surprisingly strong. Unpublished work of Robert Solovay shows that the consistency strength of the theory NFU* = NFU + Counting + Strongly Cantorian Separation is the same as that of Zermelo set theory + Σ2 Replacement. Robert M. Solovay is a set theorist who spent many years as a professor at UC Berkeley. ...


This axiom holds in a model of the kind constructed above (with Choice) if the ordinals which are fixed by j and dominate only ordinals fixed by j in the underlying nonstandard model of Zermelo set theory are standard, and the power set of any such ordinal in the model is also standard. This condition is sufficient but not necessary.


Next is

  • Axiom of Cantorian Sets: Every cantorian set is strongly cantorian.

This very simple and appealing assertion is extremely strong. Solovay has shown the precise equivalence of the consistency strength of the theory NFUA = NFU + Infinity + Cantorian Sets with that of ZFC + a schema asserting the existence of an n-Mahlo cardinal for each concrete natural number n. Ali Enayat has shown that the theory of cantorian equivalence classes of well-founded extensional relations (which gives a natural picture of an initial segment of the cumulative hierarchy of ZFC) interprets the extension of ZFC with n-Mahlo cardinals directly. A permutation technique can be applied to a model of this theory to give a model in which the hereditarily strongly cantorian sets with the usual membership relation model the strong extension of ZFC. The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...


This axiom holds in a model of the kind constructed above (with Choice) just in case the ordinals fixed by j in the underlying nonstandard model of ZFC are an initial (proper class) segment of the ordinals of the model. The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...


Next consider the

  • Axiom of Cantorian Separation: For any cantorian set A and any formula φ (not necessarily stratified!) the set {xA|φ} exists.

This combines the effect of the two preceding axioms and is actually even stronger (precisely how is not known). Unstratified mathematical induction enables proving that there are n-Mahlo cardinals for every n, given Cantorian Sets, which gives an extension of ZFC that is even stronger than the previous one, which only asserts that there are n-Mahlos for each concrete natural number (leaving open the possibility of nonstandard counterexamples). The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...


This axiom will hold in a model of the kind described above if every ordinal fixed by j is standard, and every power set of an ordinal fixed by j is also standard in the underlying model of ZFC. Again, this condition is sufficient but not necessary. In mathematics, given a set S, the power set (or powerset) of S, written or 2S, is the set of all subsets of S. In axiomatic set theory (as developed e. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...


An ordinal is said to be cantorian if it is fixed by T, and strongly cantorian if it dominates only cantorian ordinals (this implies that it is itself cantorian). In models of the kind constructed above, cantorian ordinals of NFU correspond to ordinals fixed by j (they are not the same objects because different definitions of ordinal numbers are used in the two theories).


Equal in strength to Cantorian Sets is the

  • Axiom of Large Ordinals: For each noncantorian ordinal α, there is a natural number n such that Tn(Ω) < α.

Recall that Ω is the order type of the natural order on all ordinals. This only implies Cantorian Sets if we have Choice (but is at that level of consistency strength in any case). It is remarkable that one can even define Tn(Ω): this is the nth term sn of any finite sequence of ordinals s of length n such that s0 = Ω, si + 1 = T(si) for each appropriate i. This definition is completely unstratified. The uniqueness of Tn(Ω) can be proved (for those n for which it exists) and a certain amount of common-sense reasoning about this notion can be carried out, enough to show that Large Ordinals implies Cantorian Sets in the presence of Choice. In spite of the knotty formal statement of this axiom, it is a very natural assumption, amounting to making the action of T on the ordinals as simple as possible.


A model of the kind constructed above will satisfy Large Ordinals, if the ordinals moved by j are exactly the ordinals which dominate some j i(α) in the underlying nonstandard model of ZFC. The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...

  • Axiom of Small Ordinals: For any formula φ, there is a set A such that the elements of A which are strongly cantorian ordinals are exactly the strongly cantorian ordinals such that φ.

Solovay has shown the precise equivalence in consistency strength of NFUB = NFU + Infinity + Cantorian Sets + Small Ordinals with Kelley-Morse set theory plus the assertion that the proper class ordinal (the class of all ordinals) is a weakly compact cardinal. This is very strong indeed! Moreover, NFUB-, which is NFUB with Cantorian Sets omitted, is easily seen to have the same strength as NFUB. Morse-Kelley set theory or Kelley-Morse set theory (MK or KM) is a set theory with proper classes properly extending the usual set theory ZF. It is a first order theory (though it can be confused with second-order ZF). ... In mathematics, a weakly compact cardinal is a certain kind of cardinal number; weakly compact cardinals are large cardinals, meaning that their existence can neither be proven nor disproven from the standard axioms of set theory. ...


A model of the kind constructed above will satisfy this axiom if every collection of ordinals fixed by j is the intersection of some set of ordinals with the ordinals fixed by j, in the underlying nonstandard model of ZFC. The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...


Even stronger is the theory NFUM = NFU + Infinity + Large Ordinals + Small Ordinals. This is equivalent to Kelley-Morse set theory with a predicate on the classes which is a κ-complete nonprincipal ultrafilter on the proper class ordinal κ; in effect, this is Kelley-Morse set theory + "the proper class ordinal is a measurable cardinal"! Morse-Kelley set theory or Kelley-Morse set theory (MK or KM) is a set theory with proper classes properly extending the usual set theory ZF. It is a first order theory (though it can be confused with second-order ZF). ... In mathematics, especially in order theory, an ultrafilter is a subset of a partially ordered set (a poset) which is maximal among all proper filters. ... Morse-Kelley set theory or Kelley-Morse set theory (MK or KM) is a set theory with proper classes properly extending the usual set theory ZF. It is a first order theory (though it can be confused with second-order ZF). ... Bold textcopper mellon pressure washer. ...


The technical details here are not the main point, which is that reasonable and natural (in the context of NFU) assertions turn out to be equivalent in power to very strong axioms of infinity in the ZFC context. This fact is related to the correlation between the existence of models of NFU, described above and satisfying these axioms, and the existence of models of ZFC with automorphisms having special properties. The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... In mathematics, an automorphism is an isomorphism from a mathematical object to itself. ...


See also

This article or section is in need of attention from an expert on the subject. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ... This article examines the implementation of mathematical concepts in set theory. ... Several ways have been proposed to define the natural numbers using set theory. ... In mathematical logic, positive set theory is an alternative set theory consisting of the following axioms: The axiom of extensionality: . The axiom of infinity: the von Neumann ordinal exists. ... An alternative set theory is an alternative mathematical approach to the concept of set. ...

References

  • Holmes, Randall, 1998. Elementary Set Theory with a Universal Set. Academia-Bruylant. The publisher has graciously consented to permit diffusion of this introduction to NFU via the web. Copyright is reserved.
  • Jensen, R. B., 1969, "On the Consistency of a Slight(?) Modification of Quine's NF," Synthese 19: 250-63. With discussion by Quine.
  • Quine, W. V., 1980, "New Foundations for Mathematical Logic" in From a Logical Point of View, 2nd ed., revised. Harvard Univ. Press: 80-101. The definitive version of where it all began, namely Quine's 1937 paper in the American Mathematical Monthly.

Ronald B.Jensen. ... W. V. Quine Willard Van Orman Quine (June 25, 1908 - December 25, 2000) was one of the most influential American philosophers and logicians of the 20th century. ...

External links


  Results from FactBites:
 
New Foundations - definition of New Foundations in Encyclopedia (692 words)
In mathematical logic, the New Foundations (NF) of W.
New Foundations (NF) is obtained from this theory by abandoning the distinctions of type.
The axioms of this theory are extensionality (two objects with the same elements are the same object) and all those instances of comprehension obtained by dropping type indices (without introducing new identifications between variables) from an instance of comprehension of the streamlined type theory.
SECF.org (2108 words)
Foundation leaders were also requested to send their most recent annual report, grantmaking guidelines, and any other important materials to SECF for review.
The new foundations were created in a wide variety of ways, including lease agreements, merger partnerships, joint venture arrangements, and a simple spin-off of the original hospital foundation in a nonprofit-to-nonprofit conversion.
Foundation leaders stated that they are actively seeking advice and information about how grant recipients can make their programs sustainable after the grant period ends.
  More results at FactBites »

 
 

COMMENTARY     


Share your thoughts, questions and commentary here
Your name
Your comments

Want to know more?
Search encyclopedia, statistics and forums:

 


Press Releases |  Feeds | Contact
The Wikipedia article included on this page is licensed under the GFDL.
Images may be subject to relevant owners' copyright.
All other elements are (c) copyright NationMaster.com 2003-5. All Rights Reserved.
Usage implies agreement with terms, 1022, m