BedrockPinning recursion on a subcode-closed domain
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapFix an index set of hierarchy codes that is closed under the immediate formula subcodes demanded by each recognized constructor shape. Assume also that the carrier slot, tag slots, and environment tower have their canonical meanings and that the table satisfies the complete table specification. The first half of this chapter then proves a local uniqueness statement: whenever a known formula key belongs to the index set and a table entry is supplied at that key, the entry's underlying set is the recursively defined satisfaction set. Independently of closure, the second half builds the table clauses from explicit carrier, tag, tower, value-agreement, decoding, totality, and domain hypotheses. Neither direction produces a globally chosen satisfaction function.
{-# OPTIONS --cubical --safe --guardedness #-}
The argument is carried out relative to an explicit instance of excluded middle. Classical logic supports the imported constructions of satisfaction sets, environment sets, and tables, but it does not remove propositional truncation: a decoded formula or a child table value may still be known only to exist.
open import Base.Prelude open import Base.Classical using ( LEM )
The module fixes the universe level and names the classical hypothesis: every theorem below records exactly which level instance of excluded middle it consumes.
module L.Coding.PinnedRecursion {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
Structural recursion follows the ten constructors of the formula grammar: membership and equality atoms, conjunction, disjunction, implication, falsity, the two unbounded quantifiers, ∀[]-syntax, and ∃[]-syntax. Constant relabelling lets the same syntactic tree be read first over the member alphabet of a carrier and then over the constructible carrier, without changing its constructor structure.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; Term; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇∈; ∀̇∈; ∃̇_; ∀̇_ ) import FOL.Absoluteness open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )
A formula key combines its arity with its syntax code by set-theoretic pairing. There are two versions of this construction: one directly in the cumulative hierarchy and one internally in L, carrying constructibility proofs. Pair projection, numeral projection, and code projection will show that their underlying hierarchy sets agree.
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; module VCode ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Coding.Model {ℓ} using ( module LCode; prʟ-fst; codeBridge )
The closure condition follows exactly the recursive dependencies of formula satisfaction. A binary connective requires both same-arity formula children, an unbounded quantifier requires its successor-arity body, and ∀[]-syntax or ∃[]-syntax requires only its successor-arity formula body. The term code carried by either of the last two constructors is evaluated inside the clause and is not required to belong to the closed domain.
open import L.Coding.Expressions {ℓ} using ( consAtL ) open import L.Coding.Closure {ℓ} using ( closedAt; binShapeAt; unShapeAt; bothSameAt; oneSuccAt; succSndAt; binSameClosed-out; unSuccClosed-out; binSuccClosed-out ) open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet ) open import L.Coding.CodeConstructibility {ℓ} using ( sglʟ; cupʟ; tree; tree-inv ) open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; AllCodes-out; keyS; codeS )
For a formula ψ, Sat gives the canonical recursively defined set of satisfying environments. A satisfaction table instead stores coded key-value pairs. The theorem will compare a supplied value in such a pair with Sat ψ; table totality supplies child values only under propositional truncation, so the proof may use them to establish an equality but never turns them into a reusable choice function.
open import L.Coding.Satisfaction {ℓ} lem using ( Sat ) open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst ) open import L.Coding.SatisfactionTable {ℓ} lem using ( keyʟ; slot; satTable; entry-out; inSlot; ent-slot ) renaming ( total to slotTotal )
Tags zero through nine select the ten constructor clauses. The environment tower records, for each natural arity n, the pair consisting of the numeral # n and the encoded set of length-n environments. These two coordinate systems let a clause recognize both the syntactic constructor and the arity at which its satisfaction set is being characterized.
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9; sh; i0; i1; i2; i3; i4; i7; i8 ; fstS; sndS; bigAnd-in; bigAnd-out ) open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; towerAt; module TowerRead ) open import L.Coding.CodeDomain {ℓ} using ( Tags )
The table specification has three mathematical parts: every domain key has some value, every table entry is a key-value pair whose key lies in the domain, and each of the ten constructors satisfies its semantic clause. The clause semantics turns the last part into extension facts. When a candidate value and the canonical recursive value have the same extension over the environment set, extensionality identifies their underlying hierarchy sets.
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet ) open import L.Coding.SatisfactionClauses {ℓ} using ( tmIs; tableAt; module Clause; module Rel ) open import L.Coding.SatisfactionClauseSemantics {ℓ} lem using ( extB-out; extB-in; ExtFact; ext-unique; module Frame; module RelRead; module Bridge ) open import Cubical.Data.Nat using ( _+_ )
Clause environments are finite vectors, and extending a frame shifts every older coordinate. Lookup and transport keep those coordinates aligned. Witnesses hidden by propositional truncation are eliminated only into proposition-valued targets: equality of underlying hierarchy sets in the pinning proof, and satisfaction of a fixed object-language clause in the filling proof. These eliminations do not expose reusable values, decodings, or frame data.
open import Cubical.Data.Vec using ( _∷_; lookup ) open import Cubical.Data.Sigma using ( _×_ ) open import Cubical.Foundations.Prelude using ( subst2 ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT
Propositional truncation preserves that a witness exists while forgetting which witness it was. Its eliminator therefore requires a proposition-valued target. Membership in the hierarchy is proposition-valued, and the hierarchy V is an h-set, so an equality between two of its sets is also a proposition and is a legitimate target for the eliminations used below.
open PT using ( ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet {ℓ} using ( #_; sucV )
A constructor tag is stored as an element of Fin 10, while syntax codes use an ordinary natural numeral. The map toℕ forgets the bound proof and exposes the natural number whose numeral appears in the coded pair; the bound still guarantees that only tags zero through nine arise.
open import Cubical.Data.FinData using ( toℕ )
Write S for the carrier of the first-order structure on L. An element of S consists of an underlying hierarchy set together with proof that it is constructible. Most conclusions in this chapter compare only the first projections, because equality of the represented sets is the mathematical content needed by satisfaction.
open hPropStructure 𝒮ʟ using ( S )
Object-language clauses are interpreted in the first-order structure carried by L. The notation γ ⊨ φ therefore means that the formula φ is satisfied by the finite environment γ in that structure. The bridge lemmas will compare such internal satisfaction statements with membership in the externally defined set SatW ψ.
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
Matching keys, tags, and decoded formulas
The two routes to a formula key are compared first. The external route embeds the alphabet symbols into the hierarchy and pairs the ambient numeral; the internal route relabels the constants as constructible sets, codes the formula inside L, and pairs the internal numeral.
module _ (A : S) where keyBridge : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) → fst (keyS A ψ) ≡ fst (keyʟ (mapFo (asConst A) ψ)) keyBridge {n} ψ = cong (pr (# n))
The proof aligns the syntax-code component first: relabelling the constants and then taking the ambient code agrees with projecting the internal code of the relabelled formula. It then aligns the arity numerals and finally projects the internal ordered pair. The resulting path relates the first projections of the two keys; it makes no claim that their accompanying constructibility proofs are definitionally the same.
( cong (λ χ → VCode.⌜ χ ⌝) (sym (mapFo-comp (asConst A) fst ψ)) ∙ sym (codeBridge (mapFo (asConst A) ψ)) ) ∙ cong (λ w → pr w (fst LCode.⌜ mapFo (asConst A) ψ ⌝)) (sym (numeralL-fst n)) ∙ sym (prʟ-fst (numeralL n) LCode.⌜ mapFo (asConst A) ψ ⌝)
The matching module is stated for one carrier W: its alphabet supplies the term and formula syntax whose shapes are matched.
module Match (W : S) where open Alphabet W
MatchN is a family of shape records indexed by a tag: for tags zero and one it names the two terms of an atom and their coded pair; for tags two through four it names the two immediate subformulas of a binary connective and their coded pair. The family is indexed by an already known formula, so it is not a parser of arbitrary sets.
MatchN : ∀ {n} → ℕ → Formula Ab n → V ℓ → Type (ℓ-suc ℓ) MatchN {n} 0 ψ r = Σ[ t ∈ Term Ab n ] Σ[ u ∈ Term Ab n ] ((ψ ≡ t ∈̇ u) × (r ≡ pr (ct t) (ct u))) MatchN {n} 1 ψ r = Σ[ t ∈ Term Ab n ] Σ[ u ∈ Term Ab n ] ((ψ ≡ t ≐ u) × (r ≡ pr (ct t) (ct u))) MatchN {n} 2 ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ∧̇ b) × (r ≡ pr (cd a) (cd b))) MatchN {n} 3 ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ∨̇ b) × (r ≡ pr (cd a) (cd b)))
Tags four through eight continue the same shape table. Tag four records implication and its two formula codes; tag five records falsity with numeral zero as payload; tags six and seven record the successor-arity bodies of the two unbounded quantifiers; tag eight records the current-arity term code and successor-arity body of ∀[]-syntax.
MatchN {n} 4 ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ⇒̇ b) × (r ≡ pr (cd a) (cd b))) MatchN 5 ψ r = (ψ ≡ ⊥̇) × (r ≡ # 0) MatchN {n} 6 ψ r = Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∃̇ a) × (r ≡ cd a)) MatchN {n} 7 ψ r = Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∀̇ a) × (r ≡ cd a)) MatchN {n} 8 ψ r = Σ[ t ∈ Term Ab n ] Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∀̇∈ t a) × (r ≡ pr (ct t) (cd a)))
Tag nine has the analogous payload for ∃[]-syntax: a term code at the current arity paired with a formula code at successor arity. The auxiliary family is empty at every natural tag at least ten. Thus MatchN describes exactly the ten constructor shapes, although it is defined on all natural numbers to support transport along tag equalities.
MatchN {n} 9 ψ r = Σ[ t ∈ Term Ab n ] Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∃̇∈ t a) × (r ≡ pr (ct t) (cd a))) MatchN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) ψ r = Empty.⊥*
The transport helper converts a matching record between tags and payloads. Pair injectivity splits an equality of coded pairs into the tag and payload components, and numeral injectivity transports the tag index; the matching record is then substituted along both.
private at : ∀ {n} (ψ : Formula Ab n) (j k : ℕ) (r : V ℓ) → pr (# j) (cd ψ) ≡ pr (# j) (cd ψ) → MatchN j ψ r → (r' : V ℓ) → pr (# j) r ≡ pr (# k) r' → MatchN k ψ r' at ψ j k r _ mj r' e = subst2 (λ i x → MatchN i ψ x) (#-inj′ (pr-inj e .fst)) (pr-inj e .snd) mj
The tag reader matchAt does not decode an arbitrary set. It starts from an already given formula, states the equality of that formula's code with a tagged pair, and returns the matching record: the case analysis on the formula exposes its own tag, and the transport helper relabels it to the given tag.
matchAt : ∀ {n} (ψ : Formula Ab n) (k : ℕ) (r : V ℓ) → cd ψ ≡ pr (# k) r → MatchN k ψ r matchAt (t ∈̇ u) k r e = at (t ∈̇ u) 0 k _ refl (t , u , (refl , refl)) r e matchAt (t ≐ u) k r e = at (t ≐ u) 1 k _ refl (t , u , (refl , refl)) r e matchAt (a ∧̇ b) k r e = at (a ∧̇ b) 2 k _ refl (a , b , (refl , refl)) r e matchAt (a ∨̇ b) k r e = at (a ∨̇ b) 3 k _ refl (a , b , (refl , refl)) r e
The remaining clauses perform no search. In each structural case, the known constructor supplies its canonical tag and payload: implication supplies two child codes, falsity supplies zero, each unbounded quantifier supplies its body code, and ∀[]-syntax supplies its term and body codes. The same transport helper then reconciles these canonical data with the tag and payload named by the input equality.
matchAt (a ⇒̇ b) k r e = at (a ⇒̇ b) 4 k _ refl (a , b , (refl , refl)) r e matchAt ⊥̇ k r e = at ⊥̇ 5 k _ refl (refl , refl) r e matchAt (∃̇ a) k r e = at (∃̇ a) 6 k _ refl (a , (refl , refl)) r e matchAt (∀̇ a) k r e = at (∀̇ a) 7 k _ refl (a , (refl , refl)) r e matchAt (∀̇∈ t a) k r e = at (∀̇∈ t a) 8 k _ refl (t , a , (refl , refl)) r e
For ∃[]-syntax, the canonical tag is nine and the payload is the pair of the bound term code and the successor-arity body code. This final structural branch completes matchAt for every formula constructor; its conclusion still describes the shape of the formula already supplied as input.
matchAt (∃̇∈ t a) k r e = at (∃̇∈ t a) 9 k _ refl (t , a , (refl , refl)) r e
Now suppose c belongs to the canonical code set and is presented as the pair of the arity numeral # n with a payload z. Membership in AllCodes W yields, under propositional truncation, some arity n₁, some formula ψ₁ of that arity, and an equality between c and its key. The remaining work is to reconcile n₁ with the stated n.
decodeAll : (c : S) → ⟨ fst c ∈ fst (AllCodes W) ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁ decodeAll c c∈ n z e = PT.map (λ { (n₁ , ψ₁ , e₁) → let q = pr-inj (sym e₁ ∙ e)
Injectivity of pairing equates the two arity numerals and the two payloads; numeral injectivity then gives a path n₁ ≡ n. Transporting ψ₁ along this dependent path changes its code by cd-subst, yielding a formula of exactly arity n whose code is z. The result remains propositionally truncated, so it provides neither a chosen decoder nor uniqueness of the decoded formula.
nq = #-inj′ (q .fst) in subst (Formula Ab) nq ψ₁ , (sym (q .snd) ∙ sym (cd-subst nq ψ₁)) }) (AllCodes-out W c c∈)
Uniqueness on a subcode-closed domain
The soundness argument is local to an arbitrary code domain C. Besides a proposed table T, it assumes that the stored carrier is W, the ten tag slots contain the correct numerals, the environment slot is the correct tower, C is closed under the required immediate formula subcodes, and T satisfies the packaged table specification. These hypotheses do not assert that every formula key lies in C.
module SatSoundC {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S) (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N) (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) (hcl : ⟨ γ ⊨ closedAt C ⟩) (hT : ⟨ γ ⊨ tableAt T w C E N ⟩) where open Alphabet W
Write Tv, Cv, and Ev for the underlying hierarchy sets stored in the table, code-domain, and environment-tower slots. Atomic formulas require no recursive lookup in Cv: their term codes are interpreted directly by the atomic bridge. Recursive calls enter only when a constructor has immediate formula children.
open Bridge W private Tv = fst (lookup T γ) Cv = fst (lookup C γ) Ev = fst (lookup E γ)
Let Wv denote the underlying hierarchy set of the carrier W. Quantifier bridges use this set as their range of quantification, while the atomic bridges interpret term codes over the alphabet determined by the same carrier. The proofs compare values as hierarchy sets, so the conclusion of pinning is an equality of first projections rather than an equality of proof-carrying records in S.
Wv = fst W
The environment tower supplies the row for a formula's arity, while the clause frame combines that row with the formula key, its tagged code, and a proposed table value. Reading a constructor clause at this frame exposes the semantic relation that characterizes the proposed value by its members.
module TR = TowerRead E w (N f0) γ W qw (tg f0) hE module Fr = Frame T w C E N γ tg module Cl = Clause T w C E N module R = Rel T w N
The packaged hypothesis hT contains totality, the assertion that table entries are over C, and the conjunction of the ten constructor clauses. The pinning proof uses totality to obtain child entries and uses the constructor clauses to characterize values. Its particular candidate entry is supplied directly, so the domain assertion hOn is retained from the package but is not needed by this uniqueness argument.
hTot = hT .fst hOn = hT .snd .fst hTen = hT .snd .snd
The ten constructor clauses are stored as one finite conjunction indexed by Fin 10. The reader bigAnd-out turns this package into a family cl k, so a structural case can select exactly the clause named by its constructor tag without changing any of the other nine clauses.
cl : (k : Fin 10) → ⟨ γ ⊨ Cl.clause k ⟩ cl = bigAnd-out γ 9 Cl.clause hTen
The case module packages the data of one induction step: a formula, its tag, its payload set, the equation between code and payload, membership of its key in the code domain, a candidate table entry, and the entry's membership. The tower reading supplies the canonical tower entry for the formula's arity.
module Case {n : ℕ} (ψ : Formula Ab n) (k : Fin 10) (rS : S) (ep : cd ψ ≡ pr (# (toℕ k)) (fst rS)) (c∈ : ⟨ fst (keyS W ψ) ∈ Cv ⟩) (y : S) (mem : ⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩) where q∈ : ⟨ pr (# n) (fst (envSet W n)) ∈ Ev ⟩ q∈ = TR.entry-in n
The formula code is initially written with the canonical numeral # k; the tag equation rewrites that numeral as the value stored at slot N k. The resulting equality fits the clause interface. The frame δ12 then prepends twelve coordinates to the ambient environment, including the arity row, formula key and code, payload, and candidate value.
ep' : fst (codeS W ψ) ≡ pr (fst (lookup (N k) γ)) (fst rS) ep' = ep ∙ cong (λ a → pr a (fst rS)) (sym (tg k)) δ12 : S ^ (12 + m) δ12 = Fr.At.δ12 (nn n) (envSet W n) (keyS W ψ) (codeS W ψ) rS y q∈ refl k ep' mem rel : ⟨ δ12 ⊨ R.relN (toℕ k) ⟩
Applying the selected clause to this concrete frame yields satisfaction of the tag-indexed relation relN k. The relation reader is then fixed at δ12; later constructor-specific readers extend this same frame and unpack rel into the extension fact appropriate to an atom, binary connective, or quantifier.
rel = Fr.clause-out k (cl k) (nn n) (envSet W n) (keyS W ψ) (codeS W ψ) rS y q∈ c∈ refl ep mem module RR = RelRead T w N δ12
If a child formula key belongs to Cv, table totality gives only the propositional truncation of a pair consisting of a value ya and an entry at that key. Thus sub proves mere existence, not a selected value. Each recursive case eliminates this witness directly into equality of hierarchy sets, where the h-set structure makes the target a proposition.
sub : ∀ {n} (a : Formula Ab n) → ⟨ fst (keyS W a) ∈ Cv ⟩ → ∥ Σ[ ya ∈ S ] ⟨ pr (fst (keyS W a)) (fst ya) ∈ Tv ⟩ ∥₁ sub a a∈ = Fr.total-out hTot (keyS W a) a∈
The central predicate is conditional. If the key of ψ lies in the code domain, then every table value y recorded at that key has the same underlying set as the recursively defined satisfaction set of ψ. The conditionality is the honest form: nothing is asserted for keys outside the domain.
Pinned : ∀ {n} (ψ : Formula Ab n) → Type (ℓ-suc ℓ) Pinned ψ = ⟨ fst (keyS W ψ) ∈ Cv ⟩ → (y : S) → ⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩ → fst y ≡ fst (SatW ψ)
The proof of Pinned is organized by structural recursion on the given formula. Recursive calls are made only for immediate formula children supplied by the syntax constructor. There is no recursion on members of C, no well-founded recursion on arbitrary codes, and no attempt to define a value for a code that has not already been identified with a formula key.
private
The payload set of a coded formula is recovered from the code equation by the pairing projection.
payS : ∀ {n} (ψ : Formula Ab n) (k : ℕ) (r : V ℓ) → cd ψ ≡ pr (# k) r → S payS ψ k r e = sndS (codeS W ψ) (# k) r e
All three binary connectives share the same recursive pattern. The parameters identify the constructor, its tag and payload equation, the corresponding object-language relation, and a semantic bridge. That bridge assumes equalities identifying two coordinates of an extended environment with the canonical satisfaction sets of the two children, and from them produces an extension fact for the canonical value of the compound.
binCase : ∀ {n} (op : ∀ {j} → Formula S j → Formula S j → Formula S j) (opA : Formula Ab n → Formula Ab n → Formula Ab n) (k : Fin 10) (a b : Formula Ab n) (code : cd (opA a b) ≡ pr (# (toℕ k)) (pr (cd a) (cd b))) (relIs : R.relN (toℕ k) ≡ R.binRel op) (bridge : ∀ {j} (env : S ^ j) (ya yb : Fin j)
The bridge is formulated for an environment containing the two child values at named coordinates. A separate closure reader turns membership of the compound key in Cv into membership of both child keys, at the same arity. The recursive hypotheses can then identify whichever child entries totality provides with SatW a and SatW b.
→ fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b) → ExtFact (fst (SatW (opA a b))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ op (var i0 ∈̇ var (suc ya)) (var i0 ∈̇ var (suc yb)) ⟩)) → (cl2 : ⟨ fst (keyS W (opA a b)) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩)
To prove the compound is pinned, the proof eliminates the propositionally truncated left value, right value, and binary-relation witness. Every elimination ends in the equality fst y ≡ fst (SatW (opA a b)). Since V is an h-set, this equality is a proposition, so the eliminations reveal no permanent choice of child values or frame data.
→ Pinned a → Pinned b → Pinned (opA a b) binCase {n} op opA k a b code relIs bridge cl2 ia ib c∈ y mem = PT.rec (setIsSet _ _) (λ { (ya , ma) → PT.rec (setIsSet _ _) (λ { (yb , mb) → PT.rec (setIsSet _ _) (λ { (s , s₁ , e₁ , s₂ , e₂ , ext) →
The binary-relation reader extends the common clause frame with the two child codes, keys, and values, together with its auxiliary witnesses. In this extended environment the clause supplies an extension fact for the candidate y, while the bridge supplies the corresponding extension fact for SatW (opA a b). The theorem ext-unique applies set extensionality to these two facts and equates their underlying sets.
let env = yb ∷ keyS W b ∷ s₂ ∷ e₂ ∷ ya ∷ keyS W a ∷ s₁ ∷ e₁ ∷ codeS W b ∷ codeS W a ∷ s ∷ K.δ12 P : S → Type (ℓ-suc ℓ) P z = ⟨ (z ∷ env) ⊨ R.binBody op ⟩ in ext-unique y (SatW (opA a b)) (envSet W n) P ext (bridge env i4 i0 (ia (cl2 c∈ .fst) ya ma) (ib (cl2 c∈ .snd) yb mb)) })
The relation reading is obtained from the clause by the tag identification, and the child values are obtained from the table's totality, in the order left child first, then right child.
(K.RR.bin-out op (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) (codeS W a) (codeS W b) (keyS W a) ya (keyS W b) yb refl ma refl mb refl) }) (sub b (cl2 c∈ .snd)) }) (sub a (cl2 c∈ .fst)) where
The local module K records the compound formula itself, its constructor tag, a constructible representative of the paired child-code payload, the compound key's domain membership, and the candidate entry. It therefore fixes one concrete clause frame for the entire binary argument; the recursive hypotheses concern only the two immediate children.
module K = Case (opA a b) k (payS (opA a b) (toℕ k) (pr (cd a) (cd b)) code) code c∈ y mem
The two unbounded quantifiers also share one recursive case. Their body has successor arity, and the payload is just that body's code. The semantic bridge receives coordinates for the fixed carrier and for a table value of the body; after that value is identified with SatW a, the bridge characterizes the canonical satisfaction set of the quantified formula over envSet W n.
quCase : ∀ {n} (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) (qA : Formula Ab (suc n) → Formula Ab n) (k : Fin 10) (a : Formula Ab (suc n)) (code : cd (qA a) ≡ pr (# (toℕ k)) (cd a)) (relIs : R.relN (toℕ k) ≡ R.quRel q) (bridge : ∀ {j} (env : S ^ j) (wi yai : Fin j)
The carrier coordinate remains in the original ambient environment and is reached after the frame extensions by an index shift; the child value is a newly exposed coordinate of the relation witness. Closure supplies membership of the successor-arity body key, and the recursive hypothesis identifies every table entry at that key with the body's canonical satisfaction set. The bridge then matches the object-language quantifier with quantification over Wv.
→ fst (lookup wi env) ≡ Wv → fst (lookup yai env) ≡ fst (SatW a) → ExtFact (fst (SatW (qA a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ q (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2)) ⟩)) → (cl1 : ⟨ fst (keyS W (qA a)) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩) → Pinned a → Pinned (qA a)
The proof first eliminates the propositionally truncated body value and then the propositionally truncated witness obtained by reading the quantifier relation. That witness extends the common clause frame with the successor numeral, the body key, its value, and auxiliary coordinates. Both eliminations target the equality between the candidate value and the canonical quantified satisfaction set, so no body value is selected globally.
quCase {n} q qA k a code relIs bridge cl1 ia c∈ y mem = PT.rec (setIsSet _ _) (λ { (ya , ma) → PT.rec (setIsSet _ _) (λ { (s , s' , e' , ext) → let env = nn (suc n) ∷ s' ∷ ya ∷ keyS W a ∷ s ∷ e' ∷ K.δ12
At the extended environment, the relation clause provides an extension fact for the candidate table value y. The recursive hypothesis supplies the equality needed for the bridge, and the bridge provides the matching extension fact for SatW (qA a), using the carrier equation at its shifted coordinate. Set extensionality in ext-unique then identifies the two underlying sets.
P : S → Type (ℓ-suc ℓ) P z = ⟨ (z ∷ env) ⊨ R.quBody q ⟩ in ext-unique y (SatW (qA a)) (envSet W n) P ext (bridge env (sh 18 w) i2 qw (ia (cl1 c∈) ya ma)) }) (K.RR.qu-out q (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) (keyS W a) ya (nn (suc n)) ma refl refl) }) (sub a (cl1 c∈))
Here K is instantiated with the quantified formula qA a, not with its body a. Its payload representative is constructed from the body's code, while the domain membership and candidate entry belong to the quantified formula's key. The body appears separately as the sole recursive child, at successor arity.
where module K = Case (qA a) k (payS (qA a) (toℕ k) (cd a) code) code c∈ y mem
For a bounded quantifier, the constructor code has two payload components: the code of the bounding term and the code of the body, whose arity is one larger. The case lemma therefore asks for the constructor tag and payload equation, the corresponding relation clause, a fixed five-slot presentation of its semantic body, an extension bridge for that presentation, and the one closure implication actually needed later: membership of the compound key in the domain implies membership of the body key. No closure condition is imposed on the term code.
bqCase : ∀ {n} (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) (c : ∀ {j} → Formula S j → Formula S j → Formula S j) (qA : Term Ab n → Formula Ab (suc n) → Formula Ab n) (k : Fin 10) (t : Term Ab n) (a : Formula Ab (suc n)) (code : cd (qA t a) ≡ pr (# (toℕ k)) (pr (ct t) (cd a))) (relIs : R.relN (toℕ k) ≡ R.bqRel q c)
The body equation records how the bounded-quantifier body is spelled with five shifted slots, so that the bridge can be stated at a fixed formula shape without depending on the exact slot indices of the calling site.
(body : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S (1 + j)) (bodyIs : ∀ {j} (wi ti yai N0i N1i : Fin j) → body wi ti yai N0i N1i ≡ q (var (suc wi)) (c (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i))) (q (var (suc (suc wi))) (c (var i0 ∈̇ var i1) (∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3))))))
The bridge identifies the recursively defined satisfaction set of the bounded formula with the extension described by this five-slot body over encoded environments. Its quantifier and connective are still parameters here, so the statement covers both the universal and existential bounded cases; it must not be read as asserting existential membership in every instance. This extension fact is what can be compared with the extension fact extracted from the table clause.
(bridge : ∀ {j} (env : S ^ j) (wi ti yai N0i N1i : Fin j) → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup yai env) ≡ fst (SatW a) → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1 → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ body wi ti yai N0i N1i ⟩)) → (cl1 : ⟨ fst (keyS W (qA t a)) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩)
Assume that membership of the compound key yields membership of the body key and that entries at the body key are already pinned. Then every supplied entry at the compound key is pinned as well. Totality gives only a merely existing body value, and the bounded-clause reader likewise hides its witnesses propositionally. Both may be eliminated here because the conclusion is an equality of underlying hierarchy sets, hence a proposition. The supplied compound entry itself is not obtained from totality and is not hidden by truncation.
→ Pinned a → Pinned (qA t a) bqCase {n} q c qA k t a code relIs body bodyIs bridge cl1 ia c∈ y mem = PT.rec (setIsSet _ _) (λ { (ya , ma) → PT.rec (setIsSet _ _) (λ { (s , s₁ , s' , e' , ext) →
After the clause witnesses have been read, the proof forms the extended environment containing the successor arity, the body entry and key, the body code, and the bounding-term code. At that one environment, ext-unique compares the clause's extension fact for the candidate table value with the bridge's extension fact for the recursive satisfaction value. Transport along the body equation makes the predicates in those two facts identical.
let env = nn (suc n) ∷ s' ∷ ya ∷ keyS W a ∷ s₁ ∷ e' ∷ codeS W a ∷ tS ∷ s ∷ K.δ12 P : S → Type (ℓ-suc ℓ) P z = ⟨ (z ∷ env) ⊨ R.bqBody q c ⟩ in ext-unique y (SatW (qA t a)) (envSet W n) P ext (subst (λ φ → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩))
The body entry obtained from totality is identified with the recursive satisfaction set by the induction hypothesis, after closure has supplied membership of the body key. Together with the carrier, term-code, and two tag equations, this identification discharges the bridge assumptions. The outward reading of the bounded clause supplies four auxiliary objects and its extension fact, all only for this local comparison.
(bodyIs (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1))) (bridge env (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1)) qw refl (ia (cl1 c∈) ya ma) (tg f0) (tg f1))) }) (K.RR.bq-out q c (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) tS (codeS W a) (keyS W a) ya (nn (suc n)) refl ma refl refl) }) (sub a (cl1 c∈)) where
Three named components support the case: the payload presented as a carrier element, its first projection carrying the term code, and the case module providing the twelve-slot frame with the table entry at the compound key.
rS : S rS = payS (qA t a) (toℕ k) (pr (ct t) (cd a)) code tS : S tS = fstS rS (ct t) (cd a) refl module K = Case (qA t a) k rS code c∈ y mem
An atomic formula has no formula children, so its case needs no closure implication and no recursive hypothesis. Its constructor payload is the pair of two term codes. The remaining assumptions identify the appropriate atomic relation clause and provide a bridge from the carrier equation, the two term-code equations, and the two tag equations to an extension fact for the atom's recursive satisfaction set.
atomCase : ∀ {n} (opA : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j) (k : Fin 10)
(t u : Term Ab n) (code : cd (opA t u) ≡ pr (# (toℕ k)) (pr (ct t) (ct u)))
(rel : Formula S (18 + m))
(relIs : R.relN (toℕ k) ≡ R.atomRel rel)
(bridge : ∀ (env : S ^ (15 + m)) (wi ti ui N0i N1i : Fin (15 + m))
The bridge parameter states the extension fact for the atomic formula: the satisfaction set contains exactly the environments whose term values satisfy the object-language relation. The conclusion says that this atomic formula is pinned whenever its key lies in the domain and a table entry is supplied.
→ fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup ui env) ≡ ct u → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1 → ExtFact (fst (SatW (opA t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ atomEx wi ti ui N0i N1i rel ⟩)) → Pinned (opA t u) atomCase {n} opA k t u code rel relIs bridge c∈ y mem =
The atomic clause yields merely an auxiliary set together with an extension fact for the candidate table value. In the environment formed from that set and the two term codes, the atomic bridge gives a second extension fact for the recursive satisfaction value. Since equality in the cumulative hierarchy is a proposition, the hidden clause witness can be eliminated and ext-unique identifies the two underlying sets.
PT.rec (setIsSet _ _) (λ { (s , ext) → let env = uS ∷ tS ∷ s ∷ K.δ12 P : S → Type (ℓ-suc ℓ) P z = ⟨ (z ∷ env) ⊨ R.atomBody rel ⟩
The bridge is applied at the extended environment with the two tag equations and the carrier equation, producing the extension fact for the atomic body. The outward reading of the atomic relation supplies the intermediate set.
in ext-unique y (SatW (opA t u)) (envSet W n) P ext (bridge env (sh 15 w) i1 i0 (sh 15 (N f0)) (sh 15 (N f1)) qw refl refl (tg f0) (tg f1)) }) (K.RR.atom-out rel (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) tS uS refl) where rS : S
Three named components support the atomic case: the payload as a carrier element, the two term codes as its first and second projections, and the case module providing the twelve-slot frame.
rS = payS (opA t u) (toℕ k) (pr (ct t) (ct u)) code tS uS : S tS = fstS rS (ct t) (ct u) refl uS = sndS rS (ct t) (ct u) refl module K = Case (opA t u) k rS code c∈ y mem
For the membership atom, satisfaction at the displayed environment is definitionally the same proposition as membership of the two underlying sets. The two implications in memAgree are therefore identities. This is the local agreement needed by the atomic bridge; it makes no statement about other relation symbols.
memAgree : ∀ {j} (env : S ^ j) (z v x : S)
→ (⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ∈̇ var i0 ⟩ → ⟨ fst v ∈ fst x ⟩) × (⟨ fst v ∈ fst x ⟩ → ⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ∈̇ var i0 ⟩)
memAgree env z v x = (λ h → h) , (λ h → h)
The equality agreement says the same for the equality atom: the object-language equality is the identity of the underlying sets.
eqAgree : ∀ {j} (env : S ^ j) (z v x : S) → (⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ≐ var i0 ⟩ → fst v ≡ fst x) × ((fst v ≡ fst x) → ⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ≐ var i0 ⟩) eqAgree env z v x = (λ h → h) , (λ h → h)
The closure lemma for binary connectives reads the downward closure from the shape satisfaction: if the composite key lies in the domain, then both component keys lie in the domain. The proof is one application of the binary-closure elimination.
clSame : (n k : ℕ) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩ → (ψ a b : Formula Ab n) → cd ψ ≡ pr (# k) (pr (cd a) (cd b)) → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩ clSame n k h ψ a b e c∈ = binSameClosed-out C k γ h (keyS W ψ) (nn n) (codeS W a) (codeS W b) c∈ (cong (pr (# n)) e)
The next form of the binary closure lemma fixes the two child formulas before the shape proof is supplied. Its conclusion is unchanged: domain membership of a key whose payload is the pair of those two formula codes yields domain membership of both child keys. This order lets each structural-recursion branch specialize the common closure fact to its own two children.
clBin : (n k : ℕ) (a b : Formula Ab n)
→ ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
→ (ψ : Formula Ab n) → cd ψ ≡ pr (# k) (pr (cd a) (cd b))
→ ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩
clBin n k a b h ψ e = clSame n k h ψ a b e
For an unbounded quantifier, closure follows the sole formula component of the constructor payload. Thus, if the key of the quantified formula at arity n lies in the domain, then the key of its body at successor arity lies there as well. The statement is local to this presented constructor code; it does not decode arbitrary domain elements.
clQu : (n k : ℕ) (a : Formula Ab (suc n)) (ψ : Formula Ab n)
→ ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩ → cd ψ ≡ pr (# k) (cd a)
→ ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩
clQu n k a ψ h e c∈ =
unSuccClosed-out C k γ h (keyS W ψ) (nn n) (codeS W a) c∈ (cong (pr (# n)) e)
For a bounded quantifier, the payload contains a term code first and a body-formula code second. The closure condition follows only the second component: membership of the compound key implies membership of the body key at successor arity. It deliberately yields no domain-membership claim for the bounding term code.
clBq : (n k : ℕ) (t : Term Ab n) (a : Formula Ab (suc n)) (ψ : Formula Ab n)
→ ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ → cd ψ ≡ pr (# k) (pr (ct t) (cd a))
→ ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩
clBq n k t a ψ h e c∈ =
binSuccClosed-out C k γ h (keyS W ψ) (nn n) tS (codeS W a) c∈ (cong (pr (# n)) e)
Two named components support the bounded-quantifier closure: the payload presented as a carrier element, and its first projection carrying the term code.
where pS : S pS = sndS (codeS W ψ) (# k) (pr (ct t) (cd a)) e tS : S tS = fstS pS (ct t) (cd a) refl
The pinned predicate is proved by structural recursion on the formula. The membership atom applies the atomic case with the identity agreement for the membership relation, consuming no subformula hypotheses.
pinned : ∀ {n} (ψ : Formula Ab n) → Pinned ψ pinned (t ∈̇ u) = atomCase _∈̇_ f0 t u refl (var i1 ∈̇ var i0) refl (λ env wi ti ui N0i N1i qw' qt qu q0 q1 → AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _∈̇_ (λ v x → ⟨ v ∈ x ⟩) (var i1 ∈̇ var i0) (memAgree env) (λ δ h → h) (λ δ h → h))
The equality atom applies the atomic case with the identity agreement for equality. The conjunction case applies the binary case with the conjunction bridge and the binary closure at tag two, consuming the pinned hypotheses for both subformulas.
pinned (t ≐ u) = atomCase _≐_ f1 t u refl (var i1 ≐ var i0) refl (λ env wi ti ui N0i N1i qw' qt qu q0 q1 → AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _≐_ (λ v x → v ≡ x) (var i1 ≐ var i0) (eqAgree env) (λ δ h → h) (λ δ h → h)) pinned {n} (a ∧̇ b) = binCase _∧̇_ _∧̇_ f2 a b refl refl (andBridge a b) (clBin n 2 a b (hcl .fst) (a ∧̇ b) refl) (pinned a) (pinned b)
Disjunction and implication follow the same binary pattern at their own tags. Falsity has no subformulas: its uniqueness is proved directly from the outward reading of the falsity clause and the falsity bridge, which together produce the empty extension.
pinned {n} (a ∨̇ b) = binCase _∨̇_ _∨̇_ f3 a b refl refl (orBridge a b) (clBin n 3 a b (hcl .snd .fst) (a ∨̇ b) refl) (pinned a) (pinned b) pinned {n} (a ⇒̇ b) = binCase _⇒̇_ _⇒̇_ f4 a b refl refl (impBridge a b) (clBin n 4 a b (hcl .snd .snd .fst) (a ⇒̇ b) refl) (pinned a) (pinned b) pinned {n} ⊥̇ c∈ y mem = ext-unique y (SatW ⊥̇) (envSet W n) (λ z → ⟨ (z ∷ K.δ12) ⊨ ⊥̇ ⟩) (extB-out i0 i8 ⊥̇ K.δ12 K.rel) (botBridge n K.δ12) where module K = Case ⊥̇ f5 (nn 0) refl c∈ y mem
The two unbounded quantifier branches use the existential and universal bridges. Closure moves from the quantified formula's key to the body key at successor arity, and the recursive hypothesis pins the body value needed by the bridge. The bounded universal branch follows the same local pattern, but its constructor code also contains a term code; it invokes the bounded case with the universal ∀[]-syntax bridge, while closure still follows only the body.
pinned {n} (∃̇ a) = quCase ∃̇∈ ∃̇_ f6 a refl refl (exBridge a) (clQu n 6 a (∃̇ a) (hcl .snd .snd .snd .fst) refl) (pinned a) pinned {n} (∀̇ a) = quCase ∀̇∈ ∀̇_ f7 a refl refl (allBridge a) (clQu n 7 a (∀̇ a) (hcl .snd .snd .snd .snd .fst) refl) (pinned a) pinned {n} (∀̇∈ t a) = bqCase ∀̇∈ _⇒̇_ ∀̇∈ f8 t a refl refl bqAll (λ _ _ _ _ _ → refl) (λ env wi ti yai N0i N1i qw' qt qa q0 q1 → BqBridge.allInBridge t a env wi ti yai N0i N1i qw' qt qa q0 q1) (clBq n 8 t a (∀̇∈ t a) (hcl .snd .snd .snd .snd .snd .fst) refl) (pinned a)
The bounded existential branch invokes the bounded case with the existential ∃[]-syntax bridge. Its closure conjunct supplies domain membership only for the body key at successor arity, after which the recursive hypothesis pins the body entry. The bounding term is evaluated by the bridge and does not become another recursive subproblem.
pinned {n} (∃̇∈ t a) = bqCase ∃̇∈ _∧̇_ ∃̇∈ f9 t a refl refl bqEx (λ _ _ _ _ _ → refl) (λ env wi ti yai N0i N1i qw' qt qa q0 q1 → BqBridge.exInBridge t a env wi ti yai N0i N1i qw' qt qa q0 q1) (clBq n 9 t a (∃̇∈ t a) (hcl .snd .snd .snd .snd .snd .snd) refl) (pinned a)
Filling all satisfaction clauses
We now prove the converse direction. Rather than extracting recursive values from clauses, we assume that represented values already agree with the recursively defined satisfaction sets and use that agreement to verify every clause. The working set W fixes the alphabet, the satisfaction bridges, and the constructor-code matching used throughout this argument.
module _ (W : S) where open Alphabet W open Bridge W open Match W
Fix the table, carrier, code-domain, and environment-tower slots in one environment, together with the ten numeral tags and the tower specification. The decisive hypothesis val≡ is conditional: for a known formula key and a supplied table entry at that key, it identifies the entry's underlying value with the formula's recursively defined satisfaction set. It neither asserts that every key is represented nor chooses an entry.
module SatHoldsC {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N) (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) (val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → fst c ≡ fst (keyS W ψ) → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩ → fst yc ≡ fst (SatW ψ))
Three further assumptions provide existence only under propositional truncation. A domain member presented as an arity-code pair merely decodes to a formula of that stated arity; totality merely supplies some table value at each domain key; and every table member merely decomposes into a key-value pair whose key belongs to the domain. None of these assumptions defines a reusable decoder or value-selection function.
(decode : (c : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁) (tot : (c : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩ ∥₁) (onc : (e : S) → ⟨ fst e ∈ fst (lookup T γ) ⟩
The final assumption finishes the domain condition by requiring every represented table element to be merely a pair (c,yc) with c in the stated code domain. Thus totality controls entries from keys to values, while this condition controls table members back to domain keys. The abbreviations Tv and Cv name only the underlying table and domain sets used in these local statements.
→ ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ fst (lookup C γ) ⟩) ∥₁) where private Tv = fst (lookup T γ) Cv = fst (lookup C γ)
We also name the underlying environment-tower set and the carrier. The frame, clause, and relation readers then express the same stored data at three scales: the common twelve-object frame, the top-level table conditions, and the constructor-specific relation. These are local views of the fixed environment, not new mathematical assumptions.
Ev = fst (lookup E γ) Wv = fst W module Fr = Frame T w C E N γ tg module Cl = Clause T w C E N module R = Rel T w N
Arity ar F says merely that ar is the numeral of some natural number n and that F is the corresponding encoded-environment set envSet W n. The witness n remains under propositional truncation, so this type records the arity information needed for a proposition-valued proof without choosing an arity for later computation.
Arity : (ar F : S) → Type (ℓ-suc ℓ) Arity ar F = ∥ Σ[ n ∈ ℕ ] ((fst ar ≡ # n) × (fst F ≡ fst (envSet W n))) ∥₁
To obtain such arity evidence, present an element q of the environment tower as the pair (ar,F). The tower specification, together with the carrier equation and the zero-tag equation, is then sufficient to read that pair as a merely existing natural arity and its canonical environment set.
arity : (q ar F : S) → ⟨ fst q ∈ Ev ⟩ → fst q ≡ pr (fst ar) (fst F) → Arity ar F module TR = TowerRead E w (N f0) γ W qw (tg f0) hE
The pair equation transports the membership proof from q to the displayed pair (ar,F). The tower-entry theorem then returns Arity ar F, still under propositional truncation. This step extracts exactly the local arity evidence and does not define a global inverse to the tower encoding.
arity q ar F q∈ eq = TR.entry-out ar F (subst (λ u → ⟨ u ∈ Ev ⟩) eq q∈)
The first top-level table condition is totality on the stated code domain. The hypothesis tot already gives exactly its semantic content, with each value existing only propositionally, so the frame lemma converts it directly into satisfaction of the object-language totality clause.
total : ⟨ γ ⊨ Cl.total ⟩ total = Fr.total-in tot
The second top-level condition says that every represented table element lies over a key in the stated domain. The hypothesis onc is precisely this condition at the level of underlying sets, so the frame lemma turns it into satisfaction of the corresponding object-language clause.
onC : ⟨ γ ⊨ Cl.onC ⟩ onC = Fr.onC-in onc
Each constructor clause is tested on the same twelve-object configuration. The fields listed first record those objects: a tower entry and its arity and environment set, a code-domain element and its constructor payload, and a table entry with its value, together with the auxiliary witnesses required by the object-language formula.
record Args (k : Fin 10) : Type (ℓ-suc ℓ) where field q ar F s c p s1 r s2 e yc s3 : S q∈ : ⟨ fst q ∈ Ev ⟩ eq : fst q ≡ pr (fst ar) (fst F)
The remaining fields state the relations that make those objects one coherent frame. They say that the tower element is the arity-environment pair, the code lies in the domain and splits into arity, tag, and payload, and the table element lies in the table and splits into that code and its proposed value. These are local presentation equations, not uniqueness or global decoding claims.
c∈ : ⟨ fst c ∈ Cv ⟩ ec : fst c ≡ pr (fst ar) (fst p) ep : fst p ≡ pr (# (toℕ k)) (fst r) e∈ : ⟨ fst e ∈ Tv ⟩ ee : fst e ≡ pr (fst c) (fst yc)
Fixing a tag and one coherent twelve-object frame isolates a single constructor-clause problem. All later arguments in this scope refer to the same objects and equations, so the proof can concentrate on how that tag's payload determines the required extension fact.
module Fill (k : Fin 10) (A : Args k) where
open Args A
The frame prepends the twelve objects in the exact coordinate order expected by the clause formula: yc, s3, e, r, s2, p, s1, c, F, ar, s, and q, followed by the original environment γ. Thus the proposed value, table entry, constructor payload, formula code, environment set, arity, and tower entry are interleaved with the four auxiliary witnesses at precisely the indices used by the clause.
frame : S ^ (12 + m) frame = yc ∷ s3 ∷ e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ
At this fixed frame, the relation theorem for a tag can be read or constructed in terms of its semantic extension condition. The filling proof uses the constructive direction: once the decoded payload and the prescribed child values provide the right extension fact, the tag's relation clause follows.
module RR = RelRead T w N frame
The goal of each filling case is the satisfaction of the relation clause for the given tag at the twelve-slot frame.
Goal : Type (ℓ-suc ℓ) Goal = ⟨ frame ⊨ R.relN (toℕ k) ⟩
This goal is proposition-valued because satisfaction of any formula in the structure is an h-proposition. That fact is the exact elimination boundary used later: the merely decoded arity, formula, and constructor shape may be consumed to prove this goal, but they cannot be extracted as reusable computational data.
isPropGoal : isProp Goal isPropGoal = snd (frame ⊨ R.relN (toℕ k))
The transfer lemma is the key move: given the arity equation, the environment-set equation, the formula-code equation fst p ≡ cd ψ, and an extension fact for the satisfaction set of ψ, it produces the corresponding extension fact for the table value at the frame. The three equations align the frame's arity, environment set, and formula-code object with those of the recursive satisfaction set.
transfer : (n : ℕ) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n) → fst p ≡ cd ψ → {j : ℕ} (env : S ^ j) (φ : Formula S (1 + j)) → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩) → RR.Ext env φ transfer n ψ qa qF qp env φ ext =
The frame equations first show that c is the canonical key of the decoded formula and that the supplied table member is the pair of c with yc. The value-agreement hypothesis then identifies the underlying set of yc with the recursive satisfaction set. Finally, transport reverses that value equality and the equation identifying F with the canonical environment set, converting the bridge's extension fact into the extension fact required by the frame.
subst2 (λ Y F' → ExtFact Y F' (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)) (sym (val≡ ψ c yc (ec ∙ cong₂ pr qa qp) (subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈))) (sym qF) ext
The sub-value lemma applies the value-agreement hypothesis at a child entry of the same arity, recovering the satisfaction set from the child's table entry.
subVal : (n : ℕ) (a : Formula Ab n) (c₁ ya e₁ : S) → fst ar ≡ # n → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar) (cd a) → fst ya ≡ fst (SatW a) subVal n a c₁ ya e₁ qa e₁∈ ee₁ e₁' = val≡ a c₁ ya (e₁' ∙ cong (λ v → pr v (cd a)) qa) (subst (λ u → ⟨ u ∈ Tv ⟩) ee₁ e₁∈)
For a quantified body, the child key has successor arity. The additional equation identifies its arity component ar' with the von Neumann successor of the parent arity component; composing this with ar = # n yields the numeral for suc n. The value-agreement hypothesis can therefore identify the child entry with the recursive satisfaction set of the body. This is an arity calculation, not a claim about stages of the constructible hierarchy.
subValS : (n : ℕ) (a : Formula Ab (suc n)) (c₁ ya e₁ ar' : S) → fst ar ≡ # n
→ ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar') (cd a) → fst ar' ≡ sucV (fst ar)
→ fst ya ≡ fst (SatW a)
subValS n a c₁ ya e₁ ar' qa e₁∈ ee₁ e₁' es =
val≡ a c₁ ya (e₁' ∙ cong (λ v → pr v (cd a)) (es ∙ cong sucV qa)) (subst (λ u → ⟨ u ∈ Tv ⟩) ee₁ e₁∈)
The data type collects the decoded arity, environment set, formula, and tag match: everything needed to dispatch on a constructor case.
Data : Type (ℓ-suc ℓ) Data = Σ[ n ∈ ℕ ] ((fst ar ≡ # n) × ((fst F ≡ fst (envSet W n)) × (Σ[ ψ ∈ Formula Ab n ] ((fst p ≡ cd ψ) × MatchN (toℕ k) ψ (fst r)))))
The evidence in data' remains under propositional truncation throughout. First the tower entry merely supplies an arity and its environment set. For each such witness, decode merely supplies a formula at that arity, and PT.map augments it with the constructor-shape proof obtained by matchAt. The outer elimination lands again in a truncated type, so no arity or formula is selected globally.
data' : ∥ Data ∥₁ data' = PT.rec squash₁ (λ { (n , (qa , qF)) → PT.map (λ { (ψ , qp) → n , (qa , qF , ψ , (qp , matchAt ψ (toℕ k) (fst r) (sym qp ∙ ep))) }) (decode c c∈ n (fst p) (ec ∙ cong (λ v → pr v (fst p)) qa)) })
The final argument to the outer truncation eliminator is the local Arity ar F evidence read from the presented tower entry. It initiates the nested, propositionally truncated decoding above; it does not expose the hidden natural-number witness on its own.
(arity q ar F q∈ eq)
For any binary constructor, the two child entries are first identified with the recursive satisfaction sets of the child formulas. The binary bridge then characterizes the recursive satisfaction set of the compound formula by applying the corresponding object-language connective to membership in those two child sets. This common argument will serve conjunction, disjunction, and implication separately.
module BinFill (op : ∀ {j} → Formula S j → Formula S j → Formula S j) (opA : ∀ {j} → Formula Ab j → Formula Ab j → Formula Ab j) (bridge : ∀ {n} (a b : Formula Ab n) {j : ℕ} (env : S ^ j) (ya yb : Fin j) → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b) → ExtFact (fst (SatW (opA a b))) (fst (envSet W n))
The bridge's extension fact is stated at the formula that applies the binary connective to the two membership atoms over the child satisfaction sets.
(λ z → ⟨ (z ∷ env) ⊨ op (var i0 ∈̇ var (suc ya)) (var i0 ∈̇ var (suc yb)) ⟩)) where
The payload equation says that the frame's payload is the pair of the two child codes. Pair injectivity recovers the two component equations separately, and subVal uses them to identify each represented child value with the underlying set of its recursively defined value SatW.
go : (n : ℕ) (a b ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n) → fst p ≡ cd ψ → ψ ≡ opA a b → fst r ≡ pr (cd a) (cd b) → ⟨ frame ⊨ R.binRel op ⟩ go n a b ψ qa qF qp qψ qr = RR.bin-in op (λ a' b' s' c₁ ya s₁ e₁ c₂ yb s₂ e₂ er e₁∈ ee₁ e₁' e₂∈ ee₂ e₂' → let q' = pr-inj (sym er ∙ qr) ya≡ = subVal n a c₁ ya e₁ qa e₁∈ ee₁ (e₁' ∙ cong (pr (fst ar)) (q' .fst))
These two child equalities are placed in the same extended environment as the corresponding table entries. The connective bridge then characterizes SatW (opA a b) by the binary clause, and transfer replaces that canonical value and environment set by the candidate value and environment already present in the frame.
yb≡ = subVal n b c₂ yb e₂ qa e₂∈ ee₂ (e₂' ∙ cong (pr (fst ar)) (q' .snd)) env = yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b' ∷ a' ∷ s' ∷ frame in transfer n (opA a b) qa qF (qp ∙ cong cd qψ) env (R.binBody op) (bridge a b env i4 i0 ya≡ yb≡))
For an unbounded quantified formula, the recursive child has successor arity, while its semantic quantifier still ranges over the carrier W. The abstract constructor q' will therefore be instantiated by ∃[]-syntax or ∀[]-syntax; qA names the corresponding unbounded constructor over the alphabet, and the bridge relates its recursive satisfaction set to that carrier-bounded clause.
module QuFill (q' : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) (qA : ∀ {j} → Formula Ab (suc j) → Formula Ab j) (bridge : ∀ {n} (a : Formula Ab (suc n)) {j : ℕ} (env : S ^ j) (wi yai : Fin j) → fst (lookup wi env) ≡ Wv → fst (lookup yai env) ≡ fst (SatW a) → ExtFact (fst (SatW (qA a))) (fst (envSet W n))
The clause tests a candidate encoded environment z. Its outer constructor, later instantiated as ∃[]-syntax or ∀[]-syntax, ranges over the carrier W; for each such element, the inner ∃[]-syntax asks for a member of the child's represented satisfaction set that is the encoded environment obtained by adjoining that element to z. This is the object-language description of one quantifier step, not a decoder or a reusable choice of witnesses.
(λ z → ⟨ (z ∷ env) ⊨ q' (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2)) ⟩)) where
The decoded formula has arity n, whereas its quantified body has arity suc n. The successor equation supplied by the relation reader lets subValS rewrite the body's key to that arity and identify its represented value with SatW a; the quantifier bridge can then use precisely the recursive child value required by the clause.
go : (n : ℕ) (a : Formula Ab (suc n)) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n) → fst p ≡ cd ψ → ψ ≡ qA a → fst r ≡ cd a → ⟨ frame ⊨ R.quRel q' ⟩ go n a ψ qa qF qp qψ qr = RR.qu-in q' (λ c₁ ya ar' s' s'' e' e'∈ ee₁ e₁' es → let ya≡ = subValS n a c₁ ya e' ar' qa e'∈ ee₁ (e₁' ∙ cong (pr (fst ar')) qr) es env = ar' ∷ s'' ∷ ya ∷ c₁ ∷ s' ∷ e' ∷ frame
The bridge supplies an extension fact for the canonical value SatW (qA a). The arity, environment-set, and code equations then let transfer turn that fact into the extension statement demanded for the candidate table value in this frame, completing the unbounded-quantifier clause.
in transfer n (qA a) qa qF (qp ∙ cong cd qψ) env (R.quBody q') (bridge a env (sh 18 w) i2 qw ya≡))
A bounded quantified formula has only one recursive formula child: its bounding term is evaluated inside the semantic bridge. The abstract data separate the bounded quantifier, the connective used to combine its conditions, the alphabet-level constructor, and the exact object-language clause body, so the same argument covers both universal and existential forms without treating the term code as a subformula.
module BqFill (q' : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) (c' : ∀ {j} → Formula S j → Formula S j → Formula S j) (qA : ∀ {j} → Term Ab j → Formula Ab (suc j) → Formula Ab j) (body : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S (1 + j)) (bodyIs : ∀ {j} (wi ti yai N0i N1i : Fin j)
The equation bodyIs identifies the generic clause body with its three bounded layers. The outer layer ranges over a proposed value of the bounding term in W, tmIs verifies that proposal, the next layer ranges over elements of that value that also lie in W, and the innermost ∃[]-syntax asks for the encoded extended environment in the child's satisfaction set. This equation concerns the semantic clause body, rather than the original formula body itself.
→ body wi ti yai N0i N1i ≡ q' (var (suc wi)) (c' (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i))) (q' (var (suc (suc wi))) (c' (var i0 ∈̇ var i1) (∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3)))))) (bridge : ∀ {n} (t : Term Ab n) (a : Formula Ab (suc n)) {j : ℕ} (env : S ^ j) (wi ti yai N0i N1i : Fin j) → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup yai env) ≡ fst (SatW a)
The bridge assumes five equalities locating, in one environment, the carrier, the bounding-term code, the recursive value of the formula child, and the numeral tags 0 and 1. From those hypotheses it proves the extension fact for the bounded formula. Thus the extension fact is the conclusion of the bridge, while the only recursive input is the value of the formula child.
→ fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1 → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ body wi ti yai N0i N1i ⟩)) where
Pair injectivity separates the bounded payload into its term-code component and its formula-code component. The first equality is passed to the term part of the bridge; the second, together with the successor-arity equation, lets subValS identify the represented value of the sole formula child. No recursive table lookup is required for the term code.
go : (n : ℕ) (t : Term Ab n) (a : Formula Ab (suc n)) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n) → fst p ≡ cd ψ → ψ ≡ qA t a → fst r ≡ pr (ct t) (cd a) → ⟨ frame ⊨ R.bqRel q' c' ⟩ go n t a ψ qa qF qp qψ qr = RR.bq-in q' c' (λ t' a' s' c₁ ya ar' s₁ s'' e' er e'∈ ee₁ e₁' es → let q'' = pr-inj (sym er ∙ qr) ya≡ = subValS n a c₁ ya e' ar' qa e'∈ ee₁ (e₁' ∙ cong (pr (fst ar')) (q'' .snd)) es
The concrete bridge proves the extension fact in the canonical bounded-quantifier body. Rewriting by bodyIs places that fact in the generic relation body, after which transfer replaces the canonical satisfaction value by the candidate value represented in the table entry.
env = ar' ∷ s'' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a' ∷ t' ∷ s' ∷ frame in transfer n (qA t a) qa qF (qp ∙ cong cd qψ) env (R.bqBody q' c') (subst (λ φ → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)) (bodyIs (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1))) (bridge t a env (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1)) qw (q'' .fst) ya≡ (tg f0) (tg f1))))
An atomic formula has two term codes but no recursive formula child. Its generic bridge is therefore indexed by the two-place atom constructor and by a relation formula in the enlarged environment; the bridge evaluates both terms and proves the corresponding extension fact directly.
module AtomFill (opA : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j) (rel : Formula S (18 + m)) (bridge : ∀ {n} (t u : Term Ab n) (env : S ^ (15 + m)) (wi ti ui N0i N1i : Fin (15 + m)) → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup ui env) ≡ ct u → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1 → ExtFact (fst (SatW (opA t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ atomEx wi ti ui N0i N1i rel ⟩)) where
The payload equation is again a pair equation, now separating the codes of the two terms. These equations place the term codes in the environment expected by the atomic body. The actual term values are still quantified and verified by the two tmIs clauses inside that body; they are not obtained by recursive table lookup.
go : (n : ℕ) (t u : Term Ab n) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
→ fst p ≡ cd ψ → ψ ≡ opA t u → fst r ≡ pr (ct t) (ct u) → ⟨ frame ⊨ R.atomRel rel ⟩
go n t u ψ qa qF qp qψ qr = RR.atom-in rel (λ t' u' s' er →
let q' = pr-inj (sym er ∙ qr)
env = u' ∷ t' ∷ s' ∷ frame
The three entries prepended to the frame are the two payload term codes and their pair container. With their component equations established, the atomic bridge characterizes the canonical satisfaction set by the chosen relation, and transfer moves that characterization to the candidate table value.
in transfer n (opA t u) qa qF (qp ∙ cong cd qψ) env (R.atomBody rel) (bridge t u env (sh 15 w) i1 i0 (sh 15 (N f0)) (sh 15 (N f1)) qw (q' .fst) (q' .snd) (tg f0) (tg f1)))
Bottom has neither term data nor a formula child. Its bridge says directly that the recursive satisfaction set has the empty extension over envSet W n; transfer rewrites this fact to the candidate table value, and the relation constructor packages it as the bottom clause.
botGo : (n : ℕ) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n) → fst p ≡ cd ψ → ψ ≡ ⊥̇ → ⟨ frame ⊨ R.botRel ⟩ botGo n ψ qa qF qp qψ = extB-in i0 i8 ⊥̇ frame (transfer n ⊥̇ qa qF (qp ∙ cong cd qψ) frame ⊥̇ (botBridge n frame))
Tag 0 is the membership atom. Here the relation formula already means ordinary membership in the constructible structure, so both directions of the agreement proof and both directions connecting atomic meaning to membership are identities. The atomic argument still verifies the two term codes and their values before applying that relation.
fill : (k : Fin 10) (A : Args k) → Fill.Data k A → Fill.Goal k A fill f0 A (n , (qa , qF , ψ , (qp , (t , u , (qψ , qr))))) = Fill.AtomFill.go f0 A _∈̇_ (var i1 ∈̇ var i0) (λ t u env wi ti ui N0i N1i qw' qt qu q0 q1 → AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _∈̇_ (λ v x → ⟨ v ∈ x ⟩)
Tag 1 is handled in the same way for equality. Object-language equality is interpreted by equality of the underlying hierarchy sets, so the agreement and semantic conversion maps again require no transport beyond the identities already displayed.
(var i1 ∈̇ var i0) (λ z v x → (λ h → h) , (λ h → h)) (λ δ h → h) (λ δ h → h)) n t u ψ qa qF qp qψ qr fill f1 A (n , (qa , qF , ψ , (qp , (t , u , (qψ , qr))))) = Fill.AtomFill.go f1 A _≐_ (var i1 ≐ var i0) (λ t u env wi ti ui N0i N1i qw' qt qu q0 q1 →
Tags 2, 3, and 4 use the common binary argument with the bridges for conjunction, disjunction, and implication. Tag 5 is the childless bottom case. This part of the dispatch therefore follows the constructor code exactly, while all recursive information remains confined to the two child values required by a binary connective.
AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _≐_ (λ v x → v ≡ x) (var i1 ≐ var i0) (λ z v x → (λ h → h) , (λ h → h)) (λ δ h → h) (λ δ h → h)) n t u ψ qa qF qp qψ qr fill f2 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f2 A _∧̇_ _∧̇_ andBridge n a b ψ qa qF qp qψ qr fill f3 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f3 A _∨̇_ _∨̇_ orBridge n a b ψ qa qF qp qψ qr
Tags 6 and 7 represent the unbounded existential and universal formulas. Their semantic clauses use ∃[]-syntax and ∀[]-syntax to range over the carrier W, with the recursive body value at successor arity. The remaining two tags begin the bounded cases, where the same bounded constructors are combined with conjunction or implication to express the term bound as well.
fill f4 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f4 A _⇒̇_ _⇒̇_ impBridge n a b ψ qa qF qp qψ qr fill f5 A (n , (qa , qF , ψ , (qp , (qψ , qr)))) = Fill.botGo f5 A n ψ qa qF qp qψ fill f6 A (n , (qa , qF , ψ , (qp , (a , (qψ , qr))))) = Fill.QuFill.go f6 A ∃̇∈ ∃̇_ exBridge n a ψ qa qF qp qψ qr fill f7 A (n , (qa , qF , ψ , (qp , (a , (qψ , qr))))) = Fill.QuFill.go f7 A ∀̇∈ ∀̇_ allBridge n a ψ qa qF qp qψ qr fill f8 A (n , (qa , qF , ψ , (qp , (t , a , (qψ , qr))))) =
For the bounded universal, the canonical body already has the abstract shape required by BqFill, so bodyIs is reflexivity. Its nested uses of ∀[]-syntax express that every verified value of the bounding term, and every carrier element lying in that value, must lead to an encoded environment in the recursive child set.
Fill.BqFill.go f8 A ∀̇∈ _⇒̇_ ∀̇∈ bqAll (λ _ _ _ _ _ → refl) (λ t a env wi ti yai N0i N1i qw' qt qa' q0 q1 → BqBridge.allInBridge t a env wi ti yai N0i N1i qw' qt qa' q0 q1) n t a ψ qa qF qp qψ qr fill f9 A (n , (qa , qF , ψ , (qp , (t , a , (qψ , qr))))) = Fill.BqFill.go f9 A ∃̇∈ _∧̇_ ∃̇∈ bqEx (λ _ _ _ _ _ → refl)
The bounded existential uses the parallel three-layer body with ∃[]-syntax, joining the term-value condition, membership in that value, and membership of the extended environment in the child set by conjunctions. Its body also matches by reflexivity, and tag 9 completes the ten constructor cases.
(λ t a env wi ti yai N0i N1i qw' qt qa' q0 q1 → BqBridge.exInBridge t a env wi ti yai N0i N1i qw' qt qa' q0 q1) n t a ψ qa qF qp qψ qr
To prove one constructor clause, the twelve objects and their membership and pairing equations are first collected into Args k. This fixes a single matching frame. The decoded arity, formula, and constructor shape remain inside propositional truncation in Fill.data', because the original hypotheses do not choose any of them.
clause : (k : Fin 10) → ⟨ γ ⊨ Cl.clause k ⟩ clause k = Fr.clause-in k (λ q ar F s c p s1 r s2 e yc s3 q∈ eq c∈ ec ep e∈ ee → let A : Args k A = record { q = q ; ar = ar ; F = F ; s = s ; c = c ; p = p ; s1 = s1 ; r = r ; s2 = s2 ; e = e ; yc = yc ; s3 = s3 ; q∈ = q∈ ; eq = eq ; c∈ = c∈ ; ec = ec ; ep = ep ; e∈ = e∈ ; ee = ee }
Formula satisfaction is a proposition, so Fill.Goal k A is a valid target for eliminating the propositionally truncated data. For each hidden witness, fill proves the same clause goal; propositionality then makes the result independent of which arity, formula, or decomposition witnessed the decoding. No reusable decoder or table-value choice escapes this elimination.
in PT.rec (Fill.isPropGoal k A) (fill k A) (Fill.data' k A))
The ten constructor clauses are joined into one finite conjunction. This conjunction is the ten component of the full table specification; totality and the on-domain condition are added separately in the next step.
ten : ⟨ γ ⊨ Cl.ten ⟩ ten = bigAnd-in γ 9 Cl.clause clause
The three parts now fit the definition of tableAt: total gives a merely existing table value for every code in C, onC says every table member has a key in C, and ten supplies all constructor clauses. Together they prove that the given relation satisfies the table specification, without asserting that it is a globally chosen function or that its values are unique.
holds : ⟨ γ ⊨ tableAt T w C E N ⟩ holds = total , (onC , ten)
Specializing to one formula's slot
Fixing W determines two linked viewpoints. Alphabet W supplies formulas whose constants name members of W and their codes, while Bridge W interprets those constants in the constructible carrier and compares recursive satisfaction with the object-language clauses. The specialization below uses both viewpoints for the slot generated by one formula.
module _ (W : S) where open Alphabet W open Bridge W
If x belongs to the slot generated by ψ, then, under propositional truncation, there are an arity m and a formula χ : Formula Ab m such that x is the underlying set of keyS W χ. The result preserves existence of such a formula key, but chooses no formula and retains no explicit proof that χ is a subformula of ψ.
slotAb : ∀ {n} (ψ : Formula Ab n) (x : V ℓ) → ⟨ x ∈ fst (slot W (toS ψ)) ⟩ → ∥ Σ[ m ∈ ℕ ] Σ[ χ ∈ Formula Ab m ] (x ≡ fst (keyS W χ)) ∥₁ slotAb ψ x h = PT.map (λ { (m , χ , e , _) → m , χ , (e ∙ sym (keyBridge W χ)) })
The local equality mapped ψ first rewrites the concrete slot as the generic tree that collects keyʟ (toS χ). Applying tree-inv then yields, merely, a contributing formula χ and equality with that internal key. The map keeps this equality and replaces the internal key by keyS W χ using keyBridge; the accompanying subtree inclusion is deliberately discarded by the stated result.
(tree-inv key key ψ x (subst (λ y → ⟨ x ∈ fst y ⟩) (mapped ψ) h)) where key : ∀ {n} → Formula Ab n → S key χ = keyʟ (toS χ)
The equality mapped is proved by structural recursion because toS changes only constants and leaves every formula constructor in place. Membership atoms, equality atoms, and bottom agree definitionally. For a binary connective, the slot consists of the singleton containing the formula's own key together with the union of the two child trees, so the two recursive equalities are combined under the same unions.
mapped : ∀ {n} (χ : Formula Ab n) → slot W (toS χ) ≡ tree key χ mapped (t ∈̇ u) = refl mapped (t ≐ u) = refl mapped ⊥̇ = refl mapped χ@(a ∧̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b))
Conjunction, disjunction, and implication all have the same binary tree shape and therefore use both recursive equalities. Each unbounded quantifier has just one formula body, so its singleton root is joined to one recursively matched child tree. The arity change under the binder affects the type of that child formula, but not this union pattern.
mapped χ@(a ∨̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b)) mapped χ@(a ⇒̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b)) mapped χ@(∃̇ a) = cong (cupʟ (sglʟ (key χ))) (mapped a) mapped χ@(∀̇ a) = cong (cupʟ (sglʟ (key χ))) (mapped a) mapped χ@(∀̇∈ t a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
The bounded universal and existential cases also contribute only the formula body as a child tree. Their bounding terms are part of the constructor payload, not formula subtrees collected by slot. These last two recursive equalities complete the comparison between the concrete slot and the generic key tree.
mapped χ@(∃̇∈ t a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
SlotHolds works in an environment with positions T, w, C, and E for the table, carrier, code domain, and environment tower, together with ten tag positions N. It assumes the carrier, tags, and tower facts, then fixes a base formula ψ0; the equations qT and qC identify only the underlying sets stored at T and C with the canonical table and slot generated by ψ0.
module SlotHolds {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N) (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) {n0 : ℕ} (ψ0 : Formula Ab n0) (qT : fst (lookup T γ) ≡ fst (satTable W (toS ψ0))) (qC : fst (lookup C γ) ≡ fst (slot W (toS ψ0))) where
Only two underlying sets are abbreviated: Tv is the relation stored at the table position T, and Cv is the set stored at the code-domain position C. The following four constructions establish exactly the value-agreement, decoding, totality, and on-domain assumptions needed for these two sets.
private
Tv = fst (lookup T γ)
Cv = fst (lookup C γ)
Suppose c has the same underlying set as the key of a formula ψ, and (c,yc) is represented in Tv. Rewriting by keyBridge and qT turns this into an entry of the canonical table generated by ψ0; entry-out then proves fst yc ≡ fst (SatW ψ). This pins a supplied value at a genuine formula key, but does not assert that such an entry exists.
val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → fst c ≡ fst (keyS W ψ) → ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ → fst yc ≡ fst (SatW ψ) val≡ ψ c yc qc h = entry-out W (toS ψ0) (toS ψ) (fst yc) (subst2 (λ u v → ⟨ pr u (fst yc) ∈ v ⟩) (qc ∙ keyBridge W ψ) qT h)
Decoding starts with both membership c ∈ Cv and a specified arity presentation fst c ≡ pr (# n) z. After transporting membership through qC, slotAb gives, under propositional truncation, some formula at some arity whose key is c. The remaining work must show that this hidden arity is exactly n and that its formula code is exactly z.
decode : (c : S) → ⟨ fst c ∈ Cv ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁ decode c c∈ n z e = PT.map (λ { (n₁ , ψ₁ , e₁) → let q = pr-inj (sym e₁ ∙ e)
The two equations for c give an equality between pairs. Pair injectivity compares their numeral components and code components, and numeral injectivity yields equality of the two arities. Because formulas are indexed by arity, the hidden formula must be transported along that equality; cd-subst then accounts for how its code changes under this dependent transport and produces a formula in Formula Ab n with code z.
nq = #-inj′ (q .fst) in subst (Formula Ab) nq ψ₁ , (sym (q .snd) ∙ sym (cd-subst nq ψ₁)) }) (slotAb ψ0 (fst c) (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈))
For each c ∈ Cv, transport by qC places c in the canonical slot, where slotTotal gives, under propositional truncation, a value y whose pair with c lies in the canonical table. Transport by qT moves that entry back to Tv. The result proves totality as mere existence and does not choose a value function on Cv.
tot : (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁ tot c c∈ = PT.map (λ { (y , h) → y , subst (λ u → ⟨ pr (fst c) (fst y) ∈ u ⟩) (sym qT) h }) (slotTotal W (toS ψ0) (fst c) (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈))
For a member e of Tv, the equation qT first transports its membership to the canonical satisfaction table. The inversion ent-slot then yields, under propositional truncation, an arity m, a formula χ, and an equality between fst e and the underlying set of the canonical entry contributed by χ. Composing that equality with prʟ-fst gives fst e ≡ pr (fst (keyʟ χ)) (fst (Sat W χ)).
onc : (e : S) → ⟨ fst e ∈ Tv ⟩ → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁ onc e e∈ = PT.map (λ { (m , χ , (q , _)) → let ee = q ∙ prʟ-fst (keyʟ χ) (Sat W χ)
Inside that truncated witness, take c = keyʟ χ and yc = Sat W χ. The equality just obtained supplies the required decomposition of e. Its transported membership in the canonical table implies, by inSlot, that the key lies in the canonical slot, and qC moves this fact to Cv. Thus the on-domain condition is established under the same truncation, without choosing a decomposition globally or proving single-valuedness.
in keyʟ χ , Sat W χ , (ee , subst (λ u → ⟨ fst (keyʟ χ) ∈ u ⟩) (sym qC) (inSlot W (toS ψ0) (fst (keyʟ χ)) (fst (Sat W χ)) (subst2 (λ u v → ⟨ u ∈ v ⟩) ee qT e∈))) }) (ent-slot W (toS ψ0) (fst e) (subst (λ u → ⟨ fst e ∈ u ⟩) qT e∈))
The common carrier, tag, and tower hypotheses are now combined with the four facts just proved: value agreement, decoding, totality, and the on-domain decomposition. These are exactly the seven hypotheses of SatHoldsC. Closure is absent in this direction because, when a constructor clause is rebuilt, its relation presents every matching child table entry universally and val≡ pins each supplied child value directly. The decoder handles the current domain code, while tot and onc establish the other two top-level table conditions; no step here derives child-key membership from parent-key membership.
module SH = SatHoldsC W T w C E N γ qw tg hE val≡ decode tot onc
Consequently, the slot and satisfaction table generated by ψ0, as identified by qC and qT, satisfy tableAt T w C E N. This conclusion is the concrete table specification only: it neither proves slot closure nor identifies every table satisfying the specification with the canonical table. Later consumers add slotClosed and apply SatSoundC.pinned when they need uniqueness at a represented key.
holds : ⟨ γ ⊨ tableAt T w C E N ⟩ holds = SH.holds
Recap
Pinned recursion turns an externally supplied table specification into a theorem about the canonical satisfaction table, and conversely shows that the canonical table satisfies that specification. The proof separates the mathematical obligations cleanly: decoding identifies formula codes, totality supplies values merely, the on-domain condition accounts for every table entry, and closure is invoked only in the direction where child keys must be recovered from a represented parent key.