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:
“The lawyer’s truth is not Truth, but consistency or a consistent expediency.”
—Henry David Thoreau (1817–1862)
“It is commonplace that a problem stated is well on its way to solution, for statement of the nature of a problem signifies that the underlying quality is being transformed into determinate distinctions of terms and relations or has become an object of articulate thought.”
—John Dewey (1859–1952)
“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)
“We were soon in the smooth water of the Quakish Lake,... and we had our first, but a partial view of Ktaadn, its summit veiled in clouds, like a dark isthmus in that quarter, connecting the heavens with the earth.”
—Henry David Thoreau (1817–1862)
“There is not a single rule, however plausible, and however firmly grounded in epistemology, that is not violated at some time or other. It becomes evident that such violations are not accidental events, they are not results of insufficient knowledge or of inattention which might have been avoided. On the contrary, we see that they are necessary for progress.”
—Paul Feyerabend (1924–1994)