Reading codes from inside

Codes are sets now, but a certificate living inside the model cannot use that directly: it can only say things in the object language, and what it needs to say is "this set is the code of a formula with such and such a shape". So the shapes have to be spelled out as formulas, and this chapter spells them out.

Two things are needed, and the chapter provides both because a certificate needs them together. First a set of codes to quantify over: all codes of parameter-free formulas, at every arity, gathered into one set. Its index is small, so the gathering is legitimate, and because every arity is included the subformula of a quantifier does not escape it, which is what later certificates rely on when they descend into a formula.

Second, the readers: object formulas saying "this set is the singleton of that", "this is the unordered pair", "this is the Kuratowski pair", "this is tagged with such a number". Each is a bounded formula, so each is Δ₀, and each comes with an adequacy lemma turning satisfaction into the set-theoretic fact. The readers take their de Bruijn positions as arguments, so the same formula serves at any depth of nesting.

The discipline throughout: nothing ever compares two code values. Membership is transported along paths through the library's classification lemmas, and the shape of a code is carried by the coding relation of Part 1. Comparing code values directly is what makes these proofs stop terminating, and the previous chapters were arranged specifically so that it never has to happen.

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

open import Base.Prelude
open import Base.Truth

module L.Coding.Base {ℓ : Level} where

open import FOL.Syntax
  using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-∀∈; δ-∃∈ )
open import FOL.Manipulation.Relabelling using ( embed )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; module VCode )

import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; _⊆_; extensionality )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s; SingletonPackage; module InfinitySet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)
open InfinitySet using ( #_ )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
module Sem = FOL.Semantics (hPropAlgebra (ℓ-suc ℓ)) 𝒮ᵥ
open Sem using ( _^_ )
open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ )

The set of all codes

Parameter-free formulas at every arity, indexed by the arity together with the formula. That index is an ordinary inductive type at the small level, so it is a legitimate index for a set of the hierarchy, and the set is the image of the code function along it. Membership is definitional, and every parameter-free formula's code is a member by construction. Being independent of any parameter, the set can be named by a constant of the object language, which is what lets a certificate quantify over codes at all.

ClosedΣ : Type ℓ
ClosedΣ = Σ[ n ∈ ℕ ] Formula (⊥* {ℓ}) n

allCodes : V ℓ
allCodes = sett ClosedΣ (λ p → VCode.⌜ embed (p .snd) ⌝)

allCodes-spec : (s : V ℓ)
  → ⟨ s ∈ allCodes ⟩ ≡ ∥ Σ[ p ∈ ClosedΣ ] (VCode.⌜ embed (p .snd) ⌝ ≡ s) ∥₁
allCodes-spec s = refl

code∈allCodes : ∀ {n} (φ : Formula (⊥* {ℓ}) n) → ⟨ VCode.⌜ embed φ ⌝ ∈ allCodes ⟩
code∈allCodes {n} φ = ∣ (n , φ) , refl ∣₁

allCodesTerm : ∀ {n} → Term (V ℓ) n
allCodesTerm = con allCodes

allCodesTerm-eval : ∀ {n} (γ : (V ℓ) ^ n) → ⟦ allCodesTerm {n} ⟧ γ ≡ allCodes
allCodesTerm-eval γ = refl

Singletons and pairs, characterized

The library's classification specifications, named so the proofs below read as membership reasoning. Then the two characterizations: a set whose only member is u is the singleton of u, and a set whose members are exactly u and v is their unordered pair. Both are one application of extensionality, and both are the meta-level content the readers will express.

∈sgl-elim : {u y : V ℓ} → ⟨ y ∈ ⁅ u ⁆s ⟩ → y ≡ u
∈sgl-elim {u} {y} h =
    SetPackage.classification (SingletonPackage u) y .fst (∈∈ₛ {a = y} {b = ⁅ u ⁆s} .fst h)

