The least-witness map inside a constructible stage

Suppose that, for each input x ∈ X, we know only under propositional truncation that some w ∈ Lset γ satisfies P(w,x). Such pointwise existence does not yet give a graph inside L, because one formula must determine a unique value. This chapter uses the canonical strict well order of the fixed stage to choose its least satisfying candidate, expresses that choice by a formula, and collects the graph as a set of L. The minimum is relative to this stage and this order, and P itself may have many witnesses.

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

Classical logic enters through the fixed excluded-middle hypothesis, which already underlies the canonical stage order. At the actual least-element search, it has a precise role: during well-founded descent it decides whether a smaller satisfying stage member merely exists. Propositional truncation is eliminated only into the total type of least witnesses, after that type has been proved to be a proposition; this gives no general way to extract arbitrary witnesses.

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

Fix a universe level ℓ and excluded middle for propositions at level ℓ-suc ℓ. Every selected witness and every graph constructed below is relative to this single hypothesis and to the fixed stage order introduced later.

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

The desired graph must be expressed in the first-order language of sets. Besides saying that P(w,x) holds, its formula must say that w lies in the chosen stage and that no smaller member of that stage also satisfies P. A bounded universal quantifier expresses the latter condition, while renaming lets the original two-variable formula keep its meaning after the smaller candidate is inserted into the environment.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∀̇∈ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

Two views of the stage order are needed. The host-level strict well order supports least-element search, while a constructible set Rγ of coded ordered pairs lets the same comparison appear inside the object-language graph formula. The representation lemmas pass between these views; they do not identify them by definition.

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.StageOrders {ℓ} lem using ( orderAt; relOf ) renaming ( Mem to MemOf )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-fill; relL-rep )

The strict well order supplies both a least-element operation and trichotomy. The former selects a value from a merely inhabited family of candidates; the latter proves that any two candidates satisfying the complete leastness specification coincide. Once that specification is expressed by a formula, replacement collects the resulting input-value pairs into a set of L.

open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( SWO; leastOf; lt; eq; gt ) renaming ( Tri to Tri∙ )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Graph )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( isL-ord )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )

Propositional truncation deliberately hides which initial candidate exists. The proof may eliminate that truncation only after changing the target to the total type of least elements and proving that this target is itself a proposition. Equality of constructible sets likewise ignores their proof components, so equality of the underlying sets is enough throughout the argument.

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

The carrier S packages an ambient set together with a proof that it is constructible. Inputs and candidates can therefore occupy entries of a satisfaction environment, while the packaged stage Lγ and order relation Rγ can occur as constants in formulas. First projection returns the underlying sets needed for membership and ordered-pair coding.

open hPropStructure 𝒮ʟ using ( S )

Satisfaction is read in the constructible structure 𝒮ʟ. In particular, P is already an object-language formula; the chapter selects witnesses for this definable relation and does not claim to turn an arbitrary host-level predicate into a definable one.

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

The original formula is evaluated in the two-entry environment (w,x). When leastness introduces a bounded competitor, the environment becomes (w',w,x), so the occurrence of the input must move while the new candidate w' occupies the first slot. Compatibility of satisfaction with renaming will justify that shift.

module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )

