New Foundations is consistent
1
Introduction
▶
1.1
Overview
1.2
The simple theory of types
1.3
New Foundations
1.4
Tangled type theory
1.5
Finitely axiomatising tangled type theory
2
Setting up the environment
▶
2.1
Conventions
2.2
Model parameters
2.3
The structural hierarchy
2.4
Position functions
2.5
Hypotheses of the recursion
3
Constructing the types
▶
3.1
Codes and clouds
3.2
Model data defined
3.3
Typed near-litters, singletons, and positions
4
Freedom of action
▶
4.1
Base approximations
4.2
Extensions of approximations
4.3
Structural approximations
4.4
Proving freedom of action
4.5
Base actions
4.6
Structural actions
5
The counting argument
▶
5.1
Strong supports
5.2
Coding functions
5.3
Specifications
5.4
Recoding
5.5
Coding the base type
5.6
Counting
6
Wrapping up the main induction
▶
6.1
Induction, in abstract
6.2
Building the tower
7
Verifying \( \operatorname {\mathsf{Con}}(\mathsf{TTT}) \)
▼
7.1
Raising strong supports
7.2
Tangled type theory
8
Model theory and verifying \( \operatorname {\mathsf{Con}}(\mathsf{NF}) \)
▶
8.1
Many-sorted model theory
8.2
Term models
8.3
Ambiguity
A
Auxiliary results
▶
A.1
Relations
A.2
Cardinal arithmetic
B
Bibliography
Chapter 2 graph
Chapter 3 graph
Chapter 4 graph
Chapter 5 graph
Chapter 6 graph
Chapter 7 graph
Appendix A graph
7 Verifying \( \operatorname {\mathsf{Con}}(\mathsf{TTT}) \)
7.1
Raising strong supports
7.2
Tangled type theory