New Foundations is consistent

3.1 Codes and clouds

Definition 3.1 code

A code is a pair \( c = (\beta , s) \) where \( \beta {\lt} \alpha \) is a type index and \( s \) is a nonempty set of \( \mathsf{TSet}_\beta \).

The cloud relation \( \prec \) on codes is given by the constructor

\[ (\beta , s) \prec (\gamma , \{ \operatorname {\mathsf{typed}}_\gamma (N) \mid \exists t : \mathsf{Tang}_\beta ,\, \operatorname {\mathsf{set}}(t) \in s \wedge N^\circ = f_{\beta ,\gamma }(t) \} ) \]

where \( \beta , \gamma {\lt} \alpha \) are distinct and \( \gamma \) is proper.

Proposition 3.3

If \( c \prec (\gamma , s_1) \) and \( c \prec (\gamma , s_2) \), then \( s_1 = s_2 \).

Proof

Let \( c = (\beta , s) \). We obtain

\[ s_1 = \{ \operatorname {\mathsf{typed}}_\gamma (N) \mid \exists t : \mathsf{Tang}_\beta ,\, \operatorname {\mathsf{set}}(t) \in s \wedge N^\circ = f_{\beta ,\gamma }(t) \} = s_2 \]

as required.

Proposition 3.4

The cloud relation is injective (definition A.1). That is, if \( c_1, c_2 \prec d \), then \( c_1 = c_2 \).

Proof

