Cardinals and coded injections inside L

Cardinality in L requires two related kinds of comparison. The host can compare the small types that present sets by actual functions, while a statement made inside L must be witnessed by a graph that is itself constructible. This chapter develops both notions and keeps their logical strength visible: concrete functions and graph codes carry data, whereas the cardinal comparisons used later retain only existence.

{-# OPTIONS --cubical --safe --guardedness #-}

The argument is carried out in the host language described in the prelude. Its one classical resource is excluded middle for propositions in Type (ℓ-suc ℓ). This is a level-bounded assumption, not an unrestricted excluded-middle or choice principle. The definitions of injections and graph codes do not themselves select witnesses; classical reasoning becomes relevant to the ordinal well-order and to the least-element arguments that use it later.

open import Base.Prelude
open import Base.Classical using ( LEM )

The universe level and this instance of excluded middle are therefore displayed as parameters of the whole chapter. Every construction below is relative to the same lem; no additional axiom is introduced along the way. The goal here is to prepare the precise notions and bounded order needed for later cardinal arguments, rather than to assert the existence of a cardinal representative or a successor cardinal already.

module L.Cardinal {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

Two mathematical settings will remain in view. The cumulative hierarchy supplies ambient sets and proposition-valued membership. The constructible model will supply the sets that belong to L and the relations interpreted over them. The elementary fact a ∈ sucV a, saying that every set belongs to its set-theoretic successor a ∪ {a}, will later provide a distinguished point in a bounded search.

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( self∈sucV )

An ambient set also has a canonical small presentation. Its indices name all of its members, member turns an index into membership, and fiber recovers an index from membership. Ordered pairs let a set represent a relation. On the constructible side, an element of the model pairs an ambient set with a certificate that it belongs to L; transitivity of L then carries constructibility from a set to each of its members. These facts will connect small presentations with constructible graph codes.

open import V.Presentation {ℓ} using ( member; fiber )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL )
open import L.Ordinal {ℓ} using ( suc-ord )

The bounded search will use the strict well-order induced by ordinal membership on a presentation. Its trichotomy ultimately uses lem, while its well-foundedness comes from regularity of ambient membership. The other ingredients describe graphs inside the object language: single-valuedness, exact domain, and injectivity. Keeping these order-theoretic and logical ingredients distinct will matter when a concrete graph code is later hidden by propositional truncation.

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.SquareLaw {ℓ} lem using ( ordSWO )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ} using ( SWO; module SWO )
open import L.Coding.Model {ℓ} using ( svAt; domAt )
open import L.Coding.Injection {ℓ} lem using ( injAt )

For a set a, write ⟪ a ⟫ for the small type indexing its members and ⟪ a ⟫↪ for the map sending an index to the member it names. The set-theoretic successor sucV a contains every member of a and also a itself. Thus ⟪ sucV a ⟫ is a small search space containing indices for all smaller ordinals when a is an ordinal, together with an index naming a.

open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )

Existence inside this development is often deliberately weakened by propositional truncation. A term of ∥ X ∥₁ states that X is inhabited but does not reveal an inhabitant. It may be eliminated into a proposition, such as the empty type used for a refutation, but not into arbitrary data. This rule will separate the concrete graph information in InjCode from the mere existence asserted by InjL.

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

The notation now records which setting a statement belongs to. For the ambient structure, _∈ˢ_ is proposition-valued membership between raw hierarchy sets. By contrast, S is the carrier of the constructible structure: an element a : S has an underlying ambient set fst a and a proposition-valued certificate of its constructibility. Thus ⟨ fst x ∈ˢ fst a ⟩ is a host-level proposition about underlying ambient sets, while a quantifier over x : S ranges only over constructible sets. Object-language syntax enters separately through the satisfaction relation introduced below.

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
open hPropStructure 𝒮ʟ using ( S )

The constructible structure also has a proposition-valued pointwise subset relation. A proof of ⟨ a ⊆ˢ b ⟩ takes each x : S and sends membership in a to membership in b; its quantifier therefore ranges over the constructible carrier. Transitivity of L ensures that this has the expected subset reading for the underlying sets. When a and b are ordinals, it is their non-strict order. That is why the minimality clause for a successor cardinal concludes by containment, while strict comparison is expressed by membership.

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( _⊆ˢ_ )

The satisfaction symbol _⊨_ is fixed to the interpretation in the constructible structure. In a judgment γ ⊨ φ, the environment γ lists elements of S, so the unbounded quantifiers in φ range over constructible sets. This is the semantic content of the first three conditions in InjCode; they are object-language statements true inside L, even though their proofs are handled in the host.

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

