New Foundations is consistent

3.2 Model data defined

Definition 3.9 new allowable permutation
#

Uses

A new allowable permutation is a dependent function \( \rho \) of type \( \prod _{\beta {\lt} \alpha } \mathsf{AllPerm}_\beta \), subject to the condition

\[ (\rho _\gamma )_\bot (f_{\beta ,\gamma }(t)) = f_{\beta ,\gamma }(\rho (\beta )(t)) \]

for every \( t : \mathsf{Tang}_\beta \). These form a group and have a \( \texttt{StrPermClass}_\alpha \) instance.

Proposition 3.10
#

Uses

Define an action of allowable permutations on codes by

\[ \rho (\beta , s) = (\beta , \rho (\beta )[s]) \]

Then

  1. \( c \prec d \) implies \( \rho (c) \prec \rho (d) \);

  2. \( c \looparrowright d \) implies \( \rho (c) \looparrowright \rho (d) \);

  3. \( c \) is even if and only if \( \rho (c) \) is even;

  4. \( x \in _\beta c \) if and only if \( \rho (\beta )(x) \in _\beta \rho (c) \).

Proof ▶

Part 1. Suppose that \( c \prec d \). Then, writing \( c = (\beta , s) \) and \( d = (\gamma , s') \), we obtain

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

Now, note that

\begin{align*} \rho (\gamma )[s’] & = \rho (\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) \} ] \\ & = \{ \rho (\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) \} \\ & = \{ \operatorname {\mathsf{typed}}_\gamma (\rho (\gamma )_\bot (N)) \mid \exists t : \mathsf{Tang}_\beta ,\, \operatorname {\mathsf{set}}(t) \in s \wedge N^\circ = f_{\beta ,\gamma }(t) \} \\ & = \{ \operatorname {\mathsf{typed}}_\gamma (N) \mid \exists t : \mathsf{Tang}_\beta ,\, \operatorname {\mathsf{set}}(t) \in s \wedge \rho (\gamma )_\bot ^{-1}(N)^\circ = f_{\beta ,\gamma }(t) \} \\ & = \{ \operatorname {\mathsf{typed}}_\gamma (N) \mid \exists t : \mathsf{Tang}_\beta ,\, \operatorname {\mathsf{set}}(t) \in s \wedge N^\circ = \rho (\gamma )_\bot (f_{\beta ,\gamma }(t)) \} \\ & = \{ \operatorname {\mathsf{typed}}_\gamma (N) \mid \exists t : \mathsf{Tang}_\beta ,\, \operatorname {\mathsf{set}}(t) \in s \wedge N^\circ = f_{\beta ,\gamma }(\rho (\beta )(t)) \} \end{align*}

So \( \rho (c) \prec \rho (d) \) as required.

Part 2. Direct.

Part 3. Follows from the general fact that if \( f : \tau \to \sigma \) is a bijection and we have \( x \prec _\tau y \) if and only if \( f(x) \prec _\sigma f(y) \), then the \( \prec _\tau \)-parity of \( x \) is the same as the \( \prec _\sigma \)-parity of \( f(x) \).

Part 4. We only need to show one direction, because we can apply the one-directional result to \( \rho ^{-1} \) to obtain the converse. Suppose that \( x \in _\beta c \), so \( c \looparrowright (\beta , s) \) and \( x \in s \). Then \( \rho (c) \looparrowright (\beta , \rho (\beta )[s]) \), so \( \rho (\beta )(x) \in _\beta \rho (c) \) as required,

Definition 3.11 new t-set
#

Uses

A new t-set is an even code \( c \) such that there is an \( \alpha \)-support that supports \( c \) under the action of new allowable permutations, or a designated object called the empty set. New allowable permutations act on new t-sets in the same way that they act on codes, and map the empty set to itself. We define the map \( U_\alpha \) from new t-sets to \( \mathsf{StrSet}_\alpha \) by cases from the top of the path in the obvious way (using recursion on paths and the membership relation from proposition 3.8). It is easy to check that \( \rho (U_\alpha (x)) = U_\alpha (\rho (x)) \) by proposition 3.10.

Definition 3.12 new model data
#

Uses

Given model data, position functions, and typed near-litters for all types \( \beta {\lt} \alpha \), new model data is the model data at level \( \alpha \) consisting of new t-sets (definition 3.11) and new allowable permutations (definition 3.9). The embedding from new t-sets to \( \mathsf{StrSet}_\alpha \) is defined by

\[ U_\alpha (c)(\beta ) = \{ x \mid x \in _\beta c \} \]