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)
“The government is huge, stupid, greedy and makes nosy, officious and dangerous intrusions into the smallest corners of life—this much we can stand. But the real problem is that government is boring. We could cure or mitigate the other ills Washington visits on us if we could only bring ourselves to pay attention to Washington itself. But we cannot.”
—P.J. (Patrick Jake)
“So universal and widely related is any transcendent moral greatness, and so nearly identical with greatness everywhere and in every age,—as a pyramid contracts the nearer you approach its apex,—that, when I look over my commonplace-book of poetry, I find that the best of it is oftenest applicable, in part or wholly, to the case of Captain Brown.”
—Henry David Thoreau (1817–1862)
“You must not be partial in judging: hear out the small and the great alike; you shall not be intimidated by anyone, for the judgment is God’s.”
—Bible: Hebrew, Deuteronomy 1:17.
“We do not raise our children alone.... Our children are also raised by every peer, institution, and family with which they come in contact. Yet parents today expect to be blamed for whatever results occur with their children, and they expect to do their parenting alone.”
—Richard Louv (20th century)