Choice, and the frontier emptied

The last debt. What the registry still asks for is the axiom of choice at 𝒮ʟ, in the transversal form the model record states it: given a set whose members are inhabited and pairwise disjoint, merely a set meeting each member in exactly one point.

The shape of the argument is the classical one, with its expensive step already paid. 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.Truth
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.Stage {ℓ} lem using ( bound-below₂ )
open import L.Choice.Step {ℓ} lem using ( Mem; relOf )
open import L.Choice.Order {ℓ} lem using ( module Bound )
open import L.Coding.Model {ℓ} using ( appAt; appAt-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 TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ

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

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

The description

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 order enters as a constant and has to be bound to a variable first, because the atom saying that a pair belongs to a relation takes the relation from a slot; that costs one existential and one object equality, the device every description in this part has used to name a particular set. The family is 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 
  Pick c r =
    ∃̇ ( (var zero ∈̇ con c)
      ∧̇ ( (var (suc zero) ∈̇ var zero)
        ∧̇ ∃̇ ( (var zero ≐ con r)
             ∧̇ (¬̇ ∃̇ ( (var zero ∈̇ var (suc (suc zero)))
                    ∧̇ appAt (suc zero) zero (suc (suc (suc zero))) )) ) ) )

The transversal

The module fixes the ZF model supplying the intersection, the family, and the family's two hypotheses. The bound and the order come straight from the previous chapter 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 is the well-order chapter's search applied to it. That search has been waiting since it was written: L.WellOrder.Base was delivered with exactly one consumer named for it and none in hand, and this is the consumer. It is also where the excluded middle buys a genuine choice rather than a comparison, which is what that chapter said the cost was for.

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 through Four, 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 disjointness is spent. 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. Nothing here is a new argument: isPropLeastOf was proved in the well-order chapter and this is its first use.

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)

    Four : S → S → S → S → Type (ℓ-suc ℓ)
    Four x z r w = ⟨ w ∈ˢ x ⟩
                 × ⟨ (w ∷ r ∷ x ∷ z ∷ [])
                     ⊨ appAt (suc zero) zero (suc (suc (suc zero))) ⟩

    Three : S → S → S → Type (ℓ-suc ℓ)
    Three x z r = (fst r ≡ fst rel)
                × (∥ Σ[ w ∈ S ] Four x z r w ∥₁ → Empty.⊥)

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

    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 , ∣ rel , (refl , neg) ∣₁)) ∣₁
      where
      atFour : Σ[ w ∈ S ] Four x z rel w → Empty.⊥
      atFour (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 ⟨_⟩ (appAt-adequate (suc zero) zero (suc (suc (suc zero)))
                (w ∷ rel ∷ 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 ] Four x z rel w ∥₁ → Empty.⊥
      neg = PT.rec Empty.isProp⊥ atFour

    pick-out : (z : S) → ⟨ (z ∷ []) ⊨ Pick a rel ⟩ → Out z
    pick-out z = PT.rec PT.squash₁ atTwo
      where
      atThree : (x : S) → ⟨ x ∈ˢ a ⟩ → ⟨ z ∈ˢ x ⟩ → (r : S) → Three x z r
              → Out z
      atThree x x∈a z∈x r (qr , 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 = neg ∣ elt b , (b∈x , hap) ∣₁
          where
          hpr : ⟨ pr (fst b) (fst z) ∈ fst r ⟩
          hpr = subst (λ s → ⟨ pr (fst b) (fst z) ∈ s ⟩) (sym qr)
                  (B.orderL-fill b (fst z , hz) lt)
          hap : ⟨ (elt b ∷ r ∷ x ∷ z ∷ [])
                  ⊨ appAt (suc zero) zero (suc (suc (suc zero))) ⟩
          hap = subst ⟨_⟩ (sym (appAt-adequate (suc zero) zero
                  (suc (suc (suc zero))) (elt b ∷ r ∷ x ∷ z ∷ []))) hpr

      atTwo : Σ[ x ∈ S ] Two x z → Out z
      atTwo (x , (x∈a , (z∈x , h))) =
        PT.rec PT.squash₁ (λ { (r , h3) → atThree x x∈a z∈x r h3 }) h

  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

ChoiceStatement is the statement the frontier used to hold, moved here verbatim and no longer a debt: the model's choice field at 𝒮ʟ, relative to a ZF model on this carrier because the intersection is that model's derived operation. hasChoiceL proves it. 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.

With this line the registry is empty, so L.Frontier is deleted, and the root chapter's second parameter with it. That was the promise the device was built on: a field, once proven, is deleted, and the record disappears when it empties.

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 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

This is the end of the chain, so it is worth saying plainly what stands. 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 Part 3, where the ambient 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.

Every price is printed on the label. The host is cubical Agda with its universe tower, informally about as strong as ZFC plus an inaccessible; the excluded middle is a module parameter and not an axiom, and it is the only hypothesis the theorem carries; and there are no postulates anywhere in this development, no holes, and, as of this chapter, no registry of statements not yet proven. The book opened by stating its main theorem before it could prove it, and paid for that honesty with a record whose fields were the outstanding claims. The record is empty. What is left is a theorem.