New Foundations is consistent

7.1 Raising strong supports

In this section, let \( \gamma {\lt} \beta \) be proper type indices strictly below the current level \( \alpha \).

Proposition 7.1

Let \( T \) be a \( \gamma \)-support, and let \( U \) be the strong support generated by \( T^\beta \). If \( A \) is a path such that \( \operatorname {\mathsf{im}}U_A^{\mathcal N}\) is nonempty, then \( A \) has length at least 2.

Proof

Let \( N \in \operatorname {\mathsf{im}}U_A^{\mathcal N}\). Either \( A \) is of the form \( B^\beta \) for \( B : \gamma \rightsquigarrow \bot \) and \( N \in \operatorname {\mathsf{im}}T_B^{\mathcal N}\), in which case \( B \) clearly has length at least 2 as \( \gamma \) is a proper type index, or \( N \in \operatorname {\mathsf{im}}V_B^{\mathcal N}\) where \( A = B^\beta \) and \( B : \delta \rightsquigarrow \bot \), and \( V \) supports some \( \delta \)-set. But we cannot have \( \delta = \bot \), because \( \bot \)-supports that support some \( \delta \)-set cannot contain near-litters, so in this other case \( A \) also has length at least 2.

Proposition 7.2

Let \( T \) be a \( \gamma \)-support, and let \( U \) be the strong support generated by \( T^\beta \). Then \( U^\alpha \) is strong.

Proof

The interference condition is clear.

First we show that proofs that \( A^\alpha \)-inflexibility for litters that appear in \( U^\alpha \) correspond to proofs of \( A \)-inflexibility. Clearly if \( L \) is \( A^\alpha \)-flexible then \( L \) is \( A \)-flexible. Instead, let \( I = (\delta , \varepsilon , \zeta , A) \) be an inflexible \( \alpha \)-path and \( t : \mathsf{Tang}_\varepsilon \) such that there is a near-litter \( N \in \operatorname {\mathsf{im}}(U^\alpha )^{\mathcal N}_{{A_\zeta }_\bot } \) with \( N^\circ = f_{\varepsilon ,\zeta }(t) \). Suppose that \( A \) is the empty path, so \( \delta = \alpha \). Then \( (U^\alpha )^{\mathcal N}_{{A_\zeta }_\bot } = (U^\alpha )^{\mathcal N}_{\zeta _\bot } \) is nonempty, so \( \zeta = \beta \). This shows that \( \operatorname {\mathsf{im}}(U^\alpha )^{\mathcal N}_{\beta _\bot } = \operatorname {\mathsf{im}}U^{\mathcal N}_\bot \) is nonempty, contradicting proposition 7.1. So \( A \) is nonempty, and is of the form \( B^\alpha \) for \( B : \beta \rightsquigarrow \delta \). So \( (\delta ,\varepsilon ,\zeta ,B) \) is an inflexible \( \beta \)-path for \( N^\circ \).

The expected conclusion then follows directly from the fact that \( U \) is strong.

Let \( S \) be a strong \( \alpha \)-support and let \( T \) be a \( \gamma \)-support. Let \( U \) be the strong support generated by \( T^\beta \), and let \( V \) be the support whose image is precisely those atoms in the interference of \( S_\beta \) and \( U \). Let \( \rho \) be a \( \beta \)-allowable permutation that fixes \( S_\beta \). Then \( S + (\rho (U + V))^\alpha \) is strong.

Proof

Follows directly from ??.

Proposition 7.4

Let \( S \) be a strong \( \alpha \)-support. Let \( U \) be a strong \( \beta \)-support with the property that if \( A \) is a path such that \( \operatorname {\mathsf{im}}U_A^{\mathcal N}\) is nonempty, then \( A \) has length at least 2. Then for every \( \beta \)-allowable \( \rho \) that fixes \( S_\beta \), we have \( \operatorname {\mathsf{spec}}(S + U^\alpha ) = \operatorname {\mathsf{spec}}(S + (\rho (U))^\alpha ) \).

Proof

Appeal to proposition 5.12. First, note that \( (i, a) \in (S + (\rho (U))^\alpha )_A^{\mathcal A}\) if and only if \( (i, a) \in S \) or \( A = B^\alpha \) and \( (i, a) \in \rho (U)_B^{\mathcal A}\). Thus,

\begin{align*} (i, a_1) \in (S + U^\alpha )_A^{\mathcal A}& \to \exists a_2,\, (i, a_2) \in (S + (\rho (U))^\alpha )_A^{\mathcal A}\\ & \quad \wedge [(\exists B,\, A = B^\alpha \wedge \rho _B(a_1) = a_2) \vee ((\forall B,\, A \neq B^\alpha ) \wedge a_1 = a_2)] \end{align*}

and the same holds for the other direction 1 and for near-litters.

The coimage condition is clear. Suppose that \( (i, a_1) \in (S + U^\alpha )_A^{\mathcal A}\) and \( (i, a_2) \in (S + (\rho (U))^\alpha )_A^{\mathcal A}\). Then by coinjectivity we can apply the above result, giving that either there is \( B \) such that \( A = B^\alpha \) and \( \rho _B(a_1) = a_2 \), or there is no such \( B \), and \( a_1 = a_2 \). In either case, the result is easy to show.

The result for litters follows from the fact that the condition on \( U \) implies that proofs of inflexiblity of litters in \( U \) correspond bijectively to proofs of inflexibility of litters in \( U^\alpha \). 2

Let \( S \) be a strong \( \alpha \)-support and let \( T \) be a \( \gamma \)-support. Let \( \rho \) be a \( \beta \)-allowable permutation that fixes \( S_\beta \). Then there is an \( \alpha \)-allowable permutation \( \rho ' \) such that

\[ \rho '(S) = S;\quad (\rho '_\beta )_\gamma (T) = \rho _\gamma (T) \]
Proof

Let \( U \) be the strong support generated by \( T^\beta \), and let \( V \) be the support whose image is precisely those atoms in the interference of \( S_\beta \) and \( U \). Then apply ??.

  1. We can prove the other direction easily from this by substituting \( \rho (U) \) and \( \rho ^{-1} \).
  2. TODO: Probably want more details when we get here.