Syntax as sets

Everything so far has kept formulas outside the sets they talk about: a formula is host-level data, a set is a point of the structure, and satisfaction is the bridge. Part 4 needs the other direction. To say inside a model that some set is definable, or to compare two formulas by an order that a model can see, the formulas themselves must be sets. This chapter injects them.

The encoding is deliberately dull. There is no arithmetization, no Gödel numbering, no recursion trick: a formula's code is a tagged pair, the tag being the constructor's index and the payload the codes of its parts. Recursion stays where it belongs, on the host's inductive Formula, and the code is a boundary format. The one elegance is that a set constant is already a set, so constants are their own codes.

What the chapter takes as parameters is exactly what the encoding needs: a pairing operation with injectivity, and an injection of the naturals. Nothing else about the structure matters, so the chapter is generic and the hierarchy instantiates it later.

A word on the deliverable that matters most. Alongside the code function there is an inductive relation Codes, "this set codes that formula", whose constructors carry sub-derivations at the sub-code positions. Reasoning about codes goes through that relation rather than through equations between code values, and the reason is practical: a code value is a deeply nested pair, and an equation between two of them forces a typechecker to unfold both. The relation makes the shape a constructor index instead, so matching is syntactic and the values are never normalized.

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

open import Base.Prelude
open import Base.Truth
open import FOL.ZFStructure using ( ZFStructure )

module FOL.Coding {ℓ} (𝒮 : ZFStructure (hPropAlgebra ℓ))
  (pr       : ZFStructure.S 𝒮 → ZFStructure.S 𝒮 → ZFStructure.S 𝒮)
  (pr-inj   : ∀ {a b c d} → pr a b ≡ pr c d → (a ≡ c) × (b ≡ d))
  (encℕ     : ℕ → ZFStructure.S 𝒮)
  (encℕ-inj : ∀ {j k} → encℕ j ≡ encℕ k → j ≡ k)
  where

