1.1 Overview

We will begin by discussing the mathematical background for the question of the consistency of \(\mathsf{NF}\). We will establish the mathematical context for the proof we will present. In particular, our proof will not directly show the consistency of \(\mathsf{NF}\); instead, we will construct a model of a related theory known as tangled type theory, or \(\mathsf{TTT}\). We will show that there is a structure that satisfies a particular axiomatisation of \(\mathsf{TTT}\) which we will discuss in section 1.4. The expected conclusion that \(\mathsf{NF}\) is consistent then follows from the fact that \(\mathsf{NF}\) and \(\mathsf{TTT}\) are equiconsistent [ 3 ] .

We will now outline our general strategy for the construction of a model of tangled type theory. As we will outline in section 1.4, \(\mathsf{TTT}\) is a many-sorted theory with types indexed by a limit ordinal \( \lambda \). In order to impose symmetry conditions on our structure, we will add an additional level of objects below type zero. These will not be a part of the final model we construct. This base type will be comprised of objects called atoms (although they are not atoms in the traditional model-theoretic sense). Alongside the construction of the types of our model, we will also construct a group of permutations of each type, called the allowable permutations. Such permutations will preserve the structure of the model in a strong sense; for instance, they preserve membership.

The construction of a given type can only be done under certain hypotheses on the construction of lower types. The most restrictive condition that we will need to satisfy is a bound on the size of each type. In order to do this, we will need to show that there are a lot of allowable permutations. The main technical lemma establishing this, called the freedom of action theorem, roughly states that a partial function that locally behaves like an allowable permutation can be extended to an allowable permutation. It, and its various corollaries, will be outlined in more detail when we are in a position to prove it.

We can then finish the main induction to build the entire model out of the types we have constructed. This step, while invisible to a human reader in set theory, takes substantial effort to formally establish in a dependent type theory. It then remains to show that this is a model of \(\mathsf{TTT}\) as desired, or alternatively, a model of a particular finite axiomatisation.

Finally, we will set out to formally prove the consistency of \(\mathsf{NF}\). This will involve breaking down the model-theoretic arguments from [ 7 , 3 ] into concrete formalisable lemmas.

Implementation details will be discussed in footnotes.