The indices i0 and i1 name the first two available de Bruijn slots. Their mathematical roles depend on the environment: in (w,x) they refer to the proposed value and the input, while inside the bounded environment (w',w,x) they refer to the competitor and the proposed value.

private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0

Two constructible sets with equal underlying sets are equal, by the propositionhood of constructibility; every later identification of constructible sets goes through this lift.

  S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
  S≡ = Σ≡Prop (λ v → snd (isL v))

Selecting the least satisfying member

The least-witness module receives four pieces of data. The ordinal index γ with its ordinalness determines the stage; the set X constrains the inputs; the binary formula P is the predicate; and for every input in X the hypothesis asserts, merely, that some candidate from the stage satisfies the predicate there. The candidates are drawn from the whole stage Lset γ, while the inputs are constrained to X.

module Least (γ : V ℓ) (oγ : IsOrd γ) (X : S) (P : Formula S )
  (have : (x : S) → ⟨ fst x ∈ fst X ⟩
        → ∥ Σ[ w ∈ S ] (⟨ fst w ∈ Lset γ ⟩ × ⟨ (w ∷ x ∷ []) ⊨ P ⟩) ∥₁) where

The ambient stage Lset γ is packaged as an element Lγ of the constructible carrier. This package can occur as a constant in the graph formula, so the formula can bound its search to exactly the fixed candidate stage.

  opaque
    Lγ : S
    Lγ = LsetS γ oγ

The equation Lγ-fst exposes the underlying set of this opaque package as Lset γ. Later membership proofs cross this equation when moving between the host-level stage and the constant used by the formula.

    Lγ-fst : fst Lγ ≡ Lset γ
    Lγ-fst = refl

The internal relation encoder also needs the ordinal index itself as an element of the constructible universe. Every ordinal is constructible, and oγ supplies the ordinalness needed to obtain that fact for γ.

    hγ : ⟨ isL γ ⟩
    hγ = isL-ord γ oγ

The internal implementation of the stage order is a constructible set of coded pairs, the relation in which leastness will be expressed.

  Rγ : S
  Rγ = relL γ hγ oγ

The predicate Mem x records the restriction on inputs: it is evidence that x ∈ X. It imposes no condition on witness candidates, whose separate carrier is the set of members of Lset γ introduced next.

  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst X ⟩

The order orderAt γ oγ acts on stage members rather than on arbitrary elements of S. The subtype Mγ builds the bound c ∈ Lset γ into every object being compared, so least-element search cannot range outside the fixed candidate stage.

  private
    Mγ : Type (ℓ-suc ℓ)
    Mγ = MemOf (Lset γ)

An element of Mγ contains an underlying set together with its membership in Lset γ. Every member of a constructible stage is constructible, so memS can promote that underlying set to the carrier S; the original membership proof remains available as the stage bound on the candidate.

    memS : Mγ → S
    memS c = fst c , Lset→isL γ oγ (fst c) (snd c)

The predicate at a candidate and an input is the object-language satisfaction of P in the environment placing the candidate first and the input second.

    At : S → S → hProp (ℓ-suc ℓ)
    At w x = (w ∷ x ∷ []) ⊨ P

The predicate Good x transfers the original relation to the carrier ordered by orderAt γ oγ: a stage member is good exactly when its associated element of S satisfies P with input x. Consequently the forthcoming search orders candidates from Lset γ; it does not order the inputs in X or restrict candidates to X.

    Good : S → Mγ → hProp (ℓ-suc ℓ)
    Good x c = At (memS c) x

The same underlying set may arrive with two proofs that it is constructible. Since constructibility is a proposition, S≡ identifies the two packaged elements of S; transporting satisfaction along that path shows that the repackaged stage member satisfies the same instance of P as the original witness.

    toMem : (x w : S) (hw : ⟨ fst w ∈ Lset γ ⟩) → ⟨ At w x ⟩ → ⟨ Good x (fst w , hw) ⟩
    toMem x w hw = subst (λ v → ⟨ At v x ⟩) (S≡ refl)

Selection is performed after fixing an input x and evidence m : x ∈ X. The evidence authorizes the use of the pointwise existence hypothesis have; it neither puts the candidate in X nor equips X with an order.

  module Sel (x : S) (m : Mem x) where

For the fixed input, the hypothesis is mapped into the type of good stage members. This changes only the representation of each possible witness: the resulting nonemptiness remains propositionally truncated, so no particular starting member has yet been chosen.

    private
      nonempty : ∥ Σ[ c ∈ Mγ ] ⟨ Good x c ⟩ ∥₁
      nonempty = PT.map (λ { (w , hw , hp) → (fst w , hw) , toMem x w hw hp }) (have x m)

Now leastOf descends through orderAt γ oγ and returns an actual least good member. This is the exceptional elimination step: excluded middle decides whether descent can continue, and propositional truncation may be eliminated because the total type of a least element together with its leastness proof has already been shown to be a proposition. Neither fact alone would justify extracting an arbitrary witness from nonempty.

    opaque
      c : Mγ
      c = fst (leastOf (orderAt γ oγ) lem (Good x) nonempty)

The result of the search retains the proof that the selected member is good. Thus the passage from mere existence to an actual least element does not lose the original predicate.

      c-good : ⟨ Good x c ⟩
      c-good = fst (snd (leastOf (orderAt γ oγ) lem (Good x) nonempty))

Its companion clause gives the exact relative leastness needed later: any other good member of this same stage is forbidden from lying strictly below the selected one in orderAt γ oγ.

      minimal : (c' : Mγ) → ⟨ Good x c' ⟩ → relOf (orderAt γ oγ) c' c → Empty.⊥
      minimal = snd (snd (leastOf (orderAt γ oγ) lem (Good x) nonempty))

The order compares objects in Mγ, whereas satisfaction environments contain objects of S. Repackaging the chosen member as e crosses this interface without changing its underlying set.

    e : S
    e = memS c

Because goodness was defined through this same repackaging, the selected element of S immediately satisfies P(e,x); no second choice or new search is involved.

    e-holds : ⟨ (e ∷ x ∷ []) ⊨ P ⟩
    e-holds = c-good

The membership component carried by the selected stage member also proves e ∈ Lset γ. Predicate satisfaction and the stage bound are therefore obtained from the same least candidate.

    e∈Lγ : ⟨ fst e ∈ Lset γ ⟩
    e∈Lγ = snd c

For an input x equipped with m : x ∈ X, the function fn returns this selected candidate. Its domain evidence is explicit because the existence hypothesis is available only on X.

  fn : (x : S) → Mem x → S
  fn x m = Sel.e x m

At every such domain input, the chosen value satisfies the original formula in the environment (fn(x),x).

  fn-holds : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ P ⟩
  fn-holds x m = Sel.e-holds x m

The same value lies in Lset γ. This separate range statement will later place the definable map in codomain Lγ; it does not say that the value lies in the input set X.

  fn-in : (x : S) (m : Mem x) → ⟨ fst (fn x m) ∈ Lset γ ⟩
  fn-in x m = Sel.e∈Lγ x m

To state leastness in terms that can also be expressed inside L, assume that a competitor w' is recorded below fn(x) by the internal relation Rγ. The reading lemma relL-rep converts this coded entry into the host-level comparison used by orderAt γ oγ, where the minimality of the selected member refutes it. The conclusion excludes only satisfying competitors in Lset γ and only with respect to this fixed order.

  fn-least : (x : S) (m : Mem x) (w' : S) → ⟨ fst w' ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
           → ⟨ pr (fst w') (fst (fn x m)) ∈ fst Rγ ⟩ → Empty.⊥
  fn-least x m w' hw' hp hr = Sel.minimal x m (fst w' , hw') (toMem x w' hw' hp)
    (relL-rep γ hγ oγ (fst w' , hw') (Sel.c x m) hr)

The host-level specification TWit w x combines the three facts that the graph formula must express: P(w,x), membership of w in the fixed stage, and the absence of a stage member satisfying P strictly below w in orderAt γ oγ. This is a specification of a graph value, before the graph is collected as an internal table.

  TWit : (w x : S) → Type (ℓ-suc ℓ)
  TWit w x =
      ⟨ (w ∷ x ∷ []) ⊨ P ⟩
    × ⟨ fst w ∈ Lset γ ⟩
    × ((w' : S) → ⟨ fst w' ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩

The last component tests any w' that lies in Lset γ and satisfies P(w',x). If the coded pair (w',w) belonged to Rγ, it would say that w' is strictly smaller in the fixed stage order, and the specification refutes precisely that possibility.

        → ⟨ pr (fst w') (fst w) ∈ fst Rγ ⟩ → Empty.⊥)

Uniqueness is proved only among candidates satisfying the complete TWit specification. The original predicate P may have many witnesses in the stage; what cannot happen in a strict total order is that two distinct candidates both satisfy P and both have no smaller satisfying candidate. Trichotomy reduces the comparison with the selected value to the three cases handled next.

  fn-unique : (x : S) (m : Mem x) (w : S) → TWit w x → fst w ≡ fst (fn x m)
  fn-unique x m w (hp , hw , mn) = go (SWO.tri∙ (orderAt γ oγ) c' (Sel.c x m))
    where
    c' : Mγ
    c' = fst w , hw

If the alternative candidate were strictly below the selected one, leastness would be contradicted; if the two stage members coincided, their underlying sets would be equal.

    go : Tri∙ (relOf (orderAt γ oγ) c' (Sel.c x m)) (c' ≡ Sel.c x m)
              (relOf (orderAt γ oγ) (Sel.c x m) c')
       → fst w ≡ fst (fn x m)
    go (lt k) = Empty.rec (Sel.minimal x m c' (toMem x w hw hp) k)
    go (eq q) = cong fst q

If the selected candidate were strictly below the alternative, the alternative's own leastness would be contradicted, with the missing comparison supplied by the filling direction of the internal relation.

    go (gt k) = Empty.rec (mn (fn x m) (fn-in x m) (fn-holds x m)
      (relL-fill γ hγ oγ (Sel.c x m) c' k))

Under the bounded quantifier the environment is (w',w,x), whereas P expects (candidate,input). The renaming therefore sends its variable 0 to slot 0, still w', and its variable 1 to slot 2, now x; slot 1 is reserved for the proposed value w against which w' is compared.

  private
    ρ : Fin  → Fin 
    ρ zero       = zero
    ρ (suc zero) = suc (suc zero)

Agreement records exactly those two identifications: reading variable 0 from (w',w,x) gives the first entry of (w',x), and reading variable 1 after renaming gives the second. This pointwise agreement is the premise needed to transport satisfaction of the whole formula P.

    ag : (w' w x : S) → Ren.Agrees ρ (w' ∷ w ∷ x ∷ []) (w' ∷ x ∷ [])
    ag w' w x zero       = refl
    ag w' w x (suc zero) = refl

The leastness formula ranges over w' ∈ Lγ and denies the conjunction of two claims: the coded pair (w',w) belongs to Rγ, and P(w',x) holds. Semantically it says that no candidate in the fixed stage lies below w in orderAt γ oγ while also witnessing the original predicate for the same input.

  opaque
    private
      leastFo : Formula S 
      leastFo = ∀̇∈ (con Lγ) (¬̇ (appC Rγ i0 i1 ∧̇ renameFo ρ P))

Compatibility with renaming now identifies the two readings of P: evaluating renameFo ρ P in (w',w,x) is the same as evaluating P directly in (w',x). The current proposed value w is deliberately absent from the predicate test on the competitor; it occurs only in the order comparison (w',w).

      ren : (w' w x : S)
          → ⟨ (w' ∷ w ∷ x ∷ []) ⊨ renameFo ρ P ⟩ ≡ ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
      ren w' w x = cong ⟨_⟩ (Ren.⊨-rename ρ P (w' ∷ w ∷ x ∷ []) (w' ∷ x ∷ []) (ag w' w x))

The full graph formula conjoins the original predicate with stage membership and the leastness clause: a value is recorded exactly when it satisfies the predicate, lies in the fixed stage, and is least among stage members that do.

    fo : Formula S 
    fo = P ∧̇ ((var i0 ∈̇ con Lγ) ∧̇ leastFo)

Reading fo outward recovers the three parts of the semantic specification: P(w,x), membership w ∈ Lset γ, and the absence of a satisfying member of that stage recorded below w by the internal order. The formula fo itself does not contain the condition x ∈ X; that restriction is imposed when fo is used as the graph formula of Dmap. Thus X controls the inputs on which a value must be defined, while Lset γ controls the candidates compared for that input.

    fo-out : (w x : S) → ⟨ (w ∷ x ∷ []) ⊨ fo ⟩ → TWit w x
    fo-out w x (hp , (hl , hm)) =
        hp
      , subst (λ v → ⟨ fst w ∈ v ⟩) Lγ-fst hl
      , λ w' hw' hp' hr → lower (hm w' (subst (λ v → ⟨ fst w' ∈ v ⟩) (sym Lγ-fst) hw')

To obtain the minimality component of TWit, fix a competitor w' and assume the semantic facts that pr(w',w) ∈ Rγ and P(w',x). The proof uses appC-adequate and renaming in the inward direction to turn these facts into satisfaction of the two conjuncts negated by fo; the bounded clause then yields the contradiction. The relation entry is an object-language encoding of the stage-order comparison, not a definitional equality with relOf (orderAt γ oγ).

          ( subst ⟨_⟩ (sym (appC-adequate Rγ i0 i1 (w' ∷ w ∷ x ∷ []))) hr
          , transport (sym (ren w' w x)) hp' ))

Conversely, a witness satisfying TWit determines a proof of the graph formula. Its first two components establish P(w,x) and w ∈ Lset γ. For the bounded minimality clause, take any w' in that same level and suppose that the encoded order places w' before w and that P(w',x) holds; the last component of TWit rules out exactly this conjunction.

    fo-in : (w x : S) → TWit w x → ⟨ (w ∷ x ∷ []) ⊨ fo ⟩
    fo-in w x (hp , hl , mn) =
        hp
      , subst (λ v → ⟨ fst w ∈ v ⟩) (sym Lγ-fst) hl
      , λ w' hw' hc → lift (mn w' (subst (λ v → ⟨ fst w' ∈ v ⟩) Lγ-fst hw')

Renaming and application adequacy put those two assumptions into the forms expected by semantic minimality. Together, fo-out and fo-in show that fo expresses exactly the fixed-level least-witness specification. They add neither uniqueness of witnesses for the original predicate nor any comparison with candidates outside Lset γ.

          (transport (ren w' w x) (snd hc))
          (subst ⟨_⟩ (appC-adequate Rγ i0 i1 (w' ∷ w ∷ x ∷ [])) (fst hc)))

This exact correspondence makes the selection definable. The map has input set X and codomain Lγ: for each proof that x ∈ X, its value is fn x m, and the earlier level-membership theorem places that value in Lγ. The graph formula is read in the environment (value,input), so its first variable denotes the selected witness and its second variable denotes the input.

  Dmap : DefinableMap
  Dmap = record
    { dom = X ; cod = Lγ ; fn = fn
    ; into = λ x m → subst (λ v → ⟨ fst (fn x m) ∈ v ⟩) (sym Lγ-fst) (fn-in x m)
    ; graph = fo

At the selected value, the three facts already proved supply a proof of fo: the value satisfies P, lies in the candidate level, and has no smaller satisfying competitor there. Conversely, any value satisfying fo carries this full least-witness specification and is therefore equal to the selected value. This uniqueness comes from the two candidates' leastness and trichotomy of orderAt γ oγ, not from uniqueness of P-witnesses; equality of their underlying sets lifts to equality in S because constructibility evidence is propositional.

    ; defines = λ x m → fo-in (fn x m) x (fn-holds x m , fn-in x m , fn-least x m)
    ; only = λ x m w h → S≡ (fn-unique x m w (fo-out w x h)) }

Once a formula defines one value for every input in X, replacement can collect those values inside L. Applied to Dmap, the graph construction provides a constructible set of ordered pairs together with the two directions needed to use its membership relation.

  private
    module Gr = Graph Dmap using ( F; F-in; pair-out )

Call this collected set T. Its entries are ordered pairs (x,fn(x)), with the input first and the selected value second. This reverses the order used by formula satisfaction, whose environment was (value,input); keeping the two conventions distinct prevents the graph formula from being mistaken for the internal table itself.

  T : S
  T = Gr.F

For every x ∈ X, the table contains the pair (x,fn(x)). Hence later arguments may refer to the choices through membership in one constructible set, rather than making a separate choice from the merely inhabited family for each input.

  T-in : (x : S) (m : Mem x) → ⟨ pr (fst x) (fst (fn x m)) ∈ fst T ⟩
  T-in = Gr.F-in

Conversely, an entry (x,w) ∈ T yields evidence x ∈ X and equality of the underlying set of w with that of the selected value fn(x). Table membership does not return the leastness proof itself. In HullCounting, this table is used to synchronize choices that were previously available only under propositional truncation. When an injection is needed, a separate reverse-functionality hypothesis for the underlying relation proves that a fixed related candidate cannot correspond to two different inputs; injectivity is not a consequence of least selection alone.

  T-out : (x w : S) → ⟨ pr (fst x) (fst w) ∈ fst T ⟩
        → Σ[ m ∈ Mem x ] (fst w ≡ fst (fn x m))
  T-out = Gr.pair-out