open ZFStructure 𝒮 using ( S )
open import FOL.Syntax
  using ( Term; con; var; Formula
        ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

import Cubical.Data.Empty as Empty
open import Cubical.Data.Nat using ( znots; snotz )
open import Cubical.Data.FinData using ( toℕ; inj-toℕ )

Tagged pairs

The one construction: a constructor index paired with a payload. Injectivity comes straight from the two parameters, and the clash pattern packages the case that will recur whenever two different constructors are compared.

mkTag : ℕ → S → S
mkTag k x = pr (encℕ k) x

mkTag-inj : ∀ {j k x y} → mkTag j x ≡ mkTag k y → (j ≡ k) × (x ≡ y)
mkTag-inj p = encℕ-inj (pr-inj p .fst) , pr-inj p .snd

clash : ∀ {j k x y} {A : Type ℓ} → (j ≡ k → Empty.⊥) → mkTag j x ≡ mkTag k y → A
clash ne p = Empty.rec (ne (mkTag-inj p .fst))

Codes

Terms first, where the promised elegance appears: a set constant needs no encoding, since it is already a set, and only the variable index has to be injected. Terms are separated enough that their injectivity is immediate.

⌜_⌝ᵗ : ∀ {n} → Term S n → S
⌜ con x ⌝ᵗ = mkTag 0 x
⌜ var i ⌝ᵗ = mkTag 1 (encℕ (toℕ i))

⌜⌝ᵗ-inj : ∀ {n} (t u : Term S n) → ⌜ t ⌝ᵗ ≡ ⌜ u ⌝ᵗ → t ≡ u
⌜⌝ᵗ-inj (con x) (con y) p = cong con (mkTag-inj p .snd)
⌜⌝ᵗ-inj (con x) (var j) p = clash znots p
⌜⌝ᵗ-inj (var i) (con y) p = clash snotz p
⌜⌝ᵗ-inj (var i) (var j) p = cong var (inj-toℕ (encℕ-inj (mkTag-inj p .snd)))

Then formulas: twelve constructors, twelve tags. Binary constructors pair the two sub-codes, unary ones take the sub-code bare, and the two constants take a dummy payload since the tag already tells them apart.

⌜_⌝ : ∀ {n} → Formula S n → S
⌜ t ∈̇ u ⌝   = mkTag 0  (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ t ≐ u ⌝   = mkTag 1  (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ φ ∧̇ ψ ⌝   = mkTag 2  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ φ ∨̇ ψ ⌝   = mkTag 3  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ φ ⇒̇ ψ ⌝   = mkTag 4  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ ¬̇ φ ⌝     = mkTag 5  ⌜ φ ⌝
⌜ ⊤̇ ⌝       = mkTag 6  (encℕ 0)
⌜ ⊥̇ ⌝       = mkTag 7  (encℕ 0)
⌜ ∃̇ φ ⌝     = mkTag 8  ⌜ φ ⌝
⌜ ∀̇ φ ⌝     = mkTag 9  ⌜ φ ⌝
⌜ ∀̇∈ t φ ⌝  = mkTag 10 (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)
⌜ ∃̇∈ t φ ⌝  = mkTag 11 (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)

The coding relation

And the chapter's real interface. Codes s φ says the set s codes the formula φ, as an indexed inductive family whose constructors carry sub-derivations exactly where the code function makes recursive calls. It is the same information as the code function, presented so that a proof can match on the shape of the coding rather than compute with the code.

data CodesT {n : ℕ} : S → Term S n → Type ℓ where
  c-con : (x : S)     → CodesT (mkTag 0 x) (con x)
  c-var : (i : Fin n) → CodesT (mkTag 1 (encℕ (toℕ i))) (var i)

data Codes : {n : ℕ} → S → Formula S n → Type ℓ where
  c-∈  : ∀ {n s s'} {t u : Term S n}
       → CodesT s t → CodesT s' u → Codes (mkTag 0 (pr s s')) (t ∈̇ u)
  c-≐  : ∀ {n s s'} {t u : Term S n}
       → CodesT s t → CodesT s' u → Codes (mkTag 1 (pr s s')) (t ≐ u)
  c-∧  : ∀ {n s s'} {φ ψ : Formula S n}
       → Codes s φ → Codes s' ψ → Codes (mkTag 2 (pr s s')) (φ ∧̇ ψ)
  c-∨  : ∀ {n s s'} {φ ψ : Formula S n}
       → Codes s φ → Codes s' ψ → Codes (mkTag 3 (pr s s')) (φ ∨̇ ψ)
  c-⇒  : ∀ {n s s'} {φ ψ : Formula S n}
       → Codes s φ → Codes s' ψ → Codes (mkTag 4 (pr s s')) (φ ⇒̇ ψ)
  c-¬  : ∀ {n s} {φ : Formula S n}
       → Codes s φ → Codes (mkTag 5 s) (¬̇ φ)
  c-⊤  : ∀ {n} → Codes {n} (mkTag 6 (encℕ 0)) ⊤̇
  c-⊥  : ∀ {n} → Codes {n} (mkTag 7 (encℕ 0)) ⊥̇
  c-∃  : ∀ {n s} {φ : Formula S (suc n)}
       → Codes s φ → Codes (mkTag 8 s) (∃̇ φ)
  c-∀  : ∀ {n s} {φ : Formula S (suc n)}
       → Codes s φ → Codes (mkTag 9 s) (∀̇ φ)
  c-∀∈ : ∀ {n s s'} {t : Term S n} {φ : Formula S (suc n)}
       → CodesT s t → Codes s' φ → Codes (mkTag 10 (pr s s')) (∀̇∈ t φ)
  c-∃∈ : ∀ {n s s'} {t : Term S n} {φ : Formula S (suc n)}
       → CodesT s t → Codes s' φ → Codes (mkTag 11 (pr s s')) (∃̇∈ t φ)

Two facts tie the relation to the function. Every formula is coded by its own code, so the relation is inhabited wherever it should be; and any code for a formula is the code of that formula, so the relation adds nothing beyond the function. Both are one structural recursion, and the second is the one later chapters lean on: it converts a derivation, which is cheap to match on, into the equation, which is expensive to normalize, at exactly the point where the equation is finally needed.

codesT-complete : ∀ {n} (t : Term S n) → CodesT ⌜ t ⌝ᵗ t
codesT-complete (con x) = c-con x
codesT-complete (var i) = c-var i

codes-complete : ∀ {n} (φ : Formula S n) → Codes ⌜ φ ⌝ φ
codes-complete (t ∈̇ u)  = c-∈  (codesT-complete t) (codesT-complete u)
codes-complete (t ≐ u)  = c-≐  (codesT-complete t) (codesT-complete u)
codes-complete (φ ∧̇ ψ)  = c-∧  (codes-complete φ)  (codes-complete ψ)
codes-complete (φ ∨̇ ψ)  = c-∨  (codes-complete φ)  (codes-complete ψ)
codes-complete (φ ⇒̇ ψ)  = c-⇒  (codes-complete φ)  (codes-complete ψ)
codes-complete (¬̇ φ)    = c-¬  (codes-complete φ)
codes-complete ⊤̇        = c-⊤
codes-complete ⊥̇        = c-⊥
codes-complete (∃̇ φ)    = c-∃  (codes-complete φ)
codes-complete (∀̇ φ)    = c-∀  (codes-complete φ)
codes-complete (∀̇∈ t φ) = c-∀∈ (codesT-complete t) (codes-complete φ)
codes-complete (∃̇∈ t φ) = c-∃∈ (codesT-complete t) (codes-complete φ)

