New Foundations is consistent

7.2 Tangled type theory

Definition 7.6 tangled membership
#

We define the membership relation \( \in ^\alpha _\beta : \mathsf{TSet}_\beta \to \mathsf{TSet}_\alpha \to \mathsf{Prop}\) by

\[ x \in ^\alpha _\beta y \leftrightarrow U_\beta (x) \in U_\alpha (y)(\beta ) \]

Extensionality holds at all proper type indices by proposition 3.8. Also, for every \( \alpha \)-allowable \( \rho \), we have

\[ \rho _\beta (x) \in ^\alpha _\beta \rho (y) \leftrightarrow x \in ^\alpha _\beta y \]
Definition 7.7 symmetric
#

Let \( \beta {\lt} \alpha \) be proper type indices. A set \( s : \mathsf{TSet}_\beta \) is called \( \alpha \)-symmetric if there is some \( \alpha \)-support \( S \) such that if \( \rho \) is an \( \alpha \)-allowable permutation that fixes \( S \), then \( \rho \) fixes \( s \) setwise. Note that it suffices to prove that for all \( \rho \) that fix \( S \), \( s \subseteq \rho [s] \) (or alternatively, \( \rho [s] \subseteq s \)). Every small set is symmetric, since a support can be obtained by raising the types of chosen supports for elements of the set and then collating the results.

Proposition 7.8

Let \( \beta {\lt} \alpha \) be proper type indices. Let \( s : \mathsf{TSet}_\beta \) be \( \alpha \)-symmetric. Then there is \( x : \mathsf{TSet}_\alpha \) such that

\[ \forall y : \mathsf{TSet}_\beta ,\, y \in _\beta ^\alpha x \leftrightarrow y \in s \]

Moreover, every \( x : \mathsf{TSet}_\alpha \) arises in this way; this is an induction principle for \( \mathsf{TSet}_\alpha \).

Proof

If \( s \) is empty, the result follows directly from the definition of \( \mathsf{TSet}_\alpha \). Otherwise, consider the code \( (\beta , s) \). By definition 3.7, there is exactly one code \( d \) such that \( c \looparrowright (\beta , s) \). Then \( c \) is a new t-set at level \( \alpha \), so is naturally an inhabitant of \( \mathsf{TSet}_\alpha \). Using the membership relation from proposition 3.8, the type-\( \beta \) members of \( c \) are precisely \( s \), as required.

For the induction principle, we apply the above construction to the set

\[ s = \{ y \mid y \in ^\alpha _\beta x \} \]

and use extensionality to deduce that the object constructed is exactly \( x \).

Proposition 7.9 unions of singletons

Let \( \gamma {\lt} \beta {\lt} \alpha \) be proper type indices. Let \( s : \operatorname {\mathsf{Set}}\mathsf{TSet}_\gamma \) be such that \( \operatorname {\mathsf{singleton}}_\beta [s] \) is \( \alpha \)-symmetric. Then \( s \) is \( \beta \)-symmetric.

Proof

Let \( S \) be an \( \alpha \)-support for \( \operatorname {\mathsf{singleton}}_\beta [s] \), which without loss of generality is strong. We claim that the \( \alpha \)-symmetry of \( s \) is witnessed by \( S_\beta \). Let \( \rho \) be a \( \beta \)-allowable permutation such that \( \rho (S_\beta ) = S_\beta \). Let \( x \in s \); it suffices by substituting \( \rho ^{-1} \) to prove that \( \rho _\gamma (x) \in s \). As \( x : \mathsf{TSet}_\gamma \), there is a \( \gamma \)-support \( T \) for \( x \). By proposition 7.5, there is an \( \alpha \)-allowable permutation \( \rho ' \) such that

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

Thus,

\[ \rho '_\beta (\operatorname {\mathsf{singleton}}_\beta [s]) = \operatorname {\mathsf{singleton}}_\beta [s];\quad (\rho '_\beta )_\gamma (x) = \rho _\gamma (x) \]

We thus have

\begin{align*} x & \in s \\ \operatorname {\mathsf{singleton}}_\beta (x) & \in \operatorname {\mathsf{singleton}}_\beta [s] \\ \rho ’_\beta (\operatorname {\mathsf{singleton}}_\beta (x)) & \in \rho ’_\beta (\operatorname {\mathsf{singleton}}_\beta [s]) \\ \rho ’_\beta (\operatorname {\mathsf{singleton}}_\beta (x)) & \in \operatorname {\mathsf{singleton}}_\beta [s] \\ \operatorname {\mathsf{singleton}}_\beta ((\rho ’_\beta )_\gamma (x)) & \in \operatorname {\mathsf{singleton}}_\beta [s] \\ \operatorname {\mathsf{singleton}}_\beta (\rho _\gamma (x)) & \in \operatorname {\mathsf{singleton}}_\beta [s] \\ \rho _\gamma (x) & \in s \\ \end{align*}
Theorem 7.10 consistency of tangled type theory

