Satisfaction tables over subformulas

Read this chapter directly, or use the reading guide and dependency map to choose another route.

Reading guide · Dependency map

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.

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

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.

  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.

  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.

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)