codesT-canon : ∀ {n s} {t : Term S n} → CodesT s t → s ≡ ⌜ t ⌝ᵗ
codesT-canon (c-con x) = refl
codesT-canon (c-var i) = refl

codes-canon : ∀ {n s} {φ : Formula S n} → Codes s φ → s ≡ ⌜ φ ⌝
codes-canon (c-∈ ct cu) =
  cong (mkTag 0)  (cong₂ pr (codesT-canon ct) (codesT-canon cu))
codes-canon (c-≐ ct cu) =
  cong (mkTag 1)  (cong₂ pr (codesT-canon ct) (codesT-canon cu))
codes-canon (c-∧ c d)   = cong (mkTag 2)  (cong₂ pr (codes-canon c) (codes-canon d))
codes-canon (c-∨ c d)   = cong (mkTag 3)  (cong₂ pr (codes-canon c) (codes-canon d))
codes-canon (c-⇒ c d)   = cong (mkTag 4)  (cong₂ pr (codes-canon c) (codes-canon d))
codes-canon (c-¬ c)     = cong (mkTag 5)  (codes-canon c)
codes-canon c-⊤         = refl
codes-canon c-⊥         = refl
codes-canon (c-∃ c)     = cong (mkTag 8)  (codes-canon c)
codes-canon (c-∀ c)     = cong (mkTag 9)  (codes-canon c)
codes-canon (c-∀∈ ct c) =
  cong (mkTag 10) (cong₂ pr (codesT-canon ct) (codes-canon c))
codes-canon (c-∃∈ ct c) =
  cong (mkTag 11) (cong₂ pr (codesT-canon ct) (codes-canon c))

Canonicity already gives what "the code determines the formula" is usually stated for: two derivations over the same code force the two formulas to have the same code, and an argument that recovers a formula from its code with a derivation in hand wants nothing further. That is most of them, and the relation above is the interface they were designed around.

It is not all of them. One consumer wants the equation itself, for a reason no relation answers, and the last section of this chapter proves it. The objection that once kept it out was a cost estimate, and the cost turned out not to be what the estimate assumed.

Recap

Formulas are now sets: ⌜_⌝ tags a constructor index onto the codes of the parts, constants coding themselves. The interface downstream is the relation

Codes, complete (codes-complete) and canonical (codes-canon), which keeps code values out of the equations a typechecker has to normalize. Everything is generic in the structure, needing only an injective pairing and an injection of the naturals; the hierarchy supplies both.

Codes determine formulas

Two formulas of the same arity with the same code are the same formula. The statement was dropped once, on the ground that its natural proof is a grid of twelve by twelve of which a hundred and thirty-two clauses carry no mathematics, and that the Codes relation was what every consumer had been designed around. A consumer arrived that wants the equation rather than the relation, and it wants it for a reason no relation answers: a recursion's table is a set, so if two occurrences of different subformulas shared a code the table would be genuinely multi-valued, and its existence, not merely its proof, would fail.

The grid does not have to be written. The constructor is recoverable from the tag, and the tag is a number, so what a formula's constructor is can be computed from it: one type family over the tag saying what having that tag looks like, one function producing it, and the tag equation the pairing's injectivity yields carries the second to the first. Twelve clauses each, and twelve more for the case analysis, in place of a hundred and forty-four.

That is the same move the constructibility chapter makes to match twelve constructors against eight demands, and it is worth saying once in general: when a case analysis is indexed by two things that a tag already relates, compute one side from the tag instead of matching both.

tagOf : ∀ {n} → Formula S n → ℕ
tagOf (t ∈̇ u)  = 0
tagOf (t ≐ u)  = 1
tagOf (a ∧̇ b)  = 2
tagOf (a ∨̇ b)  = 3
tagOf (a ⇒̇ b)  = 4
tagOf (¬̇ a)    = 5
tagOf ⊤̇        = 6
tagOf ⊥̇        = 7
tagOf (∃̇ a)    = 8
tagOf (∀̇ a)    = 9
tagOf (∀̇∈ t a) = 10
tagOf (∃̇∈ t a) = 11

