New Foundations is consistent

5.6 Counting

Proposition 5.33

Suppose that for all type indices δ<β, there are strictly less than #μ-many δ-coding functions. Then there are less than #μ β-specifications.

Proof
Definition 5.34

A weak β-specification is a triple W=(RA,RN,σ) where RA,RN are β-trees of relations on κ, and σ is a β-specification. We say that a weak specification specifies a support S if there is a strong support T such that σ=spec(T), ST, and

(i,j)RAAa,(i,a)SAA(j,a)TAA(i,j)RANN,(i,N)SAN(j,N)TAN
Proposition 5.35

Every support has a weak specification that specifies it.

Proof
Proposition 5.36

If W is a weak specification that specifies supports S and T, then there is an allowable permutation ρ such that ρ(S)=T.

Proof
Proposition 5.37

Suppose that for all type indices δ<β, there are strictly less than #μ-many δ-coding functions. Then there are less than #μ weak β-specifications.

Proof

Suppose that for all type indices δ<β, there are strictly less than #μ-many δ-coding functions. Then there are less than #μ β-support orbits.

Proof
Proposition 5.39

Let β be a type index (which in practice will be or the lowest proper type index). Suppose that there are less than #μ β-support orbits. Let ν be a cardinal less than #μ such that for each β-support S, there are at most ν-many objects x:TSetβ that S supports. Then there are less than #μ β-coding functions.

Proof

There are less than #μ -coding functions.

Proof

There are less than #μ β-coding functions if β is the minimal inhabitant of λ.

Proof

Suppose that for all type indices δ<β, there are strictly less than #μ-many δ-coding functions. Then if γ<β is a proper type index, there are strictly less than #μ (γ,β)-raised singletons.

Proof

There are less than #μ-many β-coding functions for all type indices βα.

Proof
Proposition 5.44

For each type index βα, #TSetβ=#μ.

Proof
Proposition 5.45

For each type index βα, #Tangβ=#μ.

Proof
  1. One useful claim to prove for this is that there is a unique path β, and so type β objects satisfy -extensionality by injectivity of Uβ.