∈sgl-intro : {u y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u ⁆s ⟩
∈sgl-intro {u} {y} e = ∈∈ₛ {a = y} {b = ⁅ u ⁆s} .snd
    (SetPackage.classification (SingletonPackage u) y .snd e)

∈pair-elim : {u v y : V ℓ} → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁
∈pair-elim {u} {v} {y} h = pairing-ax u v y .fst (∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .fst h)

∈pair-introL : {u v y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u , v ⁆ ⟩
∈pair-introL {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd
    (pairing-ax u v y .snd ∣ inl e ∣₁)

∈pair-introR : {u v y : V ℓ} → y ≡ v → ⟨ y ∈ ⁅ u , v ⁆ ⟩
∈pair-introR {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd
    (pairing-ax u v y .snd ∣ inr e ∣₁)

sgl-char : (x u : V ℓ) → ⟨ u ∈ x ⟩ → ((y : V ℓ) → ⟨ y ∈ x ⟩ → y ≡ u) → x ≡ ⁅ u ⁆s
sgl-char x u hu hall = extensionality x ⁅ u ⁆s (sub₁ , sub₂)
  where
  sub₁ : ⟨ x ⊆ ⁅ u ⁆s ⟩
  sub₁ y y∈ₛx = ∈∈ₛ {a = y} {b = ⁅ u ⁆s} .fst
    (∈sgl-intro (hall y (∈∈ₛ {a = y} {b = x} .snd y∈ₛx)))
  sub₂ : ⟨ ⁅ u ⁆s ⊆ x ⟩
  sub₂ y y∈ₛs = subst (λ z → ⟨ z ∈ₛ x ⟩)
    (sym (∈sgl-elim (∈∈ₛ {a = y} {b = ⁅ u ⁆s} .snd y∈ₛs)))
    (∈∈ₛ {a = u} {b = x} .fst hu)

pair-char : (x u v : V ℓ) → ⟨ u ∈ x ⟩ → ⟨ v ∈ x ⟩
          → ((y : V ℓ) → ⟨ y ∈ x ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁)
          → x ≡ ⁅ u , v ⁆
pair-char x u v hu hv hall = extensionality x ⁅ u , v ⁆ (sub₁ , sub₂)
  where
  sub₁ : ⟨ x ⊆ ⁅ u , v ⁆ ⟩
  sub₁ y y∈ₛx = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .fst
    (PT.rec ((y ∈ ⁅ u , v ⁆) .snd)
      (Sum.rec (λ e → ∈pair-introL {u = u} {v = v} e)
               (λ e → ∈pair-introR {u = u} {v = v} e))
      (hall y (∈∈ₛ {a = y} {b = x} .snd y∈ₛx)))
  sub₂ : ⟨ ⁅ u , v ⁆ ⊆ x ⟩
  sub₂ y y∈ₛp = PT.rec ((y ∈ₛ x) .snd)
    (Sum.rec (λ e → subst (λ z → ⟨ z ∈ₛ x ⟩) (sym e) (∈∈ₛ {a = u} {b = x} .fst hu))
             (λ e → subst (λ z → ⟨ z ∈ₛ x ⟩) (sym e) (∈∈ₛ {a = v} {b = x} .fst hv)))
    (∈pair-elim (∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd y∈ₛp))

The Kuratowski pair, at the meta level

Before writing the reader, the fact it will express: a set is the Kuratowski pair of U and W exactly when it has a member that is the singleton of U, a member that is the unordered pair, and no other members. The two auxiliary predicates are written in the shape the reader's satisfaction will unfold to, so that the adequacy lemmas afterwards are one line each rather than a second proof.

private
  SglOf : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  SglOf U w = ⟨ U ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → z ≡ U)

  PairOf : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PairOf U W w =
    ⟨ U ∈ w ⟩ × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ (z ≡ U) ⊎ (z ≡ W) ∥₁))

  sglOf→≡ : {U w : V ℓ} → SglOf U w → w ≡ ⁅ U ⁆s
  sglOf→≡ {U} {w} (hu , hall) = sgl-char w U hu hall

  pairOf→≡ : {U W w : V ℓ} → PairOf U W w → w ≡ ⁅ U , W ⁆
  pairOf→≡ {U} {W} {w} (hu , hv , hall) = pair-char w U W hu hv hall

  sglOf⁅⁆ : (U : V ℓ) → SglOf U ⁅ U ⁆s
  sglOf⁅⁆ U = ∈sgl-intro refl , (λ z z∈ → ∈sgl-elim z∈)

  pairOf⁅⁆ : (U W : V ℓ) → PairOf U W ⁅ U , W ⁆
  pairOf⁅⁆ U W = ∈pair-introL refl , ∈pair-introR refl , (λ z z∈ → ∈pair-elim z∈)

  sglOf-subst : {U w : V ℓ} → w ≡ ⁅ U ⁆s → SglOf U w
  sglOf-subst {U} e = subst (SglOf U) (sym e) (sglOf⁅⁆ U)

  pairOf-subst : {U W w : V ℓ} → w ≡ ⁅ U , W ⁆ → PairOf U W w
  pairOf-subst {U} {W} e = subst (PairOf U W) (sym e) (pairOf⁅⁆ U W)

prChar-fwd : (Q U W : V ℓ)
  → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁
  → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁
  → ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁)
  → Q ≡ pr U W