payOf : ∀ {n} → Formula S n → S
payOf (t ∈̇ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (t ≐ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (a ∧̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (a ∨̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (a ⇒̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (¬̇ a)    = ⌜ a ⌝
payOf ⊤̇        = encℕ 0
payOf ⊥̇        = encℕ 0
payOf (∃̇ a)    = ⌜ a ⌝
payOf (∀̇ a)    = ⌜ a ⌝
payOf (∀̇∈ t a) = pr ⌜ t ⌝ᵗ ⌜ a ⌝
payOf (∃̇∈ t a) = pr ⌜ t ⌝ᵗ ⌜ a ⌝

shape : ∀ {n} (φ : Formula S n) → ⌜ φ ⌝ ≡ mkTag (tagOf φ) (payOf φ)
shape (t ∈̇ u)  = refl
shape (t ≐ u)  = refl
shape (a ∧̇ b)  = refl
shape (a ∨̇ b)  = refl
shape (a ⇒̇ b)  = refl
shape (¬̇ a)    = refl
shape ⊤̇        = refl
shape ⊥̇        = refl
shape (∃̇ a)    = refl
shape (∀̇ a)    = refl
shape (∀̇∈ t a) = refl
shape (∃̇∈ t a) = refl

Match : ∀ {n} → ℕ → Formula S n → Type ℓ
Match {n} 0  φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ∈̇ u)))
Match {n} 1  φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ≐ u)))
Match {n} 2  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∧̇ b)))
Match {n} 3  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∨̇ b)))
Match {n} 4  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ⇒̇ b)))
Match {n} 5  φ = Σ[ a ∈ Formula S n ] (φ ≡ (¬̇ a))
Match     6  φ = φ ≡ ⊤̇
Match     7  φ = φ ≡ ⊥̇
Match {n} 8  φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∃̇ a))
Match {n} 9  φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∀̇ a))
Match {n} 10 φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∀̇∈ t a))
Match {n} 11 φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∃̇∈ t a))
Match     _  _ = Empty.⊥*

matches : ∀ {n} (φ : Formula S n) → Match (tagOf φ) φ
matches (t ∈̇ u)  = t , (u , refl)
matches (t ≐ u)  = t , (u , refl)
matches (a ∧̇ b)  = a , (b , refl)
matches (a ∨̇ b)  = a , (b , refl)
matches (a ⇒̇ b)  = a , (b , refl)
matches (¬̇ a)    = a , refl
matches ⊤̇        = refl
matches ⊥̇        = refl
matches (∃̇ a)    = a , refl
matches (∀̇ a)    = a , refl
matches (∀̇∈ t a) = t , (a , refl)
matches (∃̇∈ t a) = t , (a , refl)

⌜⌝-inj : ∀ {n} (φ ψ : Formula S n) → ⌜ φ ⌝ ≡ ⌜ ψ ⌝ → φ ≡ ψ

private
  go : ∀ {n} (φ ψ : Formula S n) → Match (tagOf φ) ψ → payOf φ ≡ payOf ψ → φ ≡ ψ
  go (t ∈̇ u) ψ (t' , (u' , q)) p =
    cong₂ _∈̇_ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝ᵗ-inj u u' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (t ≐ u) ψ (t' , (u' , q)) p =
    cong₂ _≐_ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝ᵗ-inj u u' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ∧̇ b) ψ (a' , (b' , q)) p =
    cong₂ _∧̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ∨̇ b) ψ (a' , (b' , q)) p =
    cong₂ _∨̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ⇒̇ b) ψ (a' , (b' , q)) p =
    cong₂ _⇒̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (¬̇ a) ψ (a' , q) p = cong ¬̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go ⊤̇ ψ q p = sym q
  go ⊥̇ ψ q p = sym q
  go (∃̇ a) ψ (a' , q) p = cong ∃̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go (∀̇ a) ψ (a' , q) p = cong ∀̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go (∀̇∈ t a) ψ (t' , (a' , q)) p =
    cong₂ ∀̇∈ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
             (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (∃̇∈ t a) ψ (t' , (a' , q)) p =
    cong₂ ∃̇∈ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
             (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q

⌜⌝-inj φ ψ e = go φ ψ
  (subst (λ k → Match k ψ) (sym (tp .fst)) (matches ψ)) (tp .snd)
  where
  tp = mkTag-inj (sym (shape φ) ∙ e ∙ shape ψ)