--- title: "Describing the satisfaction table" module: L.Coding.SatisfactionClauses lang: en site: "Bedrock" description: "Describing the satisfaction table" stage: "Internal coding: tables and uniform satisfaction" reading_order: 63 canonical: https://bedrock.institute/en/L.Coding.SatisfactionClauses.html html: L.Coding.SatisfactionClauses.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionClauses.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, L.Constructible, L.Coding.Model, L.Coding.Expressions, L.Coding.Quantification] routes: [internal-satisfaction] translations: [https://bedrock.institute/zh/L.Coding.SatisfactionClauses.md, https://bedrock.institute/ja/L.Coding.SatisfactionClauses.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Describing the satisfaction table The object language cannot invoke the host language's recursion on formulas. It therefore needs a bounded description of the graph that recursion should produce. This chapter treats `T` as a candidate relation of formula keys and environment sets, and asks which local equations each matching entry must obey. The answer consists of ten constructor clauses and two conditions on the first projection of `T`; semantic correctness, uniqueness, closure of the code domain, and existence of canonical data require further arguments. ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` There are two levels in this description. Agda supplies the metatheory in which the construction is checked, while the formulas constructed below belong to the first-order language of the constructible structure. The chapter assumes no excluded middle: it only assembles formulas from intuitionistically valid operations and proves a syntactic boundedness statement. ```agda open import Base.Prelude module L.Coding.SatisfactionClauses {ℓ : Level} where ``` A formula with `j` free slots is interpreted after those slots receive elements of the constructible carrier. Membership, equality, the propositional connectives, and bounded quantifiers are enough to state every clause below. The final Δ₀ witness will concern this object-language syntax; it will not by itself interpret the clauses or provide any of their witnesses. ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; Term; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ ) open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ ) open import L.Constructible {ℓ} using ( 𝒮ʟ ) ``` The candidate relation is expressed through coded ordered pairs. Three shapes organize the chapter: an environment-tower entry pairs an arity `ar` with an environment set `F`; a formula key pairs the same arity with a tagged payload; and a member of `T` pairs that key with a candidate value set. Bounded pair readers expose these components, while the successor and cons predicates describe the arity increase and the extension of an encoded environment. ```agda open import L.Coding.Model {ℓ} using ( prAtL ) open import L.Coding.Expressions {ℓ} using ( sucAtL; consAtL ) open import L.Coding.Quantification {ℓ} using ( f0; f1; i0; i1; i2; i3; i4; i5; i6; i8; i9; i11; i12; i14; i16; i17; i19; sh ; sndEx; sndAll; bothEx; bothAll; bigAnd ) ``` There are exactly ten formula-constructor positions, indexed by `Fin 10`. Converting such an index to a natural number lets one common family dispatch to the appropriate clause. The value stored in a tag slot is still an arbitrary parameter here; a later `Tags` hypothesis will identify each slot with its intended standard numeral. ```agda open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Data.Unit using ( tt ) ``` All object-language variables range over `S`, the carrier of the constructible structure. A slot such as `T`, `C`, or `w` names a position in an assignment; only after evaluation does that position denote a constructible set. Keeping this distinction prevents a syntactic clause from being mistaken for a metatheoretic construction of a table or a code set. ```agda open hPropStructure 𝒮ʟ using ( S ) ``` ## The table frame and its ten clauses The first reusable idea is an exact extension condition. For a proposed set `y`, a reference set `F`, and a property `φ`, the first half of `extB` says that every member of `y` lies in `F` and satisfies `φ`; hence it gives one inclusion. The second half says that every member of `F` satisfying `φ` lies in `y`, giving the reverse inclusion. Thus `extB` characterizes `y` as the subset of `F` cut out by `φ`, but it neither constructs such a set nor asserts that one exists. ```agda extB : ∀ {j} → Fin j → Fin j → Formula S (1 + j) → Formula S j extB y F φ = ∀̇∈ (var y) ((var i0 ∈̇ var (sh 1 F)) ∧̇ φ) ∧̇ ∀̇∈ (var F) (φ ⇒̇ (var i0 ∈̇ var (sh 1 y))) ``` To inspect a coded pair when its second component `v` is already known, `fstAll` ranges universally through the bounded containers used by the pair coding. Whenever the pair predicate identifies a candidate first component, the body must hold with that component added to the assignment. The two bounded universals serve the set-theoretic representation of an ordered pair; mathematically this is one guarded reading of its first component, applied to every possible decomposition. ```agda fstAll : ∀ {j} → Fin j → Fin j → Formula S (2 + j) → Formula S j fstAll x v body = ∀̇∈ (var x) (∀̇∈ (var i0) (prAtL (sh 2 x) i0 (sh 2 v) ⇒̇ body)) ``` Formula recursion first needs a same-arity lookup. `subAt T ar a body` requires `body` for every entry of `T` whose key is the pair `(ar,a)`. It is a universal implication over matching entries, so it selects no entry and proves no value unique. If the key has no entry, the condition may hold vacuously; obtaining an entry later requires both totality and a separate proof that the child key belongs to the code domain. ```agda subAt : ∀ {j} → Fin j → Fin j → Fin j → Formula S (4 + j) → Formula S j subAt T ar a body = ∀̇∈ (var T) (bothAll i0 (prAtL i1 (sh 4 ar) (sh 4 a) ⇒̇ body)) ``` A quantified formula has one more available variable in its body, so its recursive lookup must change the arity. `subSucAt T ar a body` considers every table entry whose key is `(ar',a)` and uses the additional guard `ar' = suc ar`; only then is `body` required. As with the same-arity reader, both the entry and the decomposition are universally quantified. The formula neither chooses `ar'` or a value nor guarantees that the raised child key occurs in `T`. ```agda subSucAt : ∀ {j} → Fin j → Fin j → Fin j → Formula S (6 + j) → Formula S j subSucAt T ar a body = ∀̇∈ (var T) (bothAll i0 (fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body))) ``` Term evaluation has two code shapes. `tmIs t z v N0 N1` says that `t` is either the constant code carrying `v`, or a variable code carrying an index `i` for which the graph entry `(i,v)` belongs to the encoded environment `z`. The disjunction and the variable-index witness are interpreted under propositional truncation. Moreover, `N0` and `N1` are only tag slots until a later `Tags` hypothesis identifies them with zero and one; for an arbitrary multivalued `z`, the same variable code may validate several candidate values. ```agda tmIs : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S j tmIs t z v N0 N1 = prAtL t N0 v ∨̇ sndEx t N1 (∃̇∈ (var (sh 2 z)) (prAtL i0 i1 (sh 3 v))) ``` The five constructor relations below share three parameters: the candidate relation `T`, the carrier bound `w`, and the family of ten tag slots `N`. Their local names `N0` and `N1` merely shift the first two tag slots past newly bound variables. This bookkeeping preserves which slots are referenced; it adds no equation identifying those slots with standard numerals. ```agda module Rel {m : ℕ} (T w : Fin m) (N : Fin 10 → Fin m) where private N0 N1 : ∀ {j} → Fin (j + m) N0 {j} = sh j (N f0) N1 {j} = sh j (N f1) ``` Once the two child values `ya` and `yb` have been read, a binary clause asks how one encoded environment `z` relates to them. The two propositions are simply `z ∈ ya` and `z ∈ yb`; the parameter `op` combines them. Instantiating `op` by conjunction, disjunction, or implication preserves the corresponding polarity without collapsing all three connectives into the same condition. ```agda binBody : (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S (24 + m) binBody op = op (var i0 ∈̇ var i5) (var i0 ∈̇ var i1) ``` For an unbounded quantifier of the encoded formula, the describing formula uses `w` as an explicit bound. With `q` instantiated by `∃[]-syntax`, it merely asserts under propositional truncation that some `x ∈ w` works; with `q` instantiated by `∀[]-syntax`, every `x ∈ w` must work. In either case the inner condition merely asks for an encoded extension `e'` in the body-value set such that `e'` is obtained by consing `x` onto `z`. This inner existence is propositionally truncated and supplies no globally chosen extension function. ```agda quBody : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → Formula S (19 + m) quBody q = q (var (sh 19 w)) (∃̇∈ (var i4) (consAtL i0 i1 i2)) ``` A bounded quantifier must also evaluate its bound term. For the universal case, `∀[]-syntax` together with implication requires every candidate `v` validated by `tmIs`, and then every `x ∈ w` belonging to `v`, to admit a merely existing encoded extension in the body-value set. For the existential case, `∃[]-syntax` together with conjunction asks merely for such a validated `v`, such an `x`, and such an extension. If the encoded environment relation is multivalued, these polarities remain significant; this clause does not repair it or prove term values unique. ```agda bqBody : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S (22 + m) bqBody q c = q (var (sh 22 w)) (c (tmIs i9 i1 i0 N0 N1) (q (var (sh 23 w)) (c (var i0 ∈̇ var i1) (∃̇∈ (var i5) (consAtL i0 i1 i3))))) ``` Atomic formulas do not recurse through formula children. Their payload consists of two term codes, so the atomic body merely asks, under propositional truncation, for two values `v,x ∈ w` validated by `tmIs`, and then tests the chosen atomic relation on them. Membership uses `v ∈ x`, while equality compares `v` and `x`; the term values come directly from the constant or variable shape rather than from entries of `T`. ```agda atomBody : Formula S (18 + m) → Formula S (16 + m) atomBody rel = ∃̇∈ (var (sh 16 w)) (∃̇∈ (var (sh 17 w)) (tmIs i4 i2 i1 N0 N1 ∧̇ (tmIs i3 i2 i0 N0 N1 ∧̇ rel))) ``` Falsity gives the simplest extension equation. Its property is impossible, so the forward inclusion says that the candidate value `yc` has no members. The reverse inclusion is immediate because no member of `F` can satisfy falsity. Thus the clause characterizes `yc` as empty without constructing an empty value or a table entry. ```agda botRel : Formula S (12 + m) botRel = extB i0 i8 ⊥̇ ``` For a binary connective, the payload is decomposed into two formula codes `a` and `b`. The two same-arity readers then range over every value of `T` matching the child keys `(ar,a)` and `(ar,b)`. For every resulting pair of child values, `extB` characterizes `yc` by the binary body. A multivalued candidate relation therefore imposes the equation for every combination; this relation constructor assumes neither existence nor uniqueness of either child value. ```agda binRel : (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S (12 + m) binRel op = bothAll i3 (subAt (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (binBody op)))) ``` The payload of an unbounded quantified formula is its body code. The relation reads that code only at successor arity and then uses `extB` to compare the candidate value with the environments satisfying the quantifier body. Although the encoded quantifier ranges semantically over the whole intended carrier, the describing formula ranges over the explicit set `w`; this is what keeps the description bounded. ```agda quRel : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → Formula S (12 + m) quRel q = subSucAt (sh 12 T) i9 i3 (extB i6 i14 (quBody q)) ``` The payload of a bounded quantifier is a pair `(t,a)` of a bound-term code and a body code. Only `a` is looked up recursively, again at successor arity; `t` is evaluated locally by `tmIs`. The two parameters will later give the exact polarities: the bounded universal uses `∀[]-syntax` with implication, and the bounded existential uses `∃[]-syntax` with conjunction. ```agda bqRel : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S (12 + m) bqRel q c = bothAll i3 (subSucAt (sh 15 T) i12 i0 (extB i9 i17 (bqBody q c))) ``` For an atomic payload, the pair reader exposes the two term codes and `extB` applies the atomic body to every candidate encoded environment in `F`. No child key is read from `T`. This separation reflects the syntax tree: formulas recurse through immediate subformulas, whereas the very small term language is interpreted directly by its two code shapes. ```agda atomRel : Formula S (18 + m) → Formula S (12 + m) atomRel rel = bothAll i3 (extB i3 i11 (atomBody rel)) ``` The first four tags state four exact truth conditions. Once the tag slots have been calibrated by `Tags`, tag 0 is the membership atom: if `v` and `x` are the respective values of the first and second terms, it requires `v ∈ x`. Tag 1 is the equality atom and requires `v = x`. Tags 2 and 3 combine the same-arity child assertions `z ∈ ya` and `z ∈ yb` by conjunction and disjunction, respectively. Before that calibration, these are clauses selected by the corresponding tag slots, not claims that the slots already contain the standard numerals. ```agda relN : ℕ → Formula S (12 + m) relN 0 = atomRel (var i1 ∈̇ var i0) relN 1 = atomRel (var i1 ≐ var i0) relN 2 = binRel _∧̇_ relN 3 = binRel _∨̇_ ``` Tag 4 has the remaining binary polarity: `z ∈ ya` implies `z ∈ yb`, from the left child to the right child. Tag 5 gives falsity its empty extension. Tags 6 and 7 read one body at successor arity; tag 6 uses `∃[]-syntax` over `w`, while tag 7 uses `∀[]-syntax`. Tag 8 is the bounded universal. For every `v ∈ w`, `tmIs` is the antecedent that verifies `v` as a value of the bound term; for every `x ∈ w`, membership `x ∈ v` is then the antecedent to the propositionally truncated existence of an encoded extension in the body-value set. ```agda relN 4 = binRel _⇒̇_ relN 5 = botRel relN 6 = quRel ∃̇∈ relN 7 = quRel ∀̇∈ relN 8 = bqRel ∀̇∈ _⇒̇_ ``` Tag 9 has the existential polarity. Using `∃[]-syntax` with conjunction, it merely requires some `v ∈ w` validated by `tmIs`, some `x ∈ w` with `x ∈ v`, and a merely existing encoded extension in the body-value set. This completes the ten cases numbered 0 through 9. For natural numbers at least 10, `relN` returns truth, but this last equation contributes no case to the table specification: if `k : Fin 10`, then `toℕ k` is always between 0 and 9. ```agda relN 9 = bqRel ∃̇∈ _∧̇_ relN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) = ⊤̇ ``` We can now place a constructor relation into the common frame. The data to be connected are an environment-tower pair, a formula code of the same arity with a tagged payload, and a candidate entry of `T` at that code. The local relation module is reused so that every tag is judged with the same meanings of `T`, `w`, and the two term-code tags. ```agda module Clause {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) where private module R = Rel T w N ``` For a fixed `k`, the clause follows a precise chain. It considers every `q ∈ E` and every decomposition `q=(ar,F)`; every `c ∈ C` with `c=(ar,p)`; every decomposition `p=(N k,r)`; and every `e ∈ T` with `e=(c,yc)`. At each complete matching frame, `yc` must satisfy `relN (toℕ k)`. Every decomposition is guarded by a universal implication, so the clause does not assert that any of this frame data exists. It also treats `F` and `N k` only as supplied values, without identifying them with a genuine environment set or the numeral for `k`. ```agda clause : Fin 10 → Formula S m clause k = ∀̇∈ (var E) (bothAll i0 (∀̇∈ (var (sh 4 C)) (sndAll i0 i2 (sndAll i0 (sh 7 (N k)) (∀̇∈ (var (sh 9 T)) (sndAll i0 i5 (R.relN (toℕ k)))))))) ``` The two domain conditions supply the existence that the universal local clauses lack. `total` says that for every `c ∈ C`, there merely exists a `yc` with `(c,yc) ∈ T`; both the table member and its pair decomposition remain under propositional truncation. Conversely, `onC` says that every `e ∈ T` merely decomposes as `(c,yc)` with `c ∈ C`. Together they identify the first-projection domain of `T` with `C`, but they provide no choice function and do not make `T` single-valued. ```agda total onC : Formula S m total = ∀̇∈ (var C) (∃̇∈ (var (sh 1 T)) (sndEx i0 i1 ⊤̇)) onC = ∀̇∈ (var T) (bothEx i0 (var i1 ∈̇ var (sh 4 C))) ``` The ten local clauses are gathered by one finite conjunction. The argument `9` means that the indexing type is `Fin (suc 9)`, hence `Fin 10`; it does not omit a case. Ordinary conjunction and this finite conjunction introduce no new propositional truncation beyond any truncation already present inside the individual clauses. ```agda ten : Formula S m ten = bigAnd 9 clause ``` The formula `tableAt` now conjoins three demands: truncated totality over `C`, the restriction of every table member to a key in `C`, and all ten constructor clauses. This is a local bounded specification for a candidate relation. It does not prove that `C` is closed under child codes, that `E` is the intended environment tower, that the tags are standard, that values are unique, or that the candidate is a canonical satisfaction table. Later chapters separately supply the tower and code descriptions, tag calibration, semantic bridges, and pinning arguments needed to relate suitable candidates to canonical data. ```agda tableAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m tableAt T w C E N = Clause.total T w C E N ∧̇ (Clause.onC T w C E N ∧̇ Clause.ten T w C E N) ``` Finally, the structural checker yields a witness that `tableAt` is Δ₀. Every apparent search is bounded by `T`, `C`, `E`, `w`, a pair container, or a candidate value set, so no unbounded quantifier enters the describing formula. This conclusion classifies the syntax only: it proves neither that a suitable table exists nor that any candidate satisfies the clauses, and it establishes no semantic correctness, absoluteness, or completeness theorem. ```agda Δ₀-tableAt : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) → Δ₀ (tableAt T w C E N) Δ₀-tableAt T w C E N = checkΔ₀ (tableAt T w C E N) tt ``` ## Recap The formula `tableAt` is the conjunction of `total`, `onC`, and the ten local constructor clauses collected by `ten`. Here `total` gives only propositionally truncated existence of a table value for each code in `C`; `onC` restricts the first-projection domain to `C`; and the ten clauses impose universal local extension equations. The theorem `Δ₀-tableAt` certifies only that this description is syntactically bounded. Further arguments must still identify `E` as the intended environment tower, prove that `C` contains the required child codes, calibrate the tag slots through `Tags`, and establish the two-way semantic readings, pinning, and completeness needed for the canonical graph and the global predicate `satAt`. None of those results, and no table or globally chosen value, is constructed in this chapter.