---
title: "Satisfaction tables over subformulas"
module: L.Coding.SatisfactionTable
lang: en
site: "Bedrock"
description: "Satisfaction tables over subformulas"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 51
canonical: https://bedrock.institute/en/L.Coding.SatisfactionTable.html
html: L.Coding.SatisfactionTable.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionTable.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Coding, L.Constructible, L.Axioms.Numerals, L.Coding.Model, L.Coding.CodeConstructibility, L.Coding.Satisfaction]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.SatisfactionTable.md, https://bedrock.institute/ja/L.Coding.SatisfactionTable.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Satisfaction tables over subformulas

For a formula `φ`, this chapter builds `satTable φ`, whose entries pair each subformula key with its recursively defined satisfaction value, and proves that a key determines the value recorded beside it.

The recursion's answer, assembled. For a formula of the meta-language, the finite
set of pairs of a key with the value at it, one pair for the formula and one for
each subformula, built exactly as the subformula closure was and for the same
reason: the meta level can name what it has already built.

Everything here is an element of the model by construction. The key is a pair of
a numeral with a code, and the code is taken in the model's own coding, so no
constructibility certificate is carried and none has to be proved. That is what
the coding chapter's second instantiation bought, and this is the chapter that
spends it.

What the recursion actually needs from the table is the other direction: any
value recorded against a key is *the* value at that key. That is where the code
equation has to be injective, and where a table that merely happened to record
two things at one key would not be a function at all.

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

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

module L.Coding.SatisfactionTable {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Coding.Model {ℓ} using ( module LCode; prʟ; prʟ-fst )
open import L.Coding.CodeConstructibility {ℓ}
  using ( tree; Of; tree-inv )
  renaming ( module Parts to TreeParts )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.Prelude using ( J )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_ )

open hPropStructure 𝒮ʟ using ( S )
```

## Keys and entries

`keyʟ φ` pairs the arity of `φ` with its code, and `ent φ` pairs that key with `Sat B φ`. Applying the same subformula-tree construction to entries and keys yields `satTable φ` and its indexing `slot φ`.

A key is the arity paired with the code, which is the shape every clause of the
internal recursion reads. An entry is a key paired with the value.

The shape both live in is the same, so it is written once and written
elsewhere. `tree` is the closure chapter's recursion: it gathers one
thing per subformula, and what that thing is is its parameter. With the entry it
gives the table, with the key it gives the **slot** the table is indexed by. The
recursion needs both and needs them to agree constructor for constructor, which
is why they come from one recursion rather than two.

```agda
keyʟ : ∀ {n} → Formula S n → S
keyʟ {n} φ = prʟ (numeralL n) LCode.⌜ φ ⌝

module _ (B : S) where
  ent : ∀ {n} → Formula S n → S
  ent φ = prʟ (keyʟ φ) (Sat B φ)

  satTable : ∀ {n} → Formula S n → S
  satTable = tree ent

  slot : ∀ {n} → Formula S n → S
  slot = tree keyʟ
```

## Inverting tables and slots

The four inversion lemmas instantiate `tree-inv`: membership in a satisfaction table or slot identifies the subformula that contributed the member, while `slot-ent` and `ent-slot` move between an entry and its key.

Every member is one of the things gathered. That is the inversion the closure
chapter proves, stated there against two collections at once, so the four
readings below are four instantiations of it and no induction runs here.

```agda
  module Parts (f : ∀ {m} → Formula S m → S) where
    open TreeParts f public

  satTable-inv : ∀ {n} (φ : Formula S n) (x : V ℓ)
               → ⟨ x ∈ fst (satTable φ) ⟩ → Of ent ent φ x
  satTable-inv = tree-inv ent ent

  slot-inv : ∀ {n} (φ : Formula S n) (x : V ℓ)
           → ⟨ x ∈ fst (slot φ) ⟩ → Of keyʟ keyʟ φ x
  slot-inv = tree-inv keyʟ keyʟ

  slot-ent : ∀ {n} (φ : Formula S n) (x : V ℓ)
           → ⟨ x ∈ fst (slot φ) ⟩ → Of keyʟ ent φ x
  slot-ent = tree-inv keyʟ ent

  ent-slot : ∀ {n} (φ : Formula S n) (x : V ℓ)
           → ⟨ x ∈ fst (satTable φ) ⟩ → Of ent keyʟ φ x
  ent-slot = tree-inv ent keyʟ
