New Foundations is consistent

5.3 Specifications

Definition 5.10

An atom condition is a pair \( (s, t) \) where \( s, t : \operatorname {\mathsf{Set}}\kappa \). A \( \beta \)-near-litter condition is either

  • a flexible condition, consisting of a set \( s : \operatorname {\mathsf{Set}}\kappa \); or

  • an inflexible condition, consisting of an inflexible \( \beta \)-path \( I = (\gamma ,\delta ,\varepsilon ,A) \), a \( \delta \)-coding function \( \chi \), and two \( \delta \)-trees \( R^{\mathcal A}, R^{\mathcal N}\) of relations on \( \kappa \).

A \( \beta \)-specification is a pair \( (\sigma ^{\mathcal A}, \sigma ^{\mathcal N}) \) where

  • \( \sigma ^{\mathcal A}\) is a \( \beta \)-tree of enumerations of atom conditions; and

  • \( \sigma ^{\mathcal N}\) is a \( \beta \)-tree of enumerations of \( \beta \)-near-litter conditions.

Let \( S \) be a \( \beta \)-support. Then its specification is the \( \beta \)-specification \( \sigma = \operatorname {\mathsf{spec}}(S) \) given by the following constructors.

  • Whenever \( (i, a) \in S_A^{\mathcal A}\), we have \( (i, (s, t)) \in \sigma _A^{\mathcal A}\) where

    \[ s = \{ j : \kappa \mid (j, a) \in S_A^{\mathcal A}\} ;\quad t = \{ j : \kappa \mid \exists N,\, (j, N) \in S_A^{\mathcal N}\wedge a \in N \} \]
  • Whenever \( (i, N) \in S_A^{\mathcal N}\) and \( N^\circ \) is \( A \)-flexible, we have \( (i, c) \in \sigma _A^{\mathcal N}\) where \( c \) is the flexible condition given by

    \[ s = \{ j : \kappa \mid \exists N',\, (j, N') \in S_A^{\mathcal N}\wedge N^\circ = {N’}^\circ \} \]
  • Whenever \( I = (\gamma ,\delta ,\varepsilon ,A) \) is an inflexible \( \beta \)-path, \( t : \mathsf{Tang}_\delta \), and \( (i, N) \in S_{{A_\varepsilon }_\bot }^{\mathcal N}\) is such that \( N^\circ = f_{\delta ,\varepsilon }(t) \), we have \( (i, c) \in \sigma _{{A_\varepsilon }_\bot }^{\mathcal N}\) where \( c \) is the inflexible condition given by path \( I \) and coding function \( \chi _t \), and \( R^{\mathcal A}\) and \( R^{\mathcal N}\) are the \( \delta \)-trees of relations given by the constructors

    \begin{align*} & \forall i,\, \forall j,\, \forall a,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\to (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}\to (i, j) \in R_B^{\mathcal A}\\ & \forall i,\, \forall j,\, \forall N,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\to (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}\to (i, j) \in R_B^{\mathcal N}\end{align*}
Proposition 5.12