Let \( c_i = (\beta _i, s_i) \) for \( i = 1, 2 \), and let \( d = (\gamma , s') \).

We first show that \( \beta _1 = \beta _2 \). Choose some \( t_1 : \mathsf{Tang}_{\beta _1} \) such that \( \operatorname {\mathsf{set}}(t_1) \in s_1 \). We can show directly that \( \operatorname {\mathsf{typed}}_\gamma (\operatorname {\mathsf{NL}}(f_{\beta _1,\gamma }(t_1))) \in s' \). So there is some \( t_2 : \mathsf{Tang}_{\beta _2} \) such that

\[ \operatorname {\mathsf{typed}}_\gamma (\operatorname {\mathsf{NL}}(f_{\beta _1,\gamma }(t_1))) = \operatorname {\mathsf{typed}}_\gamma (N);\quad N^\circ = f_{\beta _2,\gamma }(t_2) \]

Then since the typed near-litter map is injective (definition 2.24), the fact that the equations \( N^\circ = L_1 \) and \( N = \operatorname {\mathsf{NL}}(L_2) \) imply \( L_1 = L_2 \), and that the \( f \)-maps have disjoint ranges (proposition 2.22), we obtain \( \beta _1 = \beta _2 \).

We now show that if \( (\beta , s_1), (\beta , s_2) \prec d \), then \( s_1 \subseteq s_2 \). Let \( d = (\gamma , s') \) as above. Let \( x \in s_1 \), and choose \( t_1 : \mathsf{Tang}_\beta \) such that \( x = \operatorname {\mathsf{set}}(t_1) \). Then as \( (\beta , s_1) \prec d \), we have \( \operatorname {\mathsf{typed}}_\gamma (\operatorname {\mathsf{NL}}(f_{\beta ,\gamma }(t_1))) \in s' \). So there is some \( t_2 : \mathsf{Tang}_\beta \) with \( \operatorname {\mathsf{set}}(t_2) \in s_2 \) such that

\[ \operatorname {\mathsf{typed}}_\gamma (\operatorname {\mathsf{NL}}(f_{\beta ,\gamma }(t_1))) = \operatorname {\mathsf{typed}}_\gamma (N);\quad N^\circ = f_{\beta ,\gamma }(t_2) \]

For the same reasons as above, together with injectivity of \( f_{\beta ,\gamma } \), we have \( t_1 = t_2 \). In particular, \( x \in s_2 \) as required.

This gives the required result by antisymmetry.

Proposition 3.5

The cloud relation is well-founded.

Proof

Define a function \( F \) that maps a code \( c = (\beta , s) \) to the set

\[ \{ \iota (t) \mid \operatorname {\mathsf{set}}(t) \in s \} : \operatorname {\mathsf{Set}}\mu \]

We first show that \( c_1 \prec c_2 \) implies that

\[ \forall \nu _2 \in F(c_2),\, \exists \nu _1 \in F(c_1),\, \nu _1 {\lt} \nu _2 \]

Let \( c_i = (\beta _i, s_i) \) for \( i = 1, 2 \), and suppose \( \nu _2 \in F(c_2) \). Then \( \nu _2 = \iota (t_2) \) with \( \operatorname {\mathsf{set}}(t_2) \in s_2 \). By definition, \( \operatorname {\mathsf{set}}(t_2) = \operatorname {\mathsf{typed}}_{\beta _2}(N) \) where \( N^\circ = f_{\beta _1,\beta _2}(t_1) \) and \( \operatorname {\mathsf{set}}(t_1) \in s_1 \). Then \( \iota (t_1) \in F(c_1) \), and \( \iota (t_1) {\lt} \iota (N) \leq \iota (t_2) \) by ??, as required.

Now, we define a function \( f \) that maps a code \( c \) to \( \min F(c) \), which is always well-defined as \( F(c) \) is nonempty. The above result shows that \( c_1 \prec c_2 \) implies \( f(c_1) {\lt} f(c_2) \). Thus \( \prec \) is a subrelation of the well-founded relation given by the inverse image of \( f \), so is well-founded.

Proposition 3.6

Let \( \prec \) be a relation on a type \( \tau \). We say that an object \( x : \tau \) is \( \prec \)-even if all of its \( \prec \)-predecessors are odd; we say that \( x \) is \( \prec \)-odd if it has a \( \prec \)-predecessor that is even. Then:

  1. Minimal objects are even.

  2. If \( \prec \) is well-founded, then every object \( x : \tau \) is either even or odd, but not both.

Proof

Part 1. Direct from the definition.

Part 2. We show this by induction along \( \prec \). Suppose that all \( \prec \)-predecessors of \( x \) are either even or odd but not both. If all of these \( \prec \)-predecessors are odd, then \( x \) is even, and it is clearly not odd, because no \( y \prec x \) is even. Otherwise, there is \( y \prec x \) that is even, so \( x \) is odd, and it is not even because this \( y \) is not odd.

We define the relation \( \looparrowright \) between codes by the following two constructors.

  • If \( c \) is a \( \prec \)-even code, then \( c \looparrowright c \).

  • If \( c \) is a \( \prec \)-even code and \( c \prec d \), then \( c \looparrowright d \).

This relation is cofunctional (definition A.1): if \( d \) is a code, there is exactly one \( c \) such that \( c \looparrowright d \). Moreover, if \( c \looparrowright (\beta , s_1), (\beta , s_2) \), then \( s_1 = s_2 \).

Proof of claim

If \( d \) is even, then \( d \looparrowright d \). If \( c \) is any other even code, \( c \nprec d \).

If \( d \) is odd, then there is an even code \( c \) with \( c \prec d \), so \( c \looparrowright d \). If \( c' \) is any other even code with \( c' \looparrowright d \), we must have \( c' \prec d \) as \( c' \) and \( d \) have different parities so cannot be equal, so \( c, c' \prec d \), so \( c = c' \) by proposition 3.4.

Finally, suppose \( c \looparrowright (\beta , s_1), (\beta , s_2) \). Suppose that \( c = (\beta , s_1) \). Then \( (\beta , s_1) \looparrowright (\beta , s_2) \) implies \( s_1 = s_2 \) because in the other constructor we may conclude \( \beta \neq \beta \). The same holds for \( c = (\beta , s_2) \) by symmetry. Now suppose that \( c \prec (\beta , s_1), (\beta , s_2) \). In this case, we immediately obtain \( s_1 = s_2 \) by proposition 3.3.

Proposition 3.8 extensionality

Let \( x : \mathsf{TSet}_\beta \) for some type index \( \beta {\lt} \alpha \), and let \( c \) be a code. We say that \( x \) is a type-\( \beta \) member of \( c \) if there is a set \( s : \operatorname {\mathsf{Set}}\mathsf{TSet}_\beta \) such that \( x \in s \) and \( c \looparrowright (\beta , s) \), and hence for all sets \( s : \operatorname {\mathsf{Set}}\mathsf{TSet}_\beta \) such that \( c \looparrowright (\beta , s) \), we have \( x \in s \) by definition 3.7. We write \( x \in _\beta c \). Note that this definition is only useful when \( c \) is even.

Let \( c_1, c_2 \) be even codes. If \( \beta {\lt} \alpha \) is a proper type index such that

\[ \forall x : \mathsf{TSet}_\beta ,\, x \in _\beta c_1 \leftrightarrow x \in _\beta c_2 \]

then \( c_1 = c_2 \).

Proof

Suppose that there is no \( x : \mathsf{TSet}_\beta \) such that \( x \in _\beta c_1 \). Then it is easy to check that \( c_1 = (\gamma , \emptyset ) \) for some \( \gamma \), which is a contradiction as all codes are assumed to have nonempty second projections.

So there is some \( x : \mathsf{TSet}_\beta \) such that \( x \in _\beta c_1 \). Then there are sets \( s_1, s_2 \) where \( c_i \looparrowright (\beta , s_i) \) for \( i = 1, 2 \). Then, as \( x \in _\beta c_i \) holds if and only if \( x \in s_i \), we conclude \( s_1 = s_2 \). Hence \( c_1, c_2 \looparrowright (\beta , s_1) \), so as \( \looparrowright \) is injective, we conclude \( c_1 = c_2 \).