Editing New Foundations (section)

== Consistency ==

Some mathematicians had questioned the [[consistency]] of NF, partly because it is not clear why it avoids the known paradoxes. A key issue was that Specker proved NF combined with the [[Axiom of Choice]] is inconsistent. The proof is complex and involves T-operations. However, since 2010, Holmes has claimed to have shown that NF is consistent relative to the consistency of standard set theory (ZFC). In 2024, Sky Wilshaw confirmed Holmes' proof using the [[Lean (proof assistant)|Lean proof assistant]].<ref>{{cite web |last1=Smith |first1=Peter |title=NF really is consistent |url=https://www.logicmatters.net/2024/04/21/nf-really-is-consistent/ |website=Logic Matters |date=21 April 2024 |access-date=21 April 2024}}</ref>

Although NFU resolves the paradoxes similarly to NF, it has a much simpler consistency proof. The proof can be formalized within [[Peano Arithmetic]] (PA), a theory weaker than ZF that most mathematicians accept without question. This does not conflict with [[Gödel's second incompleteness theorem]] because NFU does not include the [[Axiom of Infinity]] and therefore PA cannot be modeled in NFU, avoiding a contradiction. PA also proves that NFU with Infinity and NFU with both Infinity and Choice  are [[equiconsistent]] with TST with Infinity and TST with both Infinity and Choice, respectively. Therefore, a stronger theory like ZFC, which proves the consistency of TST, will also prove the consistency of NFU with these additions.{{sfn|Jensen|1969}} In simpler terms, NFU is generally seen as weaker than NF because, in NFU, the collection of all sets (the power set of the universe) can be smaller than the universe itself, especially when urelements are included, as required by NFU with Choice.

=== Models of NFU ===
<!-- Where the starting point for the [[metamathematics]] of [[Zermelo–Fraenkel set theory|Zermelo-Fraenkel set theory]] is the easy-to-formalize intuition of the [[cumulative hierarchy]], the non-well-foundedness of NF and NFU makes this intuition not directly applicable. However, the intuition of forming sets at a stage from sets developed at earlier stages can be augmented to allow forming sets at a stage consisting of all possible sets but given sets formed at earlier stages, giving an analogous iterative conception of set.{{sfn|Forster|2008}}{{Specify|reason=Does this actually give a model for NFU? The cited paper only gives a model for NF_2, a significantly simpler theory.|date=July 2023}} -->

Jensen's proof gives 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 (set theory)|rank]] <math>V_{\alpha}</math><ref group="note">We talk about the automorphism moving the rank <math>V_{\alpha}</math> rather than the ordinal <math>\alpha</math> because we do not want to assume that every ordinal in the model is the index of a rank.</ref> of the [[cumulative hierarchy]] of sets.  We may suppose without loss of generality that <math>j(\alpha)<\alpha</math>.

The domain of the model of NFU will be the nonstandard rank <math>V_{\alpha}</math>. The basic idea is that the automorphism ''j'' codes the "power set" <math>V_{\alpha+1}</math> of our "universe" <math>V_{\alpha}</math> into its externally isomorphic copy <math>V_{j(\alpha)+1}</math> inside our "universe." The remaining objects not coding subsets of the universe are treated as [[urelement]]s. Formally, the membership relation of the model of NFU will be <math>x \in_{NFU} y \equiv_{def} j(x) \in y \wedge y \in V_{j(\alpha)+1}.</math>

It may now be proved that this actually is a model of NFU. Let <math>\phi</math> 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 <math>\phi</math> into a formula <math>\phi_1</math> 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 <math>\phi_1</math> in such a way that each variable ''x'' assigned type ''i'' occurs with exactly <math>N-i</math> 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 <math>(\forall x \in V_{\alpha}.\psi(j^{N-i}(x)))</math> can be converted to the form <math>(\forall x \in j^{N-i}(V_{\alpha}).\psi(x))</math> (and similarly for [[existential quantifier]]s). Carry out this transformation everywhere and obtain a formula <math>\phi_2</math> in which ''j'' is never applied to a bound variable. Choose any free variable ''y'' in <math>\phi</math> assigned type ''i''. Apply <math>j^{i-N}</math> uniformly to the entire formula to obtain a formula <math>\phi_3</math> in which ''y'' appears without any application of ''j''. Now <math>\{y \in V_{\alpha} \mid \phi_3\}</math> exists (because ''j'' appears applied only to free variables and constants), belongs to <math>V_{\alpha+1}</math>, and contains exactly those ''y'' which satisfy the original formula
<math>\phi</math> in the model of NFU. <math>j(\{y \in V_{\alpha} \mid \phi_3\})</math> 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 <math>V_{j(\alpha)+1}</math> inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements.

If <math>\alpha</math> is a natural number ''n'', one gets a model of NFU which claims that the universe is finite (it is externally infinite, of course). If <math>\alpha</math> is infinite and the ''[[Axiom of Choice|Choice]]'' holds in the nonstandard model of ZFC, one obtains a model of NFU + ''Infinity'' + ''Choice''.

=== 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 the reasons for relying on it have to do with the intuition that ZFC is correct. It is sufficient to accept TST (in fact TSTU). In outline: take the type theory TSTU (allowing urelements in each positive type) as a metatheory and consider the theory of set models of TSTU in TSTU (these models will be sequences of sets <math>T_i</math> (all of the same type in the metatheory) with embeddings of each <math>P(T_i)</math> into <math>P_1(T_{i+1})</math> coding embeddings of the power set of <math>T_i</math> into <math>T_{i+1}</math> in a type-respecting manner). Given an embedding of <math>T_0</math> into <math>T_1</math> (identifying elements of the base "type" with subsets of the base type), embeddings may be defined from each "type" into its successor in a natural way. This can be generalized to transfinite sequences <math>T_{\alpha}</math> with care.

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 <math>\beth_{\omega}</math>, 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 <math>T_{\alpha}</math>'s being used in place of <math>V_{\alpha}</math> 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 [[ordered pair|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 [[urelement]]s 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 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 <math>V_{j(\alpha)}</math> 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 [[Injective function|injection]] from the set of singletons into the set of sets, with the property that ''Endo''( {''x''} ) = {''Endo''( {''y''} ) | ''y''∈''x''} 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.