prChar-fwd Q U W h₁ h₂ h₃ = extensionality Q (pr U W) (sub₁ , sub₂)
  where
  sub₁ : ⟨ Q ⊆ pr U W ⟩
  sub₁ y y∈ₛQ = PT.rec ((y ∈ₛ pr U W) .snd)
    (Sum.rec
      (λ s → ∈∈ₛ {a = y} {b = pr U W} .fst
        (∈pair-introL {u = ⁅ U ⁆s} {v = ⁅ U , W ⁆} (sglOf→≡ s)))
      (λ p → ∈∈ₛ {a = y} {b = pr U W} .fst
        (∈pair-introR {u = ⁅ U ⁆s} {v = ⁅ U , W ⁆} (pairOf→≡ p))))
    (h₃ y (∈∈ₛ {a = y} {b = Q} .snd y∈ₛQ))
  sub₂ : ⟨ pr U W ⊆ Q ⟩
  sub₂ y y∈ₛpr = PT.rec ((y ∈ₛ Q) .snd)
    (Sum.rec
      (λ e → PT.rec ((y ∈ₛ Q) .snd)
        (λ { (w , w∈Q , s) → subst (λ z → ⟨ z ∈ₛ Q ⟩) (sym (e ∙ sym (sglOf→≡ s)))
               (∈∈ₛ {a = w} {b = Q} .fst w∈Q) })
        h₁)
      (λ e → PT.rec ((y ∈ₛ Q) .snd)
        (λ { (w , w∈Q , p) → subst (λ z → ⟨ z ∈ₛ Q ⟩) (sym (e ∙ sym (pairOf→≡ p)))
               (∈∈ₛ {a = w} {b = Q} .fst w∈Q) })
        h₂))
    (∈pair-elim (∈∈ₛ {a = y} {b = pr U W} .snd y∈ₛpr))

prChar-bwd : (Q U W : V ℓ) → Q ≡ pr U W
  → (∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁)
  × ((∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁)
  × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁))
