New Foundations is consistent

5.5 Coding the base type

Proposition 5.30 the swap permutation

Let \( S \) be a base support that is closed under interference of near-litters. Let \( a_1, a_2 \) be atoms not in \( \operatorname {\mathsf{im}}S^{\mathcal A}\) such that

\[ \forall N \in \operatorname {\mathsf{im}}S^{\mathcal N},\, a_1 \in N \leftrightarrow a_2 \in N \]

Then there is a base permutation \( \pi \) that fixes \( S \) and maps \( a_1 \) to \( a_2 \).

Proof

Let \( i \) be an index that does not occur in \( \operatorname {\mathsf{coim}}S^{\mathcal A}\), and define \( T_1, T_2 \) by

\[ U_n^{\mathcal A}= S^{\mathcal A}\sqcup \{ (i, a_n) \} ;\quad U_n^{\mathcal N}= S^{\mathcal N} \]

for \( n = 1, 2 \). We claim that \( T_1 \) and \( T_2 \) are have the same specification, treated as \( \bot \)-supports. By appealing to proposition 5.12 and noting that every litter is flexible for the unique path \( \bot \rightsquigarrow \bot \), it suffices to check:

  • (atom condition) For all \( i, a_1, a_2 \), if \( (i, a_1) \in T_1^{\mathcal A}\) and \( (i, a_2) \in T_2^{\mathcal A}\), we have

    \[ \forall j,\, (j, a_1) \in T_1^{\mathcal A}\leftrightarrow (j, a_2) \in T_2^{\mathcal A} \]

    and

    \[ \forall j,\, (\exists N,\, (j, N) \in T_1^{\mathcal N}\wedge a_1 \in N) \leftrightarrow (\exists N,\, (j, N) \in T_2^{\mathcal N}\wedge a_2 \in N) \]
  • (litter condition) For all \( i, N_1, N_2 \), if \( (i, N_1) \in T_1^{\mathcal N}\) and \( (i, N_2) \in T_2^{\mathcal N}\), we have

    \[ \forall j,\, (\exists N',\, (j, N') \in T_1^{\mathcal N}\wedge N_1^\circ = {N’}^\circ ) \leftrightarrow (\exists N',\, (j, N') \in T_2^{\mathcal N}\wedge N_2^\circ = {N’}^\circ ) \]

The atom condition follows directly from the two assumptions, and the litter condition is vacuously true as \( T_1^{\mathcal N}= T_2^{\mathcal N}\).

Note also that \( T_1, T_2 \) are strong, treated as \( \bot \)-supports. Then, by proposition 5.21, there is a \( \bot \)-allowable permutation \( \pi \) such that \( \pi (T_1) = T_2 \). Thus, \( \pi (S) = S \) and \( \pi (a_1) = a_2 \).

Let \( S \) be a base support that is closed under interference of near-litters. Suppose that \( S \) supports a set \( s : \operatorname {\mathsf{Set}}{\mathcal A}\) under the action of base permutations. Then for every pair of atoms \( a_1, a_2 \), the statements

\[ a_1, a_2 \notin \operatorname {\mathsf{im}}S^{\mathcal A} \]

and

\[ \forall N \in \operatorname {\mathsf{im}}S^{\mathcal N},\, a_1 \in N \leftrightarrow a_2 \in N \]

imply that \( a_1 \in s \leftrightarrow a_2 \in s \).

Proof

Let \( a_1, a_2 \) be atoms that satisfy the two statements. By proposition 5.30, there is a base permutation \( \pi \) that fixes \( S \) and maps \( a_1 \) to \( a_2 \). As \( S \) supports \( s \), we obtain \( \pi (s) = s \). So \( a_1 \in s \) if and only if \( a_2 \in s \), as required.

Let \( S \) be a base support. Then \( S \) supports at most \( 2^{\# \kappa } \)-many sets \( s : \operatorname {\mathsf{Set}}{\mathcal A}\) under the action of base permutations.

Proof

Without loss of generality, we may assume \( S \) is closed under interference of near-litters, since extensions will support any object that the original support supports. 1 The information of a set \( s : \operatorname {\mathsf{Set}}{\mathcal A}\) for a base support \( S \) is a triple \( (i^{\mathcal A}, i^{\mathcal N}, p) \) where

  • \( i^{\mathcal A}\) is the set of indices \( i \) such that \( (i, a) \in S^{\mathcal A}\) for some \( a \in s \);

  • \( i^{\mathcal N}\) is the set of indices \( i \) such that \( (i, N) \in S^{\mathcal N}\) for some near-litter \( N \) with \( N \cap s \setminus \operatorname {\mathsf{im}}S^{\mathcal A}\neq \varnothing \);

  • \( p \) is the proposition that every atom \( a \notin \operatorname {\mathsf{im}}S^{\mathcal A}\cup \bigcup \operatorname {\mathsf{im}}S^{\mathcal N}\) lies in \( s \).

Suppose that \( s, t \) are sets of atoms that \( S \) supports. We claim that if \( s \) and \( t \) have the same information \( (i^{\mathcal A}, i^{\mathcal N}, p) \), they are equal. By antisymmetry it suffices to show that \( s \subseteq t \).

Let \( a \in s \). Suppose that \( (i, a) \in S^{\mathcal A}\) for some \( i \). Then \( s \in t \) as \( s, t \) have the same \( i^{\mathcal A}\).

Now suppose that \( a \notin \operatorname {\mathsf{im}}S^{\mathcal A}\), but that there is some near-litter \( N \) with \( a \in N \) and \( (i, N) \in S^{\mathcal N}\). Then there is some atom \( a' \in N \cap t \setminus \operatorname {\mathsf{im}}S^{\mathcal A}\). It suffices by proposition 5.31 to show that

\[ \forall N' \in \operatorname {\mathsf{im}}S^{\mathcal N},\, a \in N' \leftrightarrow a' \in N' \]

because then \( a \in t \) if and only if \( a' \in t \). Suppose that \( a \in N' \) for some \( N' \in \operatorname {\mathsf{im}}S^{\mathcal N}\). If \( N^\circ \neq {N’}^\circ \), then \( a \in N \cap N' \setminus \operatorname {\mathsf{im}}S^{\mathcal A}\) would contradict the assumption that \( S \) is closed under interference. So \( N^\circ = {N’}^\circ \). If \( a' \notin N' \), then \( a \in (N \mathrel {\triangle }N') \setminus \operatorname {\mathsf{im}}S^{\mathcal A}\) would also contradict the assumption that \( S \) is closed under interference. Hence \( a' \in N' \) as required.

Finally, suppose that \( a \notin \operatorname {\mathsf{im}}S^{\mathcal A}\) and for all near-litters \( N \in \operatorname {\mathsf{im}}S^{\mathcal N}\), we have \( a \notin N \). If \( a \notin t \), then \( p \) is false, so there is an atom \( a' \) with the same properties that does not lie in \( s \). Again, it suffices by proposition 5.31 to show that

\[ \forall N' \in \operatorname {\mathsf{im}}S^{\mathcal N},\, a \in N' \leftrightarrow a' \in N' \]

because then \( a \in s \) if and only if \( a' \in s \). But the left-hand side and the right-hand side are both false, giving the result.

This result shows that the map that sends a set \( s \) that \( S \) supports to its information is injective, and so as there are \( 2^{\# \kappa } \)-many possible information tuples, there are at most \( 2^{\# \kappa } \)-many sets that \( S \) supports under the action of base permutations.