Let \( S, T \) be \( \beta \)-supports. Then \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \) if and only if 1

  • \( \operatorname {\mathsf{coim}}S_A^{\mathcal A}= \operatorname {\mathsf{coim}}T_A^{\mathcal A}\) and \( \operatorname {\mathsf{coim}}S_A^{\mathcal N}= \operatorname {\mathsf{coim}}T_A^{\mathcal N}\).

  • (atom condition) Whenever \( (i, a_1) \in S_A^{\mathcal A}\) and \( (i, a_2) \in T_A^{\mathcal A}\), we have

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

    and

    \[ \forall j,\, (\exists N,\, (j, N) \in S_A^{\mathcal N}\wedge a_1 \in N) \leftrightarrow (\exists N,\, (j, N) \in T_A^{\mathcal N}\wedge a_2 \in N) \]
  • (flexible condition) Whenever \( (i, N_1) \in S_A^{\mathcal N}\) and \( (i, N_2) \in T_A^{\mathcal N}\), if \( N_1^\circ \) is \( A \)-flexible, then so is \( N_2^\circ \), and

    \[ \forall j,\, (\exists N',\, (j, N') \in S_A^{\mathcal N}\wedge N_1^\circ = {N’}^\circ ) \leftrightarrow (\exists N',\, (j, N') \in T_A^{\mathcal N}\wedge N_2^\circ = {N’}^\circ ) \]
  • (inflexible condition) Let \( I = (\gamma ,\delta ,\varepsilon ) \) be an inflexible \( \beta \)-path and let \( t : \mathsf{Tang}_\delta \). Then whenever \( (i, N_1) \in S_{{A_\varepsilon }_\bot }^{\mathcal N}\) and \( (i, N_2) \in T_{{A_\varepsilon }_\bot }^{\mathcal N}\) are such that \( N_1^\circ = f_{\delta ,\varepsilon }(t) \), there is some \( \delta \)-allowable permutation \( \rho \) such that \( N_2^\circ = f_{\delta ,\varepsilon }(\rho (t)) \), and

    \begin{align*} \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}& \to \forall i,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\leftrightarrow (i, \rho _B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\\ \forall j,\, \forall N,\, (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}& \to \forall i,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\leftrightarrow (i, \rho _B(N)) \in T_{{A_\delta }_B}^{\mathcal N}\end{align*}
Proof

We will only sketch the fourth bullet point of this proof; the remainder is direct (but quite long to write down on paper). Moreover, we will show this for atoms; the result for near-litters is identical. The specifications \( \operatorname {\mathsf{spec}}(S) \) and \( \operatorname {\mathsf{spec}}(T) \) give rise to the same trees \( R^{\mathcal A}\) precisely when

\[ \forall i,\, \forall j,\, (\exists a,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\wedge (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}) \leftrightarrow (\exists a,\, (i, a) \in T_{{A_\delta }_B}^{\mathcal A}\wedge (j, a) \in \operatorname {\mathsf{supp}}(\rho (t))_B^{\mathcal A}) \]

We must show that this holds if and only if

\[ \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}\to \forall i,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\leftrightarrow (i, \rho _B(a)) \in T_{{A_\delta }_B}^{\mathcal A} \]

This can be concluded by appealing to the basic behaviour of \( \rho \) and noting the coinjectivity of \( \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}\).

Proposition 5.13

Let \( \rho \) be \( \beta \)-allowable, and let \( S \) be a \( \beta \)-support. Then \( \operatorname {\mathsf{spec}}(\rho (S)) = \operatorname {\mathsf{spec}}(S) \).

Proof

We appeal to proposition 5.12. Clearly the coimage condition holds.

For the atom condition, we must check that if \( (i, a) \in S_A^{\mathcal A}\), we have

\[ \forall j,\, (j, a) \in S_A^{\mathcal A}\leftrightarrow (j, \rho _A(a)) \in \rho (S)_A^{\mathcal A} \]

and

\[ \forall j,\, (\exists N,\, (j, N) \in S_A^{\mathcal N}\wedge a \in N) \leftrightarrow (\exists N,\, (j, N) \in \rho (S)_A^{\mathcal N}\wedge \rho _A(a) \in N) \]

both of which are trivial.

For the flexible condition, we must check that if \( (i, N) \in S_A^{\mathcal N}\) and \( N^\circ \) is \( A \)-flexible, then \( \rho _A(N)^\circ \) is also \( A \)-flexible (which is direct, and should already be its own lemma), and that

\[ \forall j,\, (\exists N',\, (j, N') \in S_A^{\mathcal N}\wedge N^\circ = {N’}^\circ ) \leftrightarrow (\exists N',\, (j, N') \in \rho (S)_A^{\mathcal N}\wedge \rho (N)^\circ = {N’}^\circ ) \]

which is similarly trivial.

Finally, for the inflexible condition, suppose that \( I = (\gamma ,\delta ,\varepsilon ) \) is an inflexible \( \beta \)-path and \( t : \mathsf{Tang}_\delta \). Let \( (i, N) \in S_{{A_\varepsilon }_\bot }^{\mathcal N}\) be such that \( N^\circ = f_{\delta ,\varepsilon }(t) \). Then by the coherence condition,

