New Foundations is consistent

5.1 Strong supports

Definition 5.1
#

We define a preorder \( \preceq \) on base supports by \( S \preceq T \) if and only if \( \operatorname {\mathsf{im}}S^{\mathcal A}\subseteq \operatorname {\mathsf{im}}T^{\mathcal A}\) and \( \operatorname {\mathsf{im}}S^{\mathcal N}\subseteq \operatorname {\mathsf{im}}T^{\mathcal N}\). For \( \beta \)-supports, we define \( S \preceq T \) if and only if \( S_A \preceq T_A \) for each \( A \).

Definition 5.2

A \( \beta \)-support \( S \) is strong if:

  • for every pair of near-litters \( N_1, N_2 \in \operatorname {\mathsf{im}}S_A^{\mathcal N}\), we have \( \operatorname {\mathsf{interf}}(N_1, N_2) \subseteq \operatorname {\mathsf{im}}S_A^{\mathcal A}\); and

  • for every inflexible path \( I = (\gamma ,\delta ,\varepsilon ,A) \) and \( t : \mathsf{Tang}_\delta \), if there is a near-litter \( N \in \operatorname {\mathsf{im}}S_{{A_\varepsilon }_\bot }^{\mathcal N}\) with \( N^\circ = f_{\delta ,\varepsilon }(t) \), then \( \operatorname {\mathsf{supp}}(t) \preceq S_{A_\delta } \).

Proposition 5.3
#

If \( S \) is a strong \( \beta \)-support and \( \rho \) is \( \beta \)-allowable, then \( \rho (S) \) is strong.

Proof

Interference is stable under application of allowable permutations, and the required supports are also preserved under action of allowable permutations.

Proposition 5.4
#

For every support \( S \), there is a strong support \( T \succeq S \).

Proof

We define a relation \( R \) on pairs \( (A, N) \) where \( A : \beta \rightsquigarrow \bot \) and \( N \) is a near-litter by the following constructor. If \( I = (\gamma ,\delta ,\varepsilon ,A) \) and \( t : \mathsf{Tang}_\delta \), then for any near-litter \( N_1 \) such that \( N_1^\circ = f_{\delta ,\varepsilon }(t) \) and any path \( B : \delta \rightsquigarrow \bot \) and near-litter \( N_2 \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}\), we define \( ((A_\delta )_B, N_2) \mathrel {R} ((A_\varepsilon )_\bot , N_1) \). This is well-founded, because if \( (B, N_2) \mathrel {R} (A, N_1) \) then \( \iota (N_2) {\lt} \iota (N_1) \). For any small set \( s \) of such pairs, the transitive closure of \( s \) under \( R \) is small.

Let \( S \) be a support, and let \( s \) be the transitive closure of the set of pairs \( (A, N) \) such that \( N \in \operatorname {\mathsf{im}}S_A^{\mathcal N}\). Generate a support \( T \) from \( S \) and \( s \) using the fact that every small set is the range of some enumeration. This satisfies the second condition of being a strong support.

Now, for any base support \( T \), we define its interference support to be a base support \( U \) consisting of just the atoms in the interference of all near-litters that appear in \( T \). We may extend this definition to structural supports.

Finally, if \( U \) is the interference support of the \( T \) defined above, the support \( T + U \) is strong, and since \( S \succeq T \), we conclude \( S \preceq T + U \).