```

## Uniqueness of the value at a key

If two table entries have the same arity-code key, injectivity of pairing and of formula coding identifies their formulas. The lemma `key-determines` therefore proves that both entries carry the same satisfaction value.

Two formulas with the same key have the same value, and that is where the code
equation's injectivity is used. The arities come out equal from the numeral
half of the key, and the code equation from the other half; the first is then
eliminated by path induction so that the second can be used at a single arity,
which is the only arity at which it is true.

```agda
  private
    same : ∀ {n} (ψ χ : Formula S n)
         → fst LCode.⌜ ψ ⌝ ≡ fst LCode.⌜ χ ⌝ → Sat B ψ ≡ Sat B χ
    same ψ χ e =
      cong (Sat B) (LCode.⌜⌝-inj ψ χ (Σ≡Prop (λ v → snd (isL v)) e))

    cross : ∀ {n m} (ψ : Formula S n) (χ : Formula S m) → n ≡ m
          → fst LCode.⌜ ψ ⌝ ≡ fst LCode.⌜ χ ⌝ → Sat B ψ ≡ Sat B χ
    cross {n} ψ χ p = J
      (λ m' p' → (χ' : Formula S m')
               → fst LCode.⌜ ψ ⌝ ≡ fst LCode.⌜ χ' ⌝ → Sat B ψ ≡ Sat B χ')
      (same ψ) p χ

  total : ∀ {n} (φ : Formula S n) (x : V ℓ) → ⟨ x ∈ fst (slot φ) ⟩
        → ∥ (Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ fst (satTable φ) ⟩) ∥₁
  total φ x h = PT.map
    (λ { (m , χ , (q , incl)) → Sat B χ
       , subst (λ w → ⟨ pr w (fst (Sat B χ)) ∈ fst (satTable φ) ⟩) (sym q)
           (incl (pr (fst (keyʟ χ)) (fst (Sat B χ)))
             (subst (λ w → ⟨ w ∈ fst (tree ent χ) ⟩)
               (prʟ-fst (keyʟ χ) (Sat B χ)) (Parts.self ent χ))) })
    (slot-ent φ x h)

  inSlot : ∀ {n} (φ : Formula S n) (x y : V ℓ)
         → ⟨ pr x y ∈ fst (satTable φ) ⟩ → ⟨ x ∈ fst (slot φ) ⟩
  inSlot φ x y h = PT.rec (snd (x ∈ fst (slot φ)))
    (λ { (m , χ , (q , incl)) →
      subst (λ w → ⟨ w ∈ fst (slot φ) ⟩)
        (sym (pr-inj (q ∙ prʟ-fst (keyʟ χ) (Sat B χ)) .fst))
        (incl (fst (keyʟ χ)) (Parts.self keyʟ χ)) })
    (ent-slot φ (pr x y) h)

  key-determines : ∀ {n m} (ψ : Formula S n) (χ : Formula S m)
                 → fst (keyʟ ψ) ≡ fst (keyʟ χ) → Sat B ψ ≡ Sat B χ
  key-determines {n} {m} ψ χ e = cross ψ χ
    (#-inj′ (sym (numeralL-fst n) ∙ pr-inj q .fst ∙ numeralL-fst m))
    (pr-inj q .snd)
    where
    q : pr (fst (numeralL n)) (fst LCode.⌜ ψ ⌝)
      ≡ pr (fst (numeralL m)) (fst LCode.⌜ χ ⌝)
    q = sym (prʟ-fst (numeralL n) LCode.⌜ ψ ⌝)
      ∙ e ∙ prʟ-fst (numeralL m) LCode.⌜ χ ⌝

  entry-out : ∀ {n m} (φ : Formula S n) (ψ : Formula S m) (y : V ℓ)
            → ⟨ pr (fst (keyʟ ψ)) y ∈ fst (satTable φ) ⟩
            → y ≡ fst (Sat B ψ)
  entry-out φ ψ y h = PT.rec (setIsSet y (fst (Sat B ψ)))
    (λ { (m , χ , (q , _)) →
      let r = pr-inj (q ∙ prʟ-fst (keyʟ χ) (Sat B χ)) in
      r .snd ∙ cong fst (sym (key-determines ψ χ (r .fst))) })
    (satTable-inv φ (pr (fst (keyʟ ψ)) y) h)

  entry-in : ∀ {n} (φ : Formula S n)
           → ⟨ pr (fst (keyʟ φ)) (fst (Sat B φ)) ∈ fst (satTable φ) ⟩
  entry-in φ = subst (λ w → ⟨ w ∈ fst (satTable φ) ⟩)
    (prʟ-fst (keyʟ φ) (Sat B φ)) (Parts.self ent φ)
```

## Subkeys determined by a constructor tag

For a key whose formula code has a specified constructor tag, the final case analysis identifies the immediate subformula keys in its slot. Binary, unary, and quantifier constructors each return the arity-adjusted keys required by the recursion clauses.

The dispatch a clause performs, and the last piece before the ten
verifications. A clause is stated at a tag and receives a key of that shape; the
formula the key names is recovered by the inversion above, and then its
constructor has to be matched against the tag. That match is the coding chapter's
own device, exported rather than rebuilt: the constructor is recoverable from the
tag, so the shape of a formula of a given tag is **computed** from the tag,
and the tag equation carries the formula's own case to it.

So one lemma serves all ten clauses, and it returns three things: what the
formula's constructor is, that the arity read is the formula's, and that the
payload read is the formula's.

```agda
keyʟ-shape : ∀ {m} (ψ : Formula S m) (k : ℕ) (ar p : V ℓ)
           → fst (keyʟ ψ) ≡ pr ar (pr (# k) p)
           → LCode.Match k ψ
           × ((# m ≡ ar) × (fst (LCode.payOf ψ) ≡ p))
keyʟ-shape {m} ψ k ar p e =
    subst (λ j → LCode.Match j ψ) tag≡ (LCode.matches ψ)
  , ( sym (numeralL-fst m) ∙ pr-inj e' .fst
    , pr-inj inner .snd )
  where
  e' : pr (fst (numeralL m)) (fst LCode.⌜ ψ ⌝) ≡ pr ar (pr (# k) p)
  e' = sym (prʟ-fst (numeralL m) LCode.⌜ ψ ⌝) ∙ e

  inner : pr (fst (numeralL (LCode.tagOf ψ))) (fst (LCode.payOf ψ))
        ≡ pr (# k) p
  inner = sym (prʟ-fst (numeralL (LCode.tagOf ψ)) (LCode.payOf ψ))
        ∙ sym (cong fst (LCode.shape ψ))
        ∙ pr-inj e' .snd

  tag≡ : LCode.tagOf ψ ≡ k
  tag≡ = #-inj′ (sym (numeralL-fst (LCode.tagOf ψ)) ∙ pr-inj inner .fst)
```