\[ \rho _{{A_\varepsilon }_\bot }(N)^\circ = \rho _{{A_\varepsilon }_\bot }(N^\circ ) = \rho _{{A_\varepsilon }_\bot }(f_{\delta ,\varepsilon }(t)) = f_{\delta ,\varepsilon }(\rho _{A_\delta }(t)) \]

We must check that

\begin{align*} \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}& \to \forall i,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\leftrightarrow (i, (\rho _{A_\delta })_B(a)) \in \rho (S)_{{A_\delta }_B}^{\mathcal A}\\ \forall j,\, \forall N,\, (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}& \to \forall i,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\leftrightarrow (i, (\rho _{A_\delta })_B(N)) \in \rho (S)_{{A_\delta }_B}^{\mathcal N}\end{align*}

which again is trivial.

Definition 5.14

Let \( S \) and \( T \) be base supports. We define the relations \( \operatorname {\mathsf{conv}}_{S,T}^{\mathcal A}, \operatorname {\mathsf{conv}}_{S,T}^{\mathcal N}\) by the constructors 2

\begin{align*} & (i, a_1) \in S^{\mathcal A}\to (i, a_2) \in T^{\mathcal A}\to (a_1, a_2) \in \operatorname {\mathsf{conv}}_{S,T}^{\mathcal A}\\ & (i, N_1) \in S^{\mathcal N}\to (i, N_2) \in T^{\mathcal N}\to (N_1, N_2) \in \operatorname {\mathsf{conv}}_{S,T}^{\mathcal N}\end{align*}

Note that \( {\operatorname {\mathsf{conv}}_{S,T}^{\mathcal A}}^{-1} = \operatorname {\mathsf{conv}}_{T,S}^{\mathcal A}\) and \( {\operatorname {\mathsf{conv}}_{S,T}^{\mathcal N}}^{-1} = \operatorname {\mathsf{conv}}_{T,S}^{\mathcal N}\).

Let \( S, T \) be supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then \( \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) is one-to-one.

Proof

If \( (a_1, a_2), (a_1, a_3) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\), then there are \( i, j \) such that \( (i, a_1), (j, a_1) \in S_A^{\mathcal A}\) and \( (i, a_2), (j, a_3) \in T_A^{\mathcal A}\). By proposition 5.12, we deduce \( (j, a_1) \in S_A^{\mathcal A}\leftrightarrow (j, a_2) \in T_A^{\mathcal A}\), so by coinjectivity of \( T_A^{\mathcal A}\), we deduce \( a_2 = a_3 \). Hence \( \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) is coinjective. By symmetry, \( \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) is one-to-one.

Let \( S, T \) be supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). If \( (a_1, a_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) and \( (N_1, N_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\), then \( a_1 \in N_1 \) if and only if \( a_2 \in N_2 \).

Proof

As \( (a_1, a_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\), there is \( i \) such that \( (i, a_1) \in S_A^{\mathcal A}\) and \( (i, a_2) \in T_A^{\mathcal A}\), and as \( (N_1, N_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\), there is \( j \) such that \( (j, N_1) \in S_A^{\mathcal N}\) and \( (j, N_2) \in T_A^{\mathcal N}\). By proposition 5.12, we deduce that

\[ \forall j,\, (\exists N,\, (j, N) \in S_A^{\mathcal N}\wedge a_1 \in N) \leftrightarrow (\exists N,\, (j, N) \in T_A^{\mathcal N}\wedge a_2 \in N) \]

If \( a_1 \in N_1 \), then as \( (j, N_1) \in S_A^{\mathcal N}\), we deduce that there is a near-litter \( N' \) such that \( (j, N') \in T_A^{\mathcal N}\) and \( a \in N' \). But \( T_A^{\mathcal N}\) is coinjective, so \( N' = N_2 \), giving \( a \in N_2 \). The converse holds by symmetry.

Let \( S, T \) be supports such that \( T \) is strong and \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). If \( (N_1, N_3), (N_2, N_4) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\), then \( N_1^\circ = N_2^\circ \) if and only if \( N_3^\circ = N_4^\circ \).

Proof

There are \( i, j \) such that \( (i, N_1), (j, N_2) \in S_A^{\mathcal N}\) and \( (i, N_3), (j, N_4) \in T_A^{\mathcal N}\). Suppose that \( N_1^\circ = N_2^\circ \); we show that \( N_3^\circ = N_4^\circ \).

First, suppose that \( N_1^\circ \) is \( A \)-flexible. Then by proposition 5.12, we have

\[ \forall j,\, (\exists N',\, (j, N') \in S_A^{\mathcal N}\wedge N_1^\circ = {N’}^\circ ) \leftrightarrow (\exists N',\, (j, N') \in T_A^{\mathcal N}\wedge N_3^\circ = {N’}^\circ ) \]