We first define an injection entirely at the host level. An element of X ↪ Y consists of a function f : X → Y together with a proof that equality of f x and f y implies equality of x and y. The function is concrete data and can be projected from the pair. No surjectivity or inverse is included, and no set, constructibility certificate, satisfaction judgment, or truncation occurs in this definition. Later its typical endpoints are the small presentation types of two ambient sets.

_↪_ : Type ℓ → Type ℓ → Type ℓ
X ↪ Y = Σ[ f ∈ (X → Y) ] ((x y : X) → f x ≡ f y → x ≡ y)

Now fix a constructible set α whose underlying set is an ordinal. To look later for a suitable ordinal no larger than necessary, it suffices to work in the canonical presentation of sucV (fst α). This set contains every member of α and α itself, so the search is both small and equipped with a natural starting point. The definitions here build this ordered search space; later arguments provide a candidate predicate and perform the least-element selection.

module LeastCardInjL (α : S) (oα : IsOrd (fst α)) where

The first obligation is to show that this set-theoretic successor itself belongs to L. From oα, two applications of ordinal successor show that sucV (sucV (fst α)) is an ordinal. The theorem that an ordinal belongs to the next constructible stage places sucV (fst α) in that named stage, and membership in a stage yields its constructibility. Thus the proof identifies a specific stage containing the successor; it does not appeal to a general closure of constructibility under sucV.

  hSucα : ⟨ isL (sucV (fst α)) ⟩
  hSucα = Lset→isL (sucV (sucV (fst α))) (suc-ord (suc-ord oα)) (sucV (fst α))
            (ord∈Lset-suc (sucV (fst α)) (suc-ord oα))

Every index m in the presentation names a member of sucV (fst α). Since that successor is constructible and L is transitive, the named member is constructible as well. The map up therefore keeps the underlying set named by m and adds precisely this certificate, producing an element of S. It is defined only on this bounded presentation and does not turn arbitrary ambient sets into constructible ones.

  up : ⟪ sucV (fst α) ⟫ → S
  up m = ⟪ sucV (fst α) ⟫↪ m
       , isL-trans (member (sucV (fst α)) m) hSucα

Ordinal membership orders these indices. Applying ordSWO to the ordinal sucV (fst α) gives a strict well-order w on ⟪ sucV (fst α) ⟫: its comparison follows membership between the named sets, its trichotomy depends on lem, and its well-foundedness follows from regularity. Declaring the value opaque controls later unfolding without changing the relation, its laws, or the assumptions on which they rest.

  opaque
    w : SWO (⟪ sucV (fst α) ⟫)
    w = ordSWO (sucV (fst α)) (suc-ord oα)

The usable description of this order is the path w-lt. For indices m and n, the proposition that m precedes n under w is identified with the proposition that the set named by m belongs to the set named by n. This is an equality of proposition types, not an equality of sets. It lets later proofs transport evidence in either direction between an index comparison and ordinal membership without unfolding the construction of the well-order.

  opaque
    unfolding w
    w-lt : (m n : ⟪ sucV (fst α) ⟫)
         → SWO._<∙_ w m n ≡ ⟨ ⟪ sucV (fst α) ⟫↪ m ∈ˢ ⟪ sucV (fst α) ⟫↪ n ⟩
    w-lt m n = refl

The search space has a distinguished index naming fst α. The proof self∈sucV (fst α) supplies membership of the ordinal in its set-theoretic successor, and fiber turns that membership into an index together with an equation describing its image. Although hierarchy membership is proposition-valued, the fiber of the presentation map is itself a proposition because the map is an embedding; truncation can therefore be eliminated into that unique fiber without invoking a choice principle. The term self is the recovered index, not the ordinal.

  self : ⟪ sucV (fst α) ⟫
  self = fiber (sucV (fst α)) (self∈sucV (fst α)) .fst

The companion equation states exactly what self names: its image under the presentation map is fst α. The equality is between underlying ambient sets. No equality of the corresponding elements of S is asserted here, since that would also have to identify their constructibility certificates. Together, self and self-eq give later searches a concrete index at which a property of α can be checked.

  self-eq : ⟪ sucV (fst α) ⟫↪ self ≡ fst α
  self-eq = fiber (sucV (fst α)) (self∈sucV (fst α)) .snd

Internal injections and successor cardinals

A concrete constructible set F begins to code an injection from a to b through three satisfaction conditions inside L. The first says that pair-shaped entries are single-valued: one input cannot have two unequal outputs. The second says that the domain is exactly a, in both directions: the first coordinate of every pair-shaped entry belongs to a, and every member of a merely has an output. The third says that the graph is injective: two entries with the same output have equal inputs. In all three judgments, the environment places F first and a second, and every unbounded quantifier ranges over S.

InjCode : S → S → S → Type (ℓ-suc ℓ)
InjCode F a b =
    ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩

The fourth condition is stated directly in the host. For any x,y : S, if the ordered pair of their underlying sets belongs to the underlying graph, then the underlying output belongs to b. Thus b is a codomain bound for the values; the condition does not say that every member of b is attained. Nor does InjCode assert that every member of F is an ordered pair. Its conditions inspect pair-shaped members, so additional members of another shape do not affect the function read from the code. This host-level range condition must therefore be distinguished from the preceding three object-language satisfaction judgments.

  × ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst b ⟩)

InjL a b forgets which concrete graph supplies these four conditions. It is the propositional truncation of the dependent pair consisting of F and InjCode F a b, so it states merely that a coded injection from a to b exists inside L. A particular graph or host-level function cannot be projected from it. It may be opened locally only when the target is a proposition; later constructions that compose or transform injections work with the graph inside such a branch and place the resulting graph back under truncation. The direction is part of the statement: InjL a b says nothing by itself about InjL b a.

InjL : S → S → Type (ℓ-suc ℓ)
InjL a b = ∥ Σ[ F ∈ S ] InjCode F a b ∥₁

For an ordinal κ, cardinality is expressed by initiality. Every member δ of a von Neumann ordinal is a smaller ordinal, and IsCardinalL κ refutes the propositionally truncated existence of a constructible graph satisfying InjCode F κ δ. In the notation just defined, it rules out InjL κ δ; it does not rule out InjL δ κ. These are internal coded-injection propositions, not instances of the host-level type _↪_, and the latter cannot in general be extracted from their truncations. The definition can also be formed for a general constructible set and contains no proof that κ is an ordinal; later uses supply IsOrd (fst κ) separately before giving it the initial-ordinal interpretation. Since a refutation has the empty type as its target, any needed elimination of the propositional truncation is legitimate.

IsCardinalL : S → Type (ℓ-suc ℓ)
IsCardinalL κ =
  (δ : S) → ⟨ fst δ ∈ fst κ ⟩
          → (∥ Σ[ F ∈ S ] InjCode F κ δ ∥₁ → Empty.⊥)

The arguments of SuccCardL δ κ are ordered so that δ is the proposed successor cardinal and κ is the object it lies above. The first three clauses say that the underlying set of δ is an ordinal, that δ satisfies the initiality predicate, and that κ ∈ δ, hence that δ lies strictly above κ in the ordinal setting. These clauses describe a property of a given pair and do not produce such a δ; they also do not require κ itself to be an ordinal or a cardinal. The continuation adds the remaining global minimality clause. No sucV occurs here: a successor cardinal is not the set-theoretic successor κ ∪ {κ}.

SuccCardL : S → S → Type (ℓ-suc ℓ)
SuccCardL δ κ =
    IsOrd (fst δ)
  × IsCardinalL δ
  × ⟨ fst κ ∈ fst δ ⟩

The final field expresses minimality among all internal ordinal cardinals above κ. Given any c : S whose underlying set is an ordinal, which satisfies IsCardinalL c, and which contains κ, it returns the internal inclusion δ ⊆ˢ c. The first field has already established that δ is an ordinal, so inclusion is the non-strict ordinal comparison: δ lies at or below every such c. Inclusion rather than membership is essential here, since the conclusion must also hold when c is δ itself. Both the quantifier over S and _⊆ˢ_ belong to the constructible carrier, so this is minimality among the candidates visible in L. The field assumes only κ ∈ c; hypotheses saying that κ is itself an ordinal and an internal cardinal are supplied at the theorems that use this predicate.

No injection graph is constructed by this field. InjCode F a b retains a particular constructible code F together with its four injection conditions, whereas InjL a b is the propositional truncation ∥ Σ[ F ∈ S ] InjCode F a b ∥₁. Thus the hypothesis IsCardinalL c, when combined with the ordinal hypothesis on c, says that c cannot merely admit such a coded injection into any smaller ordinal belonging to it. SuccCardL δ κ is itself an untruncated property of the fixed pair δ, κ: it neither proves that a suitable δ exists nor chooses one. Later, succCardExists proves the propositionally truncated existence of such a δ when κ is an ordinal internal cardinal and is not finite, using only the module's assumption LEM (ℓ-suc ℓ). The set-theoretic successor sucV does not occur in this definition.

  × ((c : S) → IsOrd (fst c) → IsCardinalL c → ⟨ fst κ ∈ fst c ⟩
             → ⟨ δ ⊆ˢ c ⟩)