The axioms in a finite axiomatization correspond to natural basic constructions, whereas stratified comprehension is powerful but not necessarily intuitive.
In his introductory book, Holmes opted to take the finite axiomatization as basic, and prove stratified comprehension as a theorem.
The axioms are then:[36] NF3 is the fragment of NF with full extensionality (no urelements) and those instances of comprehension which can be stratified using at most three types.
Relations and functions are defined in TST (and in NF and NFU) as sets of ordered pairs in the usual way.
However, Quine's definition relies on set operations on each of the elements a and b, and therefore does not directly work in NFU.
As an alternative approach, Holmes[3] takes the ordered pair (a, b) as a primitive notion, as well as its left and right projections
Fortunately, whether the ordered pair is type-level by definition or by assumption (i.e., taken as primitive) usually does not matter.
[37] It may intuitively seem that one should be able to prove Infinity in NF(U) by constructing any "externally" infinite sequence of sets, such as
NF may seem to run afoul of problems similar to those in naive set theory, but this is not the case.
is a syntactical sentence due to the conflation of all the types, but any general proof involving Comprehension is unlikely to work.
In NF, ordinals are defined (in the same way as in naive set theory) as equivalence classes of well-orderings under isomorphism.
Transfinite induction works on stratified statements, which allows one to prove that the natural ordering of ordinals (
Another (stratified) statement that can be proven by transfinite induction is that T is a strictly monotone (order-preserving) operation on the ordinals, i.e.,
A key issue was that Specker proved NF combined with the Axiom of Choice is inconsistent.
The proof can be formalized within Peano Arithmetic (PA), a theory weaker than ZF that most mathematicians accept without question.
Jensen's proof gives a fairly simple method for producing models of NFU in bulk.
Application of any power of j to both sides of an equation or membership statement preserves its truth value because j is an automorphism.
is a natural number n, one gets a model of NFU which claims that the universe is finite (it is externally infinite, of course).
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 the reasons for relying on it have to do with the intuition that ZFC is correct.
Willard Van Orman Quine first proposed NF as a way to avoid the "disagreeable consequences" of TST in a 1937 article titled New Foundations for Mathematical Logic; hence the name.
In the book, Quine introduced the system "Mathematical Logic" or "ML", an extension of NF that included proper classes as well as sets.
[44] Hao Wang showed how to amend Quine's axioms for ML so as to avoid this problem.
[38] In 1969, Jensen showed that adding urelements to NF yields a theory (NFU) that is provably consistent.
[46] Specker additionally showed that NF is equiconsistent with TST plus the axiom scheme of "typical ambiguity".
[citation needed] 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.
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.
Holmes has [date missing] shown that NFP has the same consistency strength as the predicative theory of types of Principia Mathematica without the axiom of reducibility.
[47] Since 2015, several candidate proofs by Randall Holmes of the consistency of NF relative to ZF were available both on arXiv and on the logician's home page.
His proofs were based on demonstrating the equiconsistency of a "weird" variant of TST, "tangled type theory with λ-types" (TTTλ), with NF, and then showing that TTTλ is consistent relative to ZF with atoms but without choice (ZFA) by constructing a class model of ZFA which includes "tangled webs of cardinals" in ZF with atoms and choice (ZFA+C).