Let \( \{ x \} _\beta \) be an abbreviation for \( \operatorname {\mathsf{singleton}}_\beta (x) \), and let \( \langle x, y \rangle _{\gamma ,\beta } \) be an abbreviation for \( \{ \{ x \} _\gamma , \{ x, y \} _\gamma \} _\beta \). Then, the following axioms hold for our model \( \mathsf{TSet}\) at all sequences of proper type indices \( \zeta {\lt} \varepsilon {\lt} \delta {\lt} \gamma {\lt} \beta {\lt} \alpha \).

\( - \)

extensionality

\( \forall x^\alpha ,\, \forall y^\alpha ,\, (\forall z^\beta ,\, z \in x \leftrightarrow z \in y) \to x = y \)

P1(a)

intersection

\( \forall x^\alpha y^\alpha ,\, \exists z^\alpha ,\, \forall w^\beta ,\, w \in z \leftrightarrow (w \in x \wedge w \in y) \)

P1(b)

complement

\( \forall x^\alpha ,\, \exists z^\alpha ,\, \forall w^\beta ,\, w \in z \leftrightarrow w \notin x \)

\( - \)

singleton

\( \forall x^\beta ,\, \exists y^\alpha ,\, \forall z^\beta ,\, z \in y \leftrightarrow z = x \)

P2

singleton image

\( \forall x^\beta ,\, \exists y^\alpha ,\, \forall z^\varepsilon w^\varepsilon ,\, \langle \{ z \} _\delta , \{ w \} _\delta \rangle _{\gamma ,\beta } \in y \leftrightarrow \langle z, w \rangle _{\delta ,\gamma } \in x \)

P3

insertion two

\( \forall x^\gamma ,\, \exists y^\alpha ,\, \forall z^\zeta w^\zeta t^\zeta ,\, \langle \{ \{ z \} _\varepsilon \} _\delta , \langle w, t \rangle _{\varepsilon , \delta } \rangle _{\gamma ,\beta } \in y \leftrightarrow \langle z, t \rangle _{\varepsilon ,\delta } \in x \)

P4

insertion three

\( \forall x^\gamma ,\, \exists y^\alpha ,\, \forall z^\zeta w^\zeta t^\zeta ,\, \langle \{ \{ z \} _\varepsilon \} _\delta , \langle w, t \rangle _{\varepsilon ,\delta } \rangle _{\gamma ,\beta } \in y \leftrightarrow \langle z, w \rangle _{\varepsilon ,\delta } \in x \)

P5

cross product

\( \forall x^\gamma ,\, \exists y^\alpha ,\, \forall z^\beta ,\, z \in y \leftrightarrow \exists w^\delta t^\delta ,\, z = \langle w, t \rangle _{\gamma ,\beta } \wedge t \in x \)

P6

type lowering

\( \forall x^\alpha ,\, \exists y^\delta ,\, \forall z^\varepsilon ,\, z \in y \leftrightarrow \forall w^\delta ,\, \langle w, \{ z \} _\delta \rangle _{\gamma ,\beta } \in x \)

P7

converse

\( \forall x^\alpha ,\, \exists y^\alpha ,\, \forall z^\delta w^\delta ,\, \langle z, w \rangle _{\gamma ,\beta } \in y \leftrightarrow \langle w, z \rangle _{\gamma ,\beta } \in x \)

P8

cardinal one

\( \exists x^\alpha ,\, \forall y^\beta ,\, y \in x \leftrightarrow \exists z^\gamma ,\, \forall w,\, w \in y \leftrightarrow w = z \)

P9

subset

\( \exists x^\alpha ,\, \forall y^\delta z^\delta ,\, \langle y, z \rangle _{\gamma ,\beta } \in x \leftrightarrow \forall w^\varepsilon ,\, w \in y \to w \in z \)

Proof

The axiom of extensionality was proven in proposition 3.8. All axioms except for the type lowering axiom can be easily proven using proposition 7.8. For type lowering, consider the set

\[ y' = \{ \{ \{ \{ z^\varepsilon \} _\delta \} _\gamma \} _\beta \mid \forall w^\delta ,\, \langle w, \{ z \} _\delta \rangle _{\gamma ,\beta } \in x \} \]

which exists by proposition 7.8, and then apply proposition 7.9 three times.