prChar-bwd Q U W e = h₁ , h₂ , h₃
  where
  inQ : {z : V ℓ} → ⟨ z ∈ pr U W ⟩ → ⟨ z ∈ Q ⟩
  inQ {z} h = subst (λ w → ⟨ z ∈ w ⟩) (sym e) h
  h₁ : ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁
  h₁ = ∣ ⁅ U ⁆s , (inQ (∈pair-introL refl) , sglOf⁅⁆ U) ∣₁
  h₂ : ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁
  h₂ = ∣ ⁅ U , W ⁆ , (inQ (∈pair-introR refl) , pairOf⁅⁆ U W) ∣₁
  h₃ : (y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁
  h₃ y y∈Q = PT.map (Sum.rec (λ q → inl (sglOf-subst q)) (λ q → inr (pairOf-subst q)))
    (∈pair-elim (subst (λ w → ⟨ y ∈ w ⟩) e y∈Q))

The readers

Now the object formulas. Each takes the de Bruijn positions it speaks about, and the bookkeeping is the usual one: a bounded quantifier binds a fresh variable at position zero and pushes the others outward, so a position mentioned under one binder appears as its successor. A constant needs no such shift, which is the small dividend that makes the tagged versions simpler than the plain ones.

Every clause is a bounded quantifier or an atom, so every reader is Δ₀ and its witness is read straight off its shape.

sglAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n
sglAt k i = (var i ∈̇ var k) ∧̇ (∀̇∈ (var k) (var zero ≐ var (suc i)))

sglConAt : ∀ {n} → Fin n → V ℓ → Formula (V ℓ) n
sglConAt k c = (con c ∈̇ var k) ∧̇ (∀̇∈ (var k) (var zero ≐ con c))

pairAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n
pairAt k i j = (var i ∈̇ var k) ∧̇ ((var j ∈̇ var k)
            ∧̇ (∀̇∈ (var k) ((var zero ≐ var (suc i)) ∨̇ (var zero ≐ var (suc j)))))

pairConAt : ∀ {n} → Fin n → V ℓ → Fin n → Formula (V ℓ) n
pairConAt k c j = (con c ∈̇ var k) ∧̇ ((var j ∈̇ var k)
               ∧̇ (∀̇∈ (var k) ((var zero ≐ con c) ∨̇ (var zero ≐ var (suc j)))))

Δ₀-sglAt : ∀ {n} (k i : Fin n) → Δ₀ (sglAt k i)
Δ₀-sglAt k i = δ-∧ δ-∈ (δ-∀∈ δ-≐)

Δ₀-sglConAt : ∀ {n} (k : Fin n) (c : V ℓ) → Δ₀ (sglConAt k c)
Δ₀-sglConAt k c = δ-∧ δ-∈ (δ-∀∈ δ-≐)

Δ₀-pairAt : ∀ {n} (k i j : Fin n) → Δ₀ (pairAt k i j)
Δ₀-pairAt k i j = δ-∧ δ-∈ (δ-∧ δ-∈ (δ-∀∈ (δ-∨ δ-≐ δ-≐)))

Δ₀-pairConAt : ∀ {n} (k : Fin n) (c : V ℓ) (j : Fin n) → Δ₀ (pairConAt k c j)
Δ₀-pairConAt k c j = δ-∧ δ-∈ (δ-∧ δ-∈ (δ-∀∈ (δ-∨ δ-≐ δ-≐)))

The two assembled readers, each three clauses: some member is the singleton, some member is the pair, and every member is one of the two. The tagged version is the same with the first component a constant numeral, which is how a constructor index is read.

prAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n
prAt q u v = (∃̇∈ (var q) (sglAt zero (suc u)))
          ∧̇ ((∃̇∈ (var q) (pairAt zero (suc u) (suc v)))
          ∧̇ (∀̇∈ (var q) (sglAt zero (suc u) ∨̇ pairAt zero (suc u) (suc v))))

tagAt : ∀ {n} → Fin n → ℕ → Fin n → Formula (V ℓ) n
tagAt s k x = (∃̇∈ (var s) (sglConAt zero (# k)))
           ∧̇ ((∃̇∈ (var s) (pairConAt zero (# k) (suc x)))
           ∧̇ (∀̇∈ (var s) (sglConAt zero (# k) ∨̇ pairConAt zero (# k) (suc x))))

Δ₀-prAt : ∀ {n} (q u v : Fin n) → Δ₀ (prAt q u v)
Δ₀-prAt q u v = δ-∧ (δ-∃∈ (Δ₀-sglAt zero (suc u)))
  (δ-∧ (δ-∃∈ (Δ₀-pairAt zero (suc u) (suc v)))
       (δ-∀∈ (δ-∨ (Δ₀-sglAt zero (suc u)) (Δ₀-pairAt zero (suc u) (suc v)))))

Δ₀-tagAt : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) → Δ₀ (tagAt s k x)
Δ₀-tagAt s k x = δ-∧ (δ-∃∈ (Δ₀-sglConAt zero (# k)))
  (δ-∧ (δ-∃∈ (Δ₀-pairConAt zero (# k) (suc x)))
       (δ-∀∈ (δ-∨ (Δ₀-sglConAt zero (# k)) (Δ₀-pairConAt zero (# k) (suc x)))))

Adequacy

And the payoff. Unfolding what it means to satisfy prAt gives, clause for clause, the hypotheses of the meta-level characterization: the truth algebra's conjunction is a product, its bounded existential a truncated sum, its equality a path. So each direction is the corresponding half of that characterization, and the lemma is one line. This is why the auxiliary predicates above were written in that particular shape.

prAt-adequate : ∀ {n} (q u v : Fin n) (γ : (V ℓ) ^ n)
              → (γ ⊨ prAt q u v) ≡ ((⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ))
                                   , setIsSet _ _)
prAt-adequate q u v γ = ⇔toPath
  (λ { (h₁ , h₂ , h₃) → prChar-fwd _ _ _ h₁ h₂ h₃ })
  (λ e → prChar-bwd _ _ _ e)

tagAt-adequate : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) (γ : (V ℓ) ^ n)
               → (γ ⊨ tagAt s k x) ≡ ((⟦ var s ⟧ γ ≡ pr (# k) (⟦ var x ⟧ γ))
                                     , setIsSet _ _)
tagAt-adequate s k x γ = ⇔toPath
  (λ { (h₁ , h₂ , h₃) → prChar-fwd _ _ _ h₁ h₂ h₃ })
  (λ e → prChar-bwd _ _ _ e)

Recap

allCodes gathers the codes of all parameter-free formulas at all arities into one nameable set, and prAt and tagAt read a Kuratowski pair and a tag from inside the object language, both Δ₀ and both adequate. Everything a certificate needs in order to destructure a code is now available in bounded form, with no recursion and no comparison of code values. The chapters that follow build certificates on top of these.