New Foundations is consistent

2.5 Hypotheses of the recursion

Definition 2.20 model data
#

Let \( \alpha \) be a type index. Model data at type \( \alpha \) consists of: 1

  • a \( \mathsf{TSet}_\alpha \) called the type of tangled sets or t-sets, which will be our type of model elements at level \( \alpha \), with an embedding \( U_\alpha : \mathsf{TSet}_\alpha \to \mathsf{StrSet}_\alpha \);

  • a group \( \mathsf{AllPerm}_\alpha \) called the type of allowable permutations, with a \( \texttt{StrPermClass}_\alpha \) instance and a specified action on \( \mathsf{TSet}_\alpha \),

such that

  • if \( \rho : \mathsf{AllPerm}_\alpha \) and \( x : \mathsf{TSet}_\alpha \), then \( \rho (U_\alpha (x)) = U_\alpha (\rho (x)) \);

  • every t-set of type \( \alpha \) has an \( \alpha \)-support (definition 2.15) for its action under the \( \alpha \)-allowable permutations.

Definition 2.21 tangle
#

Let \( \alpha \) be a type index with model data. An \( \alpha \)-tangle is a pair \( t = (x, S) \) where \( x \) is a tangled set of type \( \alpha \) and \( S \) is an \( \alpha \)-support for \( x \). We define \( \operatorname {\mathsf{set}}(t) = x \) and \( \operatorname {\mathsf{supp}}(t) = S \). The type of \( \alpha \)-tangles is denoted \( \mathsf{Tang}_\alpha \). Allowable permutations \( \rho \) act on tangles by \( \rho ((x, S)) = (\rho (x), \rho (S)) \), and so \( \operatorname {\mathsf{supp}}(t) \) supports \( t \) for its action under the allowable permutations. Therefore, each tangled set \( x \) is of the form \( \operatorname {\mathsf{set}}(t) \) for some tangle \( t \).

Proposition 2.22 fuzz maps

Let \( \beta \) be a type index with model data, and suppose that \( \mathsf{Tang}_\beta \) has a position function. Let \( \gamma \) be any proper type index not equal to \( \beta \). Then there is an injective fuzz map \( f_{\beta ,\gamma } : \mathsf{Tang}_\beta \to {\mathcal L}\) such that \( \iota (t) {\lt} \iota (f_{\beta ,\gamma }(t)) \), and the different \( f_{\beta ,\gamma } \) all have disjoint ranges. In particular, for any near-litter \( N \) with \( N^\circ = f_{\beta ,\gamma }(t) \), we have \( \iota (t) {\lt} \iota (N) \), and additionally, for any atom \( a \) with \( a^\circ = f_{\beta ,\gamma }(t) \), we have \( \iota (t) {\lt} \iota (a) \). 2

Proof

We define \( g : \mathsf{Tang}_\beta \to \mu \) by proposition 2.18, where the denied sets are given by \( D(t) = \{ \iota (t) \} \). Then we set \( f_{\beta ,\gamma }(t) = (g(t), \beta , \gamma ) \).

Definition 2.23 inflexible path
#

Let \( \alpha \) be a proper type index. Suppose that we have model data for all type indices \( \beta \leq \alpha \) and position functions for \( \mathsf{Tang}_\beta \) for all \( \beta {\lt} \alpha \). For any type index \( \beta \leq \alpha \), a inflexible \( \beta \)-path is a tuple \( I = (\gamma , \delta , \varepsilon , A) \) where \( \delta , \varepsilon {\lt} \gamma \) are distinct, the index \( \varepsilon \) is proper, and \( A : \beta \rightsquigarrow \gamma \). We will write \( \gamma _I, \delta _I, \varepsilon _I, A_I \) for its fields. Inflexible paths have a coderivative operation, given by \( (\gamma , \delta , \varepsilon , A)^B = (\gamma , \delta , \varepsilon , A^B) \).

Definition 2.24 typed near-litter

Let \( \alpha \) be a proper type index with model data, and suppose that \( \mathsf{Tang}_\alpha \) has a position function. We say that \( \alpha \) has typed near-litters if there is an embedding \( \operatorname {\mathsf{typed}}_\alpha : {\mathcal N}\to \mathsf{TSet}_\alpha \) such that

  • if \( \rho : \mathsf{AllPerm}_\alpha \) and \( N : {\mathcal N}\), then \( \rho (\operatorname {\mathsf{typed}}_\alpha (N)) = \operatorname {\mathsf{typed}}_\alpha (\rho _\bot (N)) \); and

  • if \( N \) is a near-litter and \( t \) is an \( \alpha \)-tangle such that \( \operatorname {\mathsf{set}}(t) = \operatorname {\mathsf{typed}}_\alpha (N) \), we have \( \iota (N) \leq \iota (t) \).