So as \( (j, N_2) \in S_A^{\mathcal N}\) and \( N_1^\circ = N_2^\circ \), there is \( N' \) with \( (j, N') \in T_A^{\mathcal N}\) and \( N_3^\circ = {N’}^\circ \), but clearly \( N' = N_4 \), giving the result.

Now suppose that \( N_1^\circ \) is \( A \)-inflexible, so there is an inflexible \( \beta \)-path \( (\gamma ,\delta ,\varepsilon ,B) \) and tangle \( t : \mathsf{Tang}_\delta \) such that

\[ A = {B_\varepsilon }_\bot ;\quad N_1^\circ = f_{\delta ,\varepsilon }(t) \]

Then by proposition 5.12, there is some \( \delta \)-allowable \( \rho \) such that \( N_3^\circ = f_{\delta ,\varepsilon }(\rho (t)) \) and

\begin{align*} \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}& \to \forall i,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\leftrightarrow (i, \rho _B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\\ \forall j,\, \forall N,\, (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}& \to \forall i,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\leftrightarrow (i, \rho _B(N)) \in T_{{A_\delta }_B}^{\mathcal N}\end{align*}

But as \( N_1^\circ = N_2^\circ \), we draw the same conclusion about \( N_2 \) and \( N_4 \), giving a \( \delta \)-allowable permutation \( \rho ' \) such that \( N_4^\circ = f_{\delta ,\varepsilon }(\rho '(t)) \); note that the inflexible path and tangle in question will be the same for both pairs. We also have

\begin{align*} \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}& \to \forall i,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\leftrightarrow (i, \rho ’_B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\\ \forall j,\, \forall N,\, (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}& \to \forall i,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\leftrightarrow (i, \rho ’_B(N)) \in T_{{A_\delta }_B}^{\mathcal N}\end{align*}

Combining these, we obtain

\begin{align*} \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}& \to \forall i,\, (i, \rho _B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\leftrightarrow (i, \rho ’_B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\\ \forall j,\, \forall N,\, (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}& \to \forall i,\, (i, \rho _B(N)) \in T_{{A_\delta }_B}^{\mathcal N}\leftrightarrow (i, \rho ’_B(N)) \in T_{{A_\delta }_B}^{\mathcal N}\end{align*}

We claim that \( \rho (\operatorname {\mathsf{supp}}(t)) = \rho '(\operatorname {\mathsf{supp}}(t)) \). As \( T \) is strong, for each atom \( a \) such that \( (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}\), there is some \( k \) such that \( (i, \rho _B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\). Thus \( \rho _B(a) = \rho '_B(a) \). The same conclusion may be drawn for near-litters. Thus \( \rho (\operatorname {\mathsf{supp}}(t)) = \rho '(\operatorname {\mathsf{supp}}(t)) \), giving \( \rho (t) = \rho '(t) \), and hence \( N_3^\circ = N_4^\circ \).

Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then for each \( (N_1, N_3), (N_2, N_4) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\),

\[ \operatorname {\mathsf{interf}}(N_1, N_2) \subseteq \operatorname {\mathsf{coim}}\operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A};\quad \operatorname {\mathsf{interf}}(N_3, N_4) \subseteq \operatorname {\mathsf{im}}\operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A} \]
Proof

