New Foundations is consistent

2.2 Model parameters

Definition 2.1 model parameters
#

A collection of model parameters is a tuple \( (\lambda , {{\lt}_\lambda }, \kappa , \mu ) \) such that

  • \( {{\lt}} = {{\lt}_\lambda } \) is a well-order on \( \lambda \), and under this ordering, \( \lambda \) has no maximal element (so \( \operatorname {\mathsf{ot}}(\lambda ) \) is a limit ordinal);

  • \( \# \kappa \) is uncountable and regular;

  • \( \# \mu \) is a strong limit, and satisfies

    \[ \# \kappa {\lt} \# \mu ;\quad \# \kappa \leq \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu ));\quad \operatorname {\mathsf{ot}}(\lambda ) \leq \operatorname {\mathsf{ord}}(\operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu ))) \]

    so in particular, \( \operatorname {\mathsf{ot}}(\lambda ) \leq \operatorname {\mathsf{ord}}(\# \mu ) \). Note that the inequalities in \( \kappa \) are inequalities of cardinals; the inequality in \( \lambda \) is an inequality of ordinals.

Given a collection of model parameters, we define

  • canonical well-orders on \( \kappa \) and \( \mu \) such that \( \operatorname {\mathsf{ot}}(\kappa ) = \operatorname {\mathsf{ord}}(\# \kappa ) \) and \( \operatorname {\mathsf{ot}}(\mu ) = \operatorname {\mathsf{ord}}(\# \mu ) \); and

  • a canonical left-cancellative additive monoid on \( \kappa \), obtained by passing through the equivalence \( \kappa \simeq \{ o : \mathsf{Ord}\mid o {\lt} \operatorname {\mathsf{ord}}(\# \kappa ) \} \).

Proposition 2.2

The tuple \( (\mathbb N, {{\lt}_{\mathbb N}}, \aleph _1, \beth _{\omega _1}) \) is a collection of model parameters, where the symbols \( \aleph _1 \) and \( \beth _{\omega _1} \) represent particular types of that cardinality.

Proof

Direct.

Definition 2.3 type index
#

The type of type indices is \( \lambda ^\bot :=\texttt{WithBot}(\lambda ) \): the collection of proper type indices \( \lambda \) together with a designated symbol \( \bot \) which is smaller than all proper type indices. Note that \( \operatorname {\mathsf{ot}}(\lambda ^\bot ) = \operatorname {\mathsf{ot}}(\lambda ) \), and hence that for each \( \alpha : \lambda ^\bot \),

\[ \# \{ \beta : \lambda ^\bot \mid \beta {\lt} \alpha \} \leq \# \{ \beta : \lambda ^\bot \mid \beta \leq \alpha \} {\lt} \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \]
Definition 2.4 small
#

A set \( s : \operatorname {\mathsf{Set}}(\tau ) \) is called small if \( \# s {\lt} \# \kappa \). Smallness is stable under subset, intersection, small-indexed unions, symmetric difference, direct image, injective preimage, and many other operations (each of which should be its own lemma when formalised). Sets \( s, t : \operatorname {\mathsf{Set}}(\tau ) \) are called near if \( s \mathrel {\triangle }t \) is small; in this case, we write \( s \mathrel {\overset {N}{\sim }}t \). Nearness is an equivalence relation. If \( s \mathrel {\overset {N}{\sim }}t \) and \( u \) is small, then \( s \mathrel {\overset {N}{\sim }}(t \mathbin {\diamond } u) \), where \( \diamond \) is one of \( \cup , \cap , \setminus , \mathrel {\triangle }\).

Definition 2.5 litter
#

A litter is a triple \( L = (\nu , \beta , \gamma ) : \mu \times \lambda ^\bot \times \lambda \) where \( \beta \neq \gamma \). The type of all litters is denoted \( {\mathcal L}\), and \( \# {\mathcal L}= \# \mu \).

Definition 2.6 atom
#

An atom is a pair \( a = (L, i) : {\mathcal L}\times \kappa \). 1 The type of all atoms is denoted \( {\mathcal A}\), and \( \# {\mathcal A}= \# \mu \). We write \( (-)^\circ : {\mathcal A}\to {\mathcal L}\) for the operation \( (L, i) \mapsto L \). 2 We write \( \operatorname {\mathsf{LS}}(L) :=\{ a \mid a^\circ = L \} \) for the litter set of \( L \). 3

Definition 2.7 near-litter
#

A near-litter is a pair \( N = (L, s) : {\mathcal L}\times \operatorname {\mathsf{Set}}{\mathcal A}\) such that \( s \mathrel {\overset {N}{\sim }}\operatorname {\mathsf{LS}}(L) \). 4 We write \( (-)^\circ : {\mathcal N}\to {\mathcal L}\) for the operation \( (L, s) \mapsto L \). We write \( a \in N \) for \( a \in s \), where \( N = (L, s) \). Near-litters satisfy extensionality: there is at most one choice of \( L \) for each \( s \). Each near-litter has size \( \# \kappa \) when treated as a set of atoms. The type of all near-litters is denoted \( {\mathcal N}\), and \( \# {\mathcal N}= \# \mu \) (there are \( \# \mu \) litters, and \( \# \mu \) small sets of atoms by lemma A.6; the latter observation should be its own lemma).

We have \( M \mathrel {\overset {N}{\sim }}N \) if and only if \( M^\circ = N^\circ \). If \( M^\circ = N^\circ \), then \( M \mathrel {\triangle }N \) is small and \( M \cap N \) has size \( \# \kappa \). If \( M^\circ \neq N^\circ \), then \( M \cap N \) has size \( \# \kappa \) and \( M \cap N \) is small.

Definition 2.8 base permutation
#

A base permutation is a pair \( \pi = (\pi ^{\mathcal A}, \pi ^{\mathcal L}) \), where \( \pi ^{\mathcal A}\) is a permutation \( {\mathcal A}\simeq {\mathcal A}\) and \( \pi ^{\mathcal L}\) is a permutation \( {\mathcal L}\simeq {\mathcal L}\), such that

\[ \pi ^{\mathcal A}[\operatorname {\mathsf{LS}}(L)] \mathrel {\overset {N}{\sim }}\operatorname {\mathsf{LS}}(\pi ^{\mathcal L}(L)) \]

Base permutations have a natural group structure, they act on atoms by \( \pi ^{\mathcal A}\), they act on litters by \( \pi ^{\mathcal L}\), and they act on near-litters by 5

\[ \pi (N)^\circ = \pi (N^\circ );\quad a \in \pi (N) \leftrightarrow a \in \pi [N] \]

Base permutations are determined by their action on atoms. We should avoid directly referencing \( \pi ^{\mathcal A}\) and \( \pi ^{\mathcal L}\) whenever possible.

  1. This should be formalised as a structure, not as a definition. We should not use the projections of atoms unless absolutely necessary.
  2. This must be a notation typeclass.
  3. Maybe revise this name?
  4. Like with atoms, this should be a structure. We should create an actual constructor, rather than using the \( \langle - \rangle \) syntax.
  5. We need to emphasise these properties, rather than emphasising the real definition \( \pi (N) = (\pi (N^\circ ), \pi [N]) \).