Objects of the form \( \operatorname {\mathsf{typed}}_\alpha \) are called typed near-litters.

Definition 2.25 coherent data
#

Let \( \alpha \) be a proper type index. Suppose that we have model data for all type indices \( \beta \leq \alpha \), position functions for \( \mathsf{Tang}_\beta \) for all \( \beta {\lt} \alpha \), and typed near-litters for all \( \beta {\lt} \alpha \). We say that the model data is coherent below level \( \alpha \) if the following hold.

  • For \( \gamma {\lt} \beta \leq \alpha \), there is a map \( \mathsf{AllPerm}_\beta \to \mathsf{AllPerm}_\gamma \) that commutes with the coercions from \( \mathsf{AllPerm}_{(-)} \) to \( \mathsf{StrPerm}_{(-)} \). We can use this map to define arbitrary derivatives of allowable permutations by recursion on paths.

  • If \( (x, S) \) is a \( \beta \)-tangle for \( \beta {\lt} \alpha \), and \( y \) is an atom or near-litter that occurs in the range of \( S_A \), then \( \iota (y) {\lt} \iota (x, S) \).

  • Let \( \beta \leq \alpha \), and let \( \gamma , \delta {\lt} \beta \) be distinct with \( \delta \) proper. Let \( t : \mathsf{Tang}_\gamma \) and \( \rho : \mathsf{AllPerm}_\beta \). Then

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

    In particular, for every \( \beta \leq \alpha \), \( \beta \)-allowable permutation \( \rho \), and \( \beta \)-inflexible path \( I \), we obtain

    \[ ((\rho _A)_\varepsilon )_\bot (f_{\delta ,\varepsilon }(t)) = f_{\delta ,\varepsilon }((\rho _A)_\delta (t)) \]

    where subscripts of \( I \) are suppressed.

  • Suppose that \( \beta \leq \alpha \) and \( (\rho (\gamma ))_{\gamma {\lt} \beta } \) is a collection of allowable permutations such that whenever \( \gamma , \delta {\lt} \beta \) are distinct, \( \delta \) is proper, and \( t : \mathsf{Tang}_\delta \), we have

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

    Then there is a \( \beta \)-allowable permutation \( \rho \) with \( \rho _\gamma = \rho (\gamma ) \) for each \( \gamma {\lt} \beta \).

  • If \( \beta \leq \alpha \) is a proper type index and \( x : \mathsf{TSet}_\beta \), then for any \( \gamma {\lt} \beta \),

    \[ U_\beta (x)(\gamma ) \subseteq \operatorname {\mathsf{ran}}U_\gamma \]
  • (extensionality) If \( \beta , \gamma \leq \alpha \) are proper type indices where \( \gamma {\lt} \beta \), the map \( U_\beta (-)(\gamma ) : \mathsf{TSet}_\beta \to \operatorname {\mathsf{Set}}\mathsf{StrSet}_\gamma \) is injective.

  • If \( \beta , \gamma : \lambda \) where \( \gamma {\lt} \beta \), for every \( x : \mathsf{TSet}_\gamma \) there is some \( y : \mathsf{TSet}_\beta \) such that \( U_\beta (y)(\gamma ) = \{ x \} \). We write \( \operatorname {\mathsf{singleton}}_\beta (x) \) for this object \( y \), which is uniquely defined by extensionality.

Note that this structure contains data (the derivative maps for allowable permutations and the singleton operations), but the type is a subsingleton: any two inhabitants are propositionally equal. We will not use this fact directly, but the idea will have relevance in chapter 6.

The strategy of our construction is as follows.

  • In chapter 3, we assume model data, position functions, and typed near-litters for all types \( \beta {\lt} \alpha \), and construct model data at level \( \alpha \).

  • In ??, we assume coherent data below level \( \alpha \) (along with the assumptions required for this definition to make sense) and prove that \( \# \mathsf{TSet}_\alpha = \# \mu \).

  • In chapter 6, we use the results of ?? to show that we can provide position functions and typed near-litters at level \( \alpha \). We then show that these constructions may be iterated so that we may define all of the above structures at every proper type level.

  1. A type theory problem with exporting this data is that under different assumptions, things like different spellings of \( \mathsf{TSet}_\alpha \) might require case splitting on \( \alpha \) before they become defeq (e.g. see the old version of Model/FOA.lean). There doesn’t seem to be an easy way around this.
  2. We might want to encapsulate atoms and near-litters somehow. We could make a typeclass, or write theorems in terms of the coproduct \( {\mathcal A}\oplus {\mathcal N}\).