New Foundations is consistent

4.5 Base actions

Definition 4.25
#

The interference of near-litters \( N_1, N_2 \) is

\[ \operatorname {\mathsf{interf}}(N_1, N_2) = \begin{cases} N_1 \mathrel {\triangle }N_2 & \text{if } N_1^\circ = N_2^\circ \\ N_1 \cap N_2 & \text{if } N_1^\circ \neq N_2^\circ \end{cases} \]

which is a small set of atoms.

Definition 4.26
#

A base action is a pair \( \xi = (\xi ^{\mathcal A}, \xi ^{\mathcal N}) \) such that \( \xi ^{\mathcal A}\) and \( \xi ^{\mathcal N}\) are relations of atoms and near-litters respectively (definition A.1), such that

  • \( \xi ^{\mathcal A}\) and \( \xi ^{\mathcal N}\) are defined on small sets;

  • \( \xi ^{\mathcal A}\) is one-to-one;

  • if \( (a_1, a_2) \in \xi ^{\mathcal A}\) and \( (N_1, N_2) \in \xi ^{\mathcal N}\), then \( a_1 \in N_1 \) if and only if \( a_2 \in N_2 \);

  • if \( (N_1, N_3), (N_2, N_4) \in \xi ^{\mathcal N}\), then \( N_1^\circ = N_2^\circ \) if and only if \( N_3^\circ = N_4^\circ \);

  • for each \( (N_1, N_3), (N_2, N_4) \in \xi ^{\mathcal N}\),

    \[ \operatorname {\mathsf{interf}}(N_1, N_2) \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A};\quad \operatorname {\mathsf{interf}}(N_3, N_4) \subseteq \operatorname {\mathsf{im}}\xi ^{\mathcal A} \]

Note that these conditions imply that \( \xi ^{\mathcal N}\) is one-to-one. We define the one-to-one relation \( \xi ^{\mathcal L}\) by the constructor

\[ (N_1, N_2) \in \xi ^{\mathcal N}\to (N_1^\circ , N_2^\circ ) \in \xi ^{\mathcal L} \]

The partial order on base actions is defined by \( \xi \leq \zeta \) if and only if \( \xi ^{\mathcal A}\leq \zeta ^{\mathcal A}\) and \( \xi ^{\mathcal N}= \zeta ^{\mathcal N}\). 1 The inverse of \( \xi \) is \( ((\xi ^{\mathcal A})^{-1}, (\xi ^{\mathcal N})^{-1}) \). They act on base supports in the natural way.

Definition 4.27
#

A base action \( \xi \) is nice if whenever \( (N_1, N_2) \in \xi ^{\mathcal N}\),

\[ N_1 \mathrel {\triangle }\operatorname {\mathsf{LS}}(N_1^\circ ) \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A};\quad N_2 \mathrel {\triangle }\operatorname {\mathsf{LS}}(N_2^\circ ) \subseteq \operatorname {\mathsf{im}}\xi ^{\mathcal A} \]
Proposition 4.28 extending orbits inside near-litters
#

Every base action \( \xi \) admits an extension \( \zeta \) satisfying

\[ \forall N \in \operatorname {\mathsf{coim}}\xi ^{\mathcal N},\, N \setminus \operatorname {\mathsf{LS}}(N^\circ ) \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A} \]
Proof

For each litter \( L \), there is an injection

\[ i_L : \bigcup _{N \in \operatorname {\mathsf{coim}}\xi ^{\mathcal N}} (N \setminus \operatorname {\mathsf{LS}}(N^\circ )) \to \{ a : {\mathcal A}\mid a^\circ = L \wedge \forall N \in \operatorname {\mathsf{im}}\xi ^{\mathcal N},\, N^\circ = L \to a \in N \} \setminus \operatorname {\mathsf{im}}\xi ^{\mathcal A} \]

by a cardinality argument. Define the relation \( R \) on atoms by the constructor

\[ \forall (N_1, N_2) \in \xi ^{\mathcal N},\, \forall a \in N_1 \setminus \operatorname {\mathsf{LS}}(N_1^\circ ) \setminus \operatorname {\mathsf{coim}}\xi ^{\mathcal A},\, (a, i_{N_2^\circ }(a)) \in R \]

This is one-to-one and has disjoint image and coimage from \( \xi ^{\mathcal A}\).

