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.

{-# 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.

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.

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.

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.

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.

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.

extB : ∀ {j} → Fin j → Fin j → Formula S ( + j) → Formula S j
extB y F φ = ∀̇∈ (var y) ((var i0 ∈̇ var (sh  F)) ∧̇ φ)
           ∧̇ ∀̇∈ (var F) (φ ⇒̇ (var i0 ∈̇ var (sh  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.

fstAll : ∀ {j} → Fin j → Fin j → Formula S ( + j) → Formula S j
fstAll x v body = ∀̇∈ (var x) (∀̇∈ (var i0) (prAtL (sh  x) i0 (sh  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.

subAt : ∀ {j} → Fin j → Fin j → Fin j → Formula S ( + j) → Formula S j
subAt T ar a body = ∀̇∈ (var T) (bothAll i0 (prAtL i1 (sh  ar) (sh  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.

subSucAt : ∀ {j} → Fin j → Fin j → Fin j → Formula S ( + j) → Formula S j
subSucAt T ar a body =
  ∀̇∈ (var T) (bothAll i0 (fstAll i1 (sh  a) (sucAtL (sh  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.

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  z)) (prAtL i0 i1 (sh  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.

module Rel {m : ℕ} (T w : Fin m) (N : Fin  → 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.

  binBody : (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S ( + 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.

  quBody : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → Formula S ( + m)
  quBody q = q (var (sh  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.

  bqBody : (∀ {j} → Term S j → Formula S (suc j) → Formula S j)
         → (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S ( + m)
  bqBody q c =
    q (var (sh  w)) (c (tmIs i9 i1 i0 N0 N1)
      (q (var (sh  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.

  atomBody : Formula S ( + m) → Formula S ( + m)
  atomBody rel =
    ∃̇∈ (var (sh  w)) (∃̇∈ (var (sh  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.

  botRel : Formula S ( + 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.

  binRel : (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S ( + m)
  binRel op =
    bothAll i3 (subAt (sh  T) i12 i1 (subAt (sh  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.

  quRel : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → Formula S ( + m)
  quRel q = subSucAt (sh  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.

  bqRel : (∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S ( + m)
  bqRel q c = bothAll i3 (subSucAt (sh  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.

  atomRel : Formula S ( + m) → Formula S ( + 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.

  relN : ℕ → Formula S ( + m)
  relN  = atomRel (var i1 ∈̇ var i0)
  relN  = atomRel (var i1 ≐ var i0)
  relN  = binRel _∧̇_
  relN  = 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.

  relN  = binRel _⇒̇_
  relN  = botRel
  relN  = quRel ∃̇∈
  relN  = quRel ∀̇∈
  relN  = 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.

  relN  = 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.

module Clause {m : ℕ} (T w C E : Fin m) (N : Fin  → 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.

  clause : Fin  → Formula S m
  clause k =
    ∀̇∈ (var E) (bothAll i0 (∀̇∈ (var (sh  C)) (sndAll i0 i2 (sndAll i0 (sh  (N k))
      (∀̇∈ (var (sh  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.

  total onC : Formula S m
  total = ∀̇∈ (var C) (∃̇∈ (var (sh  T)) (sndEx i0 i1 ⊤̇))
  onC = ∀̇∈ (var T) (bothEx i0 (var i1 ∈̇ var (sh  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.

  ten : Formula S m
  ten = bigAnd  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.

tableAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → 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.

Δ₀-tableAt : ∀ {m} (T w C E : Fin m) (N : Fin  → 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.