The Consistency Problem and Related Partial Results
The outstanding problem with NF is that it is not known to be relatively consistent to any mainstream mathematical system. NF disproves Choice, and so proves Infinity (Specker, 1953). But it is also known (Jensen, 1969) that the minor(?) modification of allowing urelements (multiple distinct objects lacking members) yields NFU, a theory that is consistent relative to Peano arithmetic; if Infinity and Choice are added, the resulting theory has the same consistency strength as type theory with infinity or bounded Zermelo set theory. (NFU corresponds to a type theory TSTU, where type 0 has urelements, not just a single empty set.) There are other relatively consistent variants of NF.
NFU is, roughly speaking, weaker than NF because in NF, the power set of the universe is the universe itself, while in NFU, the power set of the universe may be strictly smaller than the universe (the power set of the universe contains only sets, while the universe may contain urelements). In fact, this is necessarily the case in NFU+"Choice".
Specker has shown that NF is equiconsistent with TST + Amb, where Amb is the axiom scheme of typical ambiguity which asserts 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 consistent. 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 attempts to alleviate this awkwardness), largely because there is no obvious definition for an ordered pair. Despite this awkwardness, 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 with the same theory. This does not hold for four types: 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.
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
Read more about this topic: New Foundations
Famous quotes containing the words consistency, problem, related, partial and/or results:
“All religions have honored the beggar. For he proves that in a matter at the same time as prosaic and holy, banal and regenerative as the giving of alms, intellect and morality, consistency and principles are miserably inadequate.”
—Walter Benjamin (1892–1940)
“In the nineteenth century the problem was that God is dead; in the twentieth century the problem is that man is dead.”
—Erich Fromm (1900–1980)
“Becoming responsible adults is no longer a matter of whether children hang up their pajamas or put dirty towels in the hamper, but whether they care about themselves and others—and whether they see everyday chores as related to how we treat this planet.”
—Eda Le Shan (20th century)
“There is no luck in literary reputation. They who make up the final verdict upon every book are not the partial and noisy readers of the hour when it appears; but a court as of angels, a public not to be bribed, not to be entreated, and not to be overawed, decides upon every man’s title to fame. Only those books come down which deserve to last.”
—Ralph Waldo Emerson (1803–1882)
“The chief benefit, which results from philosophy, arises in an indirect manner, and proceeds more from its secret, insensible influence, than from its immediate application.”
—David Hume (1711–1776)