As \( S \) is strong, we have \( \operatorname {\mathsf{interf}}(N_1, N_2) \subseteq \operatorname {\mathsf{im}}S_A^{\mathcal A}\). But \( \operatorname {\mathsf{coim}}\operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}= \operatorname {\mathsf{im}}S_A^{\mathcal A}\), as required. 3 The result for \( \operatorname {\mathsf{interf}}(N_3, N_4) \) then follows by symmetry.

Let \( S, T \) be strong \( \beta \)-supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then for each \( A \), we define the base action \( \operatorname {\mathsf{conv}}_{S_A, T_A} \) to be \( (\operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}, \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}) \); this is a base action by ??. We now define the \( \beta \)-action \( \operatorname {\mathsf{conv}}_{S,T} \) by \( (\operatorname {\mathsf{conv}}_{S,T})_A = \operatorname {\mathsf{conv}}_{S_A,T_A} \).

Proposition 5.20

Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then \( \operatorname {\mathsf{conv}}_{S,T} \) is coherent.

Proof

Suppose that \( (N_1, N_2) \in \operatorname {\mathsf{conv}}_{S_A,T_A}^{\mathcal N}\), so there is \( i \) such that \( (i, N_1) \in S_A^{\mathcal N}\) and \( (i, N_2) \in T_A^{\mathcal N}\).

Suppose that \( N_1^\circ \) is \( A \)-flexible. By proposition 5.12, we immediately conclude that \( N_2^\circ \) is \( A \)-flexible as required.

Now suppose that \( N_1^\circ \) is \( A \)-inflexible with inflexible \( \beta \)-path \( I = (\gamma ,\delta ,\varepsilon ,B) \) and tangle \( t : \mathsf{Tang}_\delta \). By proposition 5.12, there is some \( \delta \)-allowable permutation \( \rho \) such that \( N_2^\circ = f_{\delta ,\varepsilon }(\rho (t)) \) and

\begin{align*} \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_C^{\mathcal A}& \to \forall i,\, (i, a) \in S_{{B_\delta }_C}^{\mathcal A}\leftrightarrow (i, \rho _C(a)) \in T_{{B_\delta }_C}^{\mathcal A}\\ \forall j,\, \forall N,\, (j, N) \in \operatorname {\mathsf{supp}}(t)_C^{\mathcal N}& \to \forall i,\, (i, N) \in S_{{B_\delta }_C}^{\mathcal N}\leftrightarrow (i, \rho _C(N)) \in T_{{B_\delta }_C}^{\mathcal N}\end{align*}

We must show that \( ((\operatorname {\mathsf{conv}}_{S,T})_B)_\delta (\operatorname {\mathsf{supp}}(t)) = \rho (\operatorname {\mathsf{supp}}(t)) \). We will show the result for atoms; the result for near-litters is identical. Let \( (j, a) \in \operatorname {\mathsf{supp}}(t)_C^{\mathcal A}\). Then as \( S \) is strong, there is \( k \) such that \( (k, a) \in S_{{B_\delta }_C}^{\mathcal A}\). Then by the equation above, \( (k, \rho _C(a)) \in T_{{B_\delta }_C}^{\mathcal A}\). Hence \( (a, \rho _C(a)) \in (((\operatorname {\mathsf{conv}}_{S,T})_B)_\delta )_C \) as required.

Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then there is an allowable permutation \( \rho \) such that \( \rho (S) = T \).

Proof

By proposition 5.20, we may apply theorem 4.38 to \( \operatorname {\mathsf{conv}}_{S,T} \) to obtain an allowable permutation \( \rho \) that \( \operatorname {\mathsf{conv}}_{S,T} \) approximates, which directly gives \( \rho (S) = T \) as required.

  1. The following bullet points should comprise a proposition type relating \( S \) and \( T \).
  2. This should be abstracted out even further; this can be defined for any pair of relations with common domain.
  3. Make this a lemma.