We now show that if \( (a_1, a_2) \in R \) and \( (N_1, N_2) \in \xi ^{\mathcal N}\), then \( a_1 \in N_1 \) if and only if \( a_2 \in N_2 \). Let \( (N_1, N_2), (N_1', N_2') \in \xi ^{\mathcal N}\), and let \( a \in N_1 \setminus \operatorname {\mathsf{LS}}(N_1^\circ ) \setminus \operatorname {\mathsf{coim}}\xi ^{\mathcal A}\). Suppose that \( a \in N_1' \); we must show \( i_{N_2^\circ }(a) \in N_2' \). If \( N_1^\circ \neq {N_1’}^\circ \), then \( \operatorname {\mathsf{interf}}(N_1, N_1') = N_1 \cap N_1' \), so \( a \in \operatorname {\mathsf{interf}}(N_1, N_1') \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A}\), a contradiction. So \( N_1^\circ = {N_1’}^\circ \), giving \( N_2^\circ = {N_2’}^\circ \), so \( i_{N_2^\circ }(a) = i_{{N_2’}^\circ }(a) \in N_2' \) by definition.

Conversely, suppose that \( i_{N_2^\circ }(a) \in N_2' \); we must show \( a \in N_1' \). Note that by definition, \( i_{N_2^\circ }(a) \in N_2 \). So if \( N_2^\circ \neq {N_2’}^\circ \), we would have \( i_{N_2^\circ }(a) \in N_2 \cap N_2' = \operatorname {\mathsf{interf}}(N_2, N_2') \subseteq \operatorname {\mathsf{im}}\xi ^{\mathcal A}\), a contradiction. Hence \( N_2^\circ = {N_2’}^\circ \) and \( N_1^\circ = {N_1’}^\circ \). Thus, if \( a \notin N_1' \), we would have \( a \in N_1 \mathrel {\triangle }N_1' = \operatorname {\mathsf{interf}}(N_1, N_1') \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A}\), again a contradiction.

Hence \( \zeta = (\xi ^{\mathcal A}\sqcup R, \xi ^{\mathcal N}) \) is a base action and satisfies the conclusion.

Proposition 4.29 extending orbits outside near-litters

Every base action \( \xi \) admits an extension \( \zeta \) satisfying

\[ \forall N \in \operatorname {\mathsf{coim}}\xi ^{\mathcal N},\, \operatorname {\mathsf{LS}}(N) \setminus N \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A} \]
Proof

Without loss of generality (as extensions are transitive), let \( \xi \) satisfy the conclusion of proposition 4.28.

Let \( L \) be an arbitrary litter that whose litter set does not contain an atom in \( \operatorname {\mathsf{im}}\xi ^{\mathcal A}\) or \( \bigcup \operatorname {\mathsf{im}}\xi ^{\mathcal N}\). Define an injection

\[ i : \bigcup _{N \in \operatorname {\mathsf{coim}}\xi ^{\mathcal N}} (\operatorname {\mathsf{LS}}(N^\circ ) \setminus N \setminus \operatorname {\mathsf{coim}}\xi ^{\mathcal A}) \to \operatorname {\mathsf{LS}}(L) \]

by a cardinality argument. Note that \( i \) has domain disjoint from \( \operatorname {\mathsf{coim}}\xi ^{\mathcal A}\) and image disjoint from \( \operatorname {\mathsf{im}}\xi ^{\mathcal A}\).

We show that \( (\xi ^{\mathcal A}\sqcup \operatorname {\mathsf{graph}}i, \xi ^{\mathcal N}) \) is a base action. It suffices to check that if \( (a_1, a_2) \in \operatorname {\mathsf{graph}}i \) and \( (N_1, N_2) \in \xi ^{\mathcal N}\), then \( a_1 \in N_1 \) if and only if \( a_2 \in N_2 \). As \( a_2 \in \operatorname {\mathsf{LS}}(L) \), we have \( a_2 \notin N_2 \). Suppose that \( a_1 \in N_1 \). We know that there is a near-litter \( N \in \operatorname {\mathsf{coim}}\xi ^{\mathcal N}\) such that \( a_1 \in \operatorname {\mathsf{LS}}(N^\circ ) \setminus N \setminus \operatorname {\mathsf{coim}}\xi ^{\mathcal A}\). If \( N^\circ = N_1^\circ \), then \( a_1 \in N \mathrel {\triangle }N_1 = \operatorname {\mathsf{interf}}(N, N_1) \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A}\), a contradiction, hence \( a^\circ = N^\circ \neq N_1^\circ \). But then as \( \xi \) satisfies the conclusion of proposition 4.28, we have \( N_1 \setminus \operatorname {\mathsf{LS}}(N_1^\circ ) \subseteq \operatorname {\mathsf{coim}}\xi ^{\mathcal A}\), which again is a contradiction.

Proposition 4.30

Every base action has a nice extension.

Proof

Apply proposition 4.28 to \( \xi \) to obtain \( \xi _1 \); apply proposition 4.28 again to \( \xi _1^{-1} \) to obtain \( \xi _2 \); apply proposition 4.29 to \( \xi _2 \) to obtain \( \xi _3 \), and finally apply proposition 4.29 again to \( \xi _3^{-1} \) to obtain \( \xi _4 \), our target.

  1. We should make utilities for constructing extensions of base actions, reducing the proof obligations of showing that these are base actions (e.g. removing the last two bullet points and not needing to prove results we already know about \( \xi \)).