Choice by a transversal

Read this chapter directly, or use the reading guide and dependency map to choose another route.

Reading guide · Dependency map

This chapter proves the axiom of choice for 𝒮ʟ by separating the least member of every cell under a stage-bounded internal well-order and showing that the resulting set meets each pairwise-disjoint cell exactly once.

This chapter proves the axiom of choice at 𝒮ʟ in the transversal form used by the model record: given a set whose members are inhabited and pairwise disjoint, merely a set meeting each member in exactly one point.

The argument follows the classical proof, with its most laborious step already carried out earlier. The textbook well-orders the universe and takes the least member of every cell. A well-order of all of L is a relation on a proper class, and this book never built one; what the previous chapters built instead is a well-order of each stage, uniformly, and, at every ordinal, as an element of the model. That is enough, because a set is small. One ordinal bounds a family, its members and their members all at once, and inside the tower at that ordinal the choosing is an ordinary least-element search.

So the chapter is four moves. The bound: the stage chapter's bounding ordinal for the family, above the family's own stage and hence above every member of every member of it. The order there: the table's relation at that ordinal, an element of the model, with two lemmas reading membership in it against the meta comparison in both directions. The description: "some member of the family contains this set, and nothing in that member precedes it", a formula with the order as a constant, which the model's own separation cuts a set out with. The count: that set meets each member in exactly one point, existence from the least element and uniqueness from pairwise disjointness, which is what disjointness is for and the only place the book uses it.

There is a fifth thing, and it is an observation rather than a move. Choice is stated relative to a ZF model on this carrier, because the intersection it names is that model's derived operation; and the whole of that dependence is one transport along the intersection's specification.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∃̇_ )
import FOL.ZFModel
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset→isL )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( bound-below₂ )
open import L.Choice.StageOrders {ℓ} lem using ( Mem; relOf )
open import L.Choice.InternalWellOrder {ℓ} lem using ( module Bound )
open import L.Coding.Model {ℓ} using ( appC; appC-adequate )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( SWO; IsLeast; isPropLeastOf; leastOf )

open import Cubical.Data.Sigma using ( Σ≡Prop )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( isZFModel )

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

The description

Pick is the one-variable formula saying that a point lies in a member of the family and has no predecessor there under the chosen relation.

One formula, one free variable, two constants. Of a set z it says: some member of the family contains z, and nothing in that member precedes z under the order. The application atom takes the order directly as a constant. The family is likewise named directly, since it appears only under a membership atom.

The formula is sealed, by the standing law that a description read at constants is sealed where it is built. Here that law is free rather than decisive: sealed and unsealed both check in 2.3 s, and the chapter says so rather than borrowing someone else's number. The reason is worth one line, because it says what the earlier measurements were really about. Those descriptions carried coded syntax inside them, and each satisfaction at a concrete environment normalized a whole hierarchy description; this one carries four atoms and one application, so there is nothing large to unfold. The seal stays, because it costs nothing and because a later reader of this description should not have to re-measure.

Perf: sealed by the standing law (a description read at constants), though measured here at 2.3 s either way: this description names no coded syntax.

opaque
  Pick : S → S → Formula S 1
  Pick c r =
    ∃̇ ( (var zero ∈̇ con c)
      ∧̇ ( (var (suc zero) ∈̇ var zero)
        ∧̇ (¬̇ ∃̇ ( (var zero ∈̇ var (suc zero))
               ∧̇ appC r zero (suc (suc zero)) )) ) )

The transversal

Inside the bounding stage, least-element search chooses one point per cell; separation collects those points, and disjointness proves uniqueness in every intersection.

The module fixes the ZF model supplying the intersection, the family, and the family's two hypotheses. The choice-stage construction supplies the bound and order at the family itself: β is an ordinal above the family's own stage, hence above its members and their members, and above ω where the names live; W is the well-order of the members of the tower at β; and rel is that same order as an element of the model, which is what lets it be named by a constant in the description at all.

Cell x is the predicate "is a member of x" on those members, and least applies the generic search from L.WellOrder.Base to it. The same search serves finite-stage orders and name selection, and will serve later GCH constructions; here its role is specific: it turns the stage order into one chosen representative for each cell. This is precisely the selection that excluded middle makes possible for the transversal.

pick-in and pick-out are the description's two readings, and neither is a corollary of the other: one builds a satisfaction out of a least element, the other extracts a least element from a satisfaction, and each has to move a set between the two ways it can be presented, as an element of L and as a member of the tower at β. Every truncation payload is named, Two and Predecessor, so that neither reading writes the nesting out; the negation is the one place a truncation is eliminated into the empty type, and it is eliminated in a named helper.

Then the separation and the counting. transversalSet is the model's own separation, at the tower at β, by the description. Cut fixes a member of the family: the centre of the intersection is the least element, which is in the transversal because pick-in says so and in the member because being least includes being there. Uniqueness is where pairwise disjointness is used. Another point of the intersection satisfies the description, so it is least in some member of the family; it also lies in this one; so the two members meet and are equal; so it is least in this member too, and least elements are unique by trichotomy alone. The generic uniqueness theorem isPropLeastOf closes precisely this last comparison.

module Trans (zf : isZFModel) (a : S)
             (inh : (x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
             (disj : (x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
                   → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
             where
  open ModelL.isZFModel zf using ( separate; separate-spec; _∩_; ∩-spec )
  private
    module B = Bound (fst a) (snd a)

  β : V ℓ
  β = B.boundOrd

  oβ : IsOrd β
  oβ = B.boundOrd-ord

  W : SWO (Mem (Lset β))
  W = B.boundOrder

  rel : S
  rel = B.orderL

  elt : Mem (Lset β) → S
  elt m = fst m , Lset→isL β oβ (fst m) (snd m)

  Cell : S → Mem (Lset β) → hProp (ℓ-suc ℓ)
  Cell x m = fst m ∈ fst x

  Least : S → S → Type (ℓ-suc ℓ)
  Least x z = Σ[ h ∈ ⟨ fst z ∈ Lset β ⟩ ] IsLeast W (Cell x) (fst z , h)

  private
    members : (x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ m ∈ Mem (Lset β) ] ⟨ Cell x m ⟩ ∥₁
    members x x∈a = PT.map atMember (inh x x∈a)
      where
      atMember : Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ → Σ[ m ∈ Mem (Lset β) ] ⟨ Cell x m ⟩
      atMember (y , y∈x) =
        (fst y , bound-below₂ (fst a) (snd a) (fst x) (fst y) y∈x x∈a) , y∈x

    least : (x : S) → ⟨ x ∈ˢ a ⟩ → Σ[ m ∈ Mem (Lset β) ] IsLeast W (Cell x) m
    least x x∈a = leastOf W lem (Cell x) (members x x∈a)

    Predecessor : S → S → S → Type (ℓ-suc ℓ)
    Predecessor x z w = ⟨ w ∈ˢ x ⟩
                      × ⟨ (w ∷ x ∷ z ∷ []) ⊨ appC rel zero (suc (suc zero)) ⟩

    Two : S → S → Type (ℓ-suc ℓ)
    Two x z = ⟨ x ∈ˢ a ⟩
            × (⟨ z ∈ˢ x ⟩
              × (∥ Σ[ w ∈ S ] Predecessor x z w ∥₁
                 → Lift {j = ℓ-suc ℓ} Empty.⊥))

    Out : S → Type (ℓ-suc ℓ)
    Out z = ∥ Σ[ x ∈ S ] (⟨ x ∈ˢ a ⟩ × Least x z) ∥₁

  opaque
    unfolding Pick

    pick-in : (x : S) → ⟨ x ∈ˢ a ⟩ → (z : S) → Least x z
            → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
    pick-in x x∈a z (hz , (z∈x , mini)) =
      ∣ x , (x∈a , (z∈x , neg)) ∣₁
      where
      noPredecessor : Σ[ w ∈ S ] Predecessor x z w → Empty.⊥
      noPredecessor (w , (w∈x , hap)) = mini (fst w , hw) w∈x lt
        where
        hw : ⟨ fst w ∈ Lset β ⟩
        hw = bound-below₂ (fst a) (snd a) (fst x) (fst w) w∈x x∈a
        hpr : ⟨ pr (fst w) (fst z) ∈ fst rel ⟩
        hpr = subst ⟨_⟩ (appC-adequate rel zero (suc (suc zero)) (w ∷ x ∷ z ∷ [])) hap
        lt : relOf W (fst w , hw) (fst z , hz)
        lt = B.orderL-rep (fst w , hw) (fst z , hz) hpr

      neg : ∥ Σ[ w ∈ S ] Predecessor x z w ∥₁
          → Lift {j = ℓ-suc ℓ} Empty.⊥
      neg q = lift (PT.rec Empty.isProp⊥ noPredecessor q)

    pick-out : (z : S) → ⟨ (z ∷ []) ⊨ Pick a rel ⟩ → Out z
    pick-out z = PT.rec PT.squash₁ atTwo
      where
      atTwo : Σ[ x ∈ S ] Two x z → Out z
      atTwo (x , (x∈a , (z∈x , neg))) = ∣ x , (x∈a , (hz , (z∈x , mini))) ∣₁
        where
        hz : ⟨ fst z ∈ Lset β ⟩
        hz = bound-below₂ (fst a) (snd a) (fst x) (fst z) z∈x x∈a

        mini : (b : Mem (Lset β)) → ⟨ Cell x b ⟩
             → relOf W b (fst z , hz) → Empty.⊥
        mini b b∈x lt = lower (neg ∣ elt b , (b∈x , hap) ∣₁)
          where
          hpr : ⟨ pr (fst b) (fst z) ∈ fst rel ⟩
          hpr = B.orderL-fill b (fst z , hz) lt
          hap : ⟨ (elt b ∷ x ∷ z ∷ []) ⊨ appC rel zero (suc (suc zero)) ⟩
          hap = subst ⟨_⟩
            (sym (appC-adequate rel zero (suc (suc zero)) (elt b ∷ x ∷ z ∷ []))) hpr

  transversalSet : S
  transversalSet = separate (LsetS β oβ) (Pick a rel)

  private
    csp : (z : S) → (z ∈ˢ transversalSet)
                  ≡ ((z ∈ˢ LsetS β oβ) ⊓ ((z ∷ []) ⊨ Pick a rel))
    csp = separate-spec (LsetS β oβ) (Pick a rel)

    inC : (z : S) → ⟨ fst z ∈ Lset β ⟩ → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
        → ⟨ z ∈ˢ transversalSet ⟩
    inC z hL hp = subst ⟨_⟩ (sym (csp z)) (hL , hp)

    outC : (z : S) → ⟨ z ∈ˢ transversalSet ⟩ → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
    outC z h = snd (subst ⟨_⟩ (csp z) h)

  module Cut (x : S) (x∈a : ⟨ x ∈ˢ a ⟩) where
    private
      m : Mem (Lset β)
      m = least x x∈a .fst

      lm : IsLeast W (Cell x) m
      lm = least x x∈a .snd

      z₀ : S
      z₀ = elt m

      inMeet : (z : S) → ⟨ z ∈ˢ transversalSet ⟩ → ⟨ z ∈ˢ x ⟩
             → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
      inMeet z hc hx = subst ⟨_⟩ (sym (∩-spec transversalSet x z)) (hc , hx)

      outMeet : (z : S) → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
              → ⟨ z ∈ˢ transversalSet ⟩ × ⟨ z ∈ˢ x ⟩
      outMeet z h = subst ⟨_⟩ (∩-spec transversalSet x z) h

      centre : Σ[ z ∈ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
      centre = z₀ , inMeet z₀
        (inC z₀ (snd m) (pick-in x x∈a z₀ (snd m , lm))) (fst lm)

      same : (z : S) → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩ → fst z ≡ fst m
      same z h = PT.rec (setIsSet (fst z) (fst m)) atOut
                   (pick-out z (outC z (fst (outMeet z h))))
        where
        z∈x : ⟨ z ∈ˢ x ⟩
        z∈x = snd (outMeet z h)

        atOut : Σ[ x' ∈ S ] (⟨ x' ∈ˢ a ⟩ × Least x' z) → fst z ≡ fst m
        atOut (x' , (x'∈a , (hz , lz))) =
          cong (λ p → fst (fst p))
            (isPropLeastOf W (Cell x) ((fst z , hz) , lz') (m , lm))
          where
          x≡x' : x ≡ x'
          x≡x' = disj x x' x∈a x'∈a ∣ z , (z∈x , fst lz) ∣₁

          lz' : IsLeast W (Cell x) (fst z , hz)
          lz' = subst (λ y → IsLeast W (Cell y) (fst z , hz)) (sym x≡x') lz

    meetsOnce : isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩)
    meetsOnce = centre , atPoint
      where
      atPoint : (p : Σ[ z ∈ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩) → centre ≡ p
      atPoint (z , h) = sym (Σ≡Prop
        (λ w → snd (w ∈ˢ (transversalSet ∩ x)))
        (Σ≡Prop (λ v → snd (isL v)) (same z h)))

  transversal : (x : S) → ⟨ x ∈ˢ a ⟩
              → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩)
  transversal = Cut.meetsOnce

The theorem

The final wrapper converts the transversal construction into the exact choice field required by the ZF model record on 𝒮ʟ.

ChoiceStatement is the statement the frontier used to hold, moved here verbatim and proved here: the model's choice field at 𝒮ʟ, relative to a ZF model on this carrier because the intersection is that model's derived operation. hasChoiceL gives the proof. The root chapter applies it to the very model it is assembling, which is why the statement quantifies over the model in the first place.

This line gives the Choice field used by the root theorem. Its statement remains relative to the ZF model being assembled because intersection is the derived operation of that model.

ChoiceStatement : isZFModel → Type (ℓ-suc ℓ)
ChoiceStatement zf =
  (a : S)
  → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
  → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
       → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
  → ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩
       → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁
  where open ModelL.isZFModel zf using ( _∩_ )

hasChoiceL : (zf : isZFModel) → ChoiceStatement zf
hasChoiceL zf a inh disj = ∣ T.transversalSet , T.transversal ∣₁
  where module T = Trans zf a inh disj

Recap

Pick, the bounded stage order, and separation together produce the transversal whose exact-one-point property supplies hasChoiceL.

Pick is the description: some member of the family contains this set, and nothing in that member precedes it. pick-in and pick-out are its two readings against being a least element of a member. transversalSet is what the model's separation cuts out with it, over the tower at the family's bounding ordinal, and transversal counts the intersection with each member: one point, existence from the least-element search and uniqueness from pairwise disjointness. hasChoiceL is the model's choice field, and with it the frontier is empty and gone.

One measurement, and it is a law declining to bite. A description read at constants is sealed where it is built, and that law was worth ninety-nine fold where it was found; here it is worth nothing, 2.3 s either way, because this description carries no coded syntax. The seal stays, and the number is recorded so that the law keeps its true shape: it is about what a description contains, not about where it is read.

What the book was for

The completed Choice chain supplies the missing model field, so under the single stated excluded-middle hypothesis the constructible universe satisfies ZFC.

This is the end of the chain, so it is worth stating plainly what has been established. In cubical Agda, granted one instance of the excluded middle at the model's own truth level, the constructible universe is a model of ZFC. Read with the ambient-hierarchy result that the hierarchy models ZF, that is Gödel's relative consistency of choice in semantic form: a universe satisfying ZF contains inside it a sub-universe satisfying ZFC, so an inconsistency of ZFC would already be an inconsistency of ZF.

The costs are stated explicitly. The host is cubical Agda with its universe tower, informally about as strong as ZFC plus an inaccessible; excluded middle is a module parameter rather than an axiom, and it is the only hypothesis the theorem carries; and the development has no postulates or holes. This chapter supplies the Choice field that L.Model combines with the earlier ZF structure.