8 Model theory and verifying \( \operatorname {\mathsf{Con}}(\mathsf{NF}) \)

In this chapter, we establish the model theory that is used to derive the consistency of \( \mathsf{NF}\) from that of \( \mathsf{TTT}\). This requires much of mathlib’s model theory library to be completely rewritten for the many-sorted case, which is (so far) not an objective of this project. Some potential design decisions are considered in the following sections. On the whole, this chapter should be considered just a sketch of the main argument: sufficient for a human reader, but insufficient for a detailed blueprint.