Syntax as sets

A model can quantify only over elements of its carrier, whereas terms and formulas initially live in the surrounding type theory. To make syntax available inside the model, this chapter assigns each term and formula an element of the carrier. A code is a tagged pair: the numeric tag identifies the outer constructor, and the payload contains the codes of its immediate parts. Set constants can appear directly as payloads because they already belong to the carrier.

The construction assumes an injective pairing operation and an injective map from natural numbers. These hypotheses make both components recoverable from a tagged pair. The chapter first proves that term codes are injective, then defines formula codes for all ten constructors. It also gives the constant and membership cases of relational coding through CodesT and Codes. Finally, a tag-indexed description of constructor shapes supports the proof that equal codes determine equal formulas of the same arity.

To encode syntax as sets, two operations on the carrier would suffice on their own, but injectivity is what makes decoding possible: if two pieces of syntax received the same set, the coding could not be inverted. This chapter therefore works over a structure 𝒮 of type ZFStructure, whose equality and membership take values in hProp ℓ, and takes the encoding data as explicit module parameters. Every definition below is stated for an arbitrary structure with such data; the cumulative hierarchy will supply an instance in a later chapter.

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

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

module FOL.Coding {ℓ} (𝒮 : ZFStructure ℓ)

The two pieces of data are an injective pairing and an injective numeral map. pr takes two elements of the carrier S to their pair, and pr-inj says the pairing can be taken apart again: an equality pr a b ≡ pr c d returns both a ≡ c and b ≡ d as a pair of paths. encℕ sends each natural number to an element of S, and encℕ-inj says distinct numbers land at distinct elements. These are exactly the hypotheses the tagged-pair construction will consume; nothing else about 𝒮 enters the chapter.

  (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

The objects being coded come from the syntax layer: the inductive types Term and Formula, built from two term constructors (con for a set constant, var for a variable) and ten formula constructors, from the atoms _∈̇_ and _≐_ through the connectives and the bounded and unbounded quantifiers. From the structure itself, only the carrier S is used, since coding attaches no set-theoretic operation to syntax. The empty type appears only as the codomain of impossible equations, in proofs that certain codes cannot coincide.

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

import Cubical.Data.Empty as Empty

Two small arithmetic facts support the injectivity proofs. First, structurally distinct numerals are never equal: the lemmas znots and snotz refute 0 ≡ suc k and suc j ≡ 0, and these are exactly the clashes that occur when two formulas with different tags are assumed to share a code. Second, a variable index in Fin n is converted to a natural number by toℕ, and inj-toℕ records that this conversion is injective, so coding a variable by its index loses no information.

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.

The building block is mkTag k x = pr (encℕ k) x: the tag is the numeral of k and the payload is x, both elements of S since pr returns one. A small example shows how the tag separates shapes: the code of a constant will be mkTag 0 x, while the code of a variable with index i will be mkTag 1 (encℕ (toℕ i)). If two tagged pairs were equal, the tags would have to agree; mkTag-inj makes this precise, composing pr-inj and encℕ-inj to return (j ≡ k) × (x ≡ y). Its dual, clash, handles the negative case: given a proof that the tags j and k cannot be equal, it extracts the tag equation from an equality of tagged pairs and contradicts that proof, concluding in any type A of the ambient level.

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

The body of clash runs this argument in one line. mkTag-inj p .fst is the equation j ≡ k extracted from the assumed equality of codes; feeding it to the hypothesis ne yields an element of the empty type, and Empty.rec eliminates that element to return a value of the arbitrary type A. Whenever two constructor shapes force numerals 0 and suc _ to be equal, clash converts the arithmetic refutation into the needed conclusion.

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.

A term in context n codes as an element of S by the two clauses above. A constant con x gets tag 0 and payload x, the set itself: the promised economy, since no encoding of the payload is needed. A variable var i gets tag 1 and payload the numeral of toℕ i, so the tag and the index live on different sides of the pair and cannot be confused. The injectivity proof splits by the constructors of both terms. In the constant-constant case only the payloads can differ, so mkTag-inj p .snd is directly x ≡ y, and cong con lifts it to con x ≡ con y.

⌜_⌝ᵗ : ∀ {n} → Term S n → S
⌜ con x ⌝ᵗ = mkTag  x
⌜ var i ⌝ᵗ = mkTag  (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)

The remaining branches complete the argument. In a mixed case, an equality of codes would force the numerals 0 and 1 to be equal; since 1 is a successor, znots or snotz refutes this, and clash turns the refutation into an equality of terms. In the variable-variable case the payload equation says encℕ (toℕ i) ≡ encℕ (toℕ j); encℕ-inj yields toℕ i ≡ toℕ j, and inj-toℕ promotes it to i ≡ j, from which cong var gives var i ≡ var j. Every branch ends in an equation of terms, so for each fixed n the code function is injective on Term S n. Note that n here is the number of available variable slots, not the number of variables a particular term actually uses.

⌜⌝ᵗ-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: ten constructors, ten tags. Binary constructors pair the two sub-codes, unary ones take the sub-code bare, and falsity takes a dummy payload since its tag already determines it.

Formulas use the same tagged-pair scheme, with tags 0 through 4 on the five binary constructors. A membership atom t ∈̇ u codes as tag 0 paired with the pair of the two term codes, and equality likewise at tag 1; each connective pairs the codes of its two immediate subformulas. Compare this with terms: there the payload was a bare set or a numeral, here it may itself be a built-up code, so the whole structure of a formula nests inside payloads. The recursion happens on the host inductive types Term and Formula, never on the sets themselves.

⌜_⌝ : ∀ {n} → Formula S n → S
⌜ t ∈̇ u ⌝   = mkTag   (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ t ≐ u ⌝   = mkTag   (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ φ ∧̇ ψ ⌝   = mkTag   (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ φ ∨̇ ψ ⌝   = mkTag   (pr ⌜ φ ⌝ ⌜ ψ ⌝)

Implication takes tag 4 like the other connectives. Falsity ⊥̇ is the one constructor with no parts: its tag 5 alone determines it, so the payload is the dummy numeral encℕ 0, present only so every code has the uniform form of a tagged pair. The unbounded quantifiers ∃̇ and ∀̇ are unary; their codes are tag 6 or 7 paired directly with the subformula's code.

⌜ φ ⇒̇ ψ ⌝   = mkTag   (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ ⊥̇ ⌝       = mkTag  (encℕ )
⌜ ∃̇ φ ⌝     = mkTag  ⌜ φ ⌝
⌜ ∀̇ φ ⌝     = mkTag  ⌜ φ ⌝
⌜ ∀̇∈ t φ ⌝  = mkTag  (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)

The bounded quantifiers close the list with tags 8 and 9. Each pairs the code of its bounding term with the code of its body. The arities reflect binding: the bounding term lives in the same context n as the whole formula, while the body has arity suc n, one extra variable slot for the bound variable. With this, every formula constructor has a distinct tag, and the tag plus payload determines the formula, which the next section proves.

⌜ ∃̇∈ t φ ⌝  = mkTag  (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)

The coding relation

The module next records the first cases of a relational presentation of coding. CodesT s t relates a set to a term, and Codes s φ relates a set to a formula. In this file the former contains the constant case and the latter the membership case.

CodesT has the constructor c-con, which relates the code mkTag 0 x to the constant con x. The constructor c-∈ of Codes takes derivations for the two term codes and relates their paired payload under tag 0 to the membership formula. These declarations cover exactly the cases shown here; the formula-code injectivity proof below proceeds directly from ⌜_⌝.

data CodesT {n : ℕ} : S → Term S n → Type ℓ where
  c-con : (x : S)     → CodesT (mkTag  x) (con x)

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  (pr s s')) (t ∈̇ u)

Codes determine formulas

Two formulas of the same arity with the same code are equal. Rather than compare every pair of the ten constructors directly, the proof separates a formula code into its numeric tag and payload. A type family indexed by the tag describes the corresponding constructor shape, and pairing injectivity supplies equalities of the tags and payloads. The proof then recurses only through the payload components.

The section is a proof by tag separation. Its first ingredient, tagOf, extracts the constructor index of a formula as a natural number, using the same numbering that ⌜_⌝ used to build codes: membership 0, equality 1, conjunction 2, disjunction 3. So ⌜_⌝ builds the tag into a set while tagOf reads it back out, and the section works because these two numberings agree.

tagOf : ∀ {n} → Formula S n → ℕ
tagOf (t ∈̇ u)  = 
tagOf (t ≐ u)  = 
tagOf (a ∧̇ b)  = 
tagOf (a ∨̇ b)  = 

The remaining clauses assign 4 through 9 to implication, falsity, the two unbounded quantifiers, and the two bounded quantifiers. Every formula therefore has a tag in 0 through 9, and no two constructors share one, which is exactly what makes the tag able to identify the constructor shape.

tagOf (a ⇒̇ b)  = 
tagOf ⊥̇        = 
tagOf (∃̇ a)    = 
tagOf (∀̇ a)    = 
tagOf (∀̇∈ t a) = 

The second ingredient, payOf, extracts the payload the same way: for membership and equality it is the pair of the two term codes, and for conjunction the pair of the two subformula codes. Each clause is the payload component of the matching clause of ⌜_⌝, so reading a code with tagOf and payOf recovers exactly the data ⌜_⌝ put in.

tagOf (∃̇∈ t a) = 

payOf : ∀ {n} → Formula S n → S
payOf (t ∈̇ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (t ≐ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (a ∧̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝

Disjunction and implication pair the two sub-codes, and the unbounded quantifiers return the single sub-code. Falsity is the case where extraction must agree with construction by convention: since ⌜ ⊥̇ ⌝ named the dummy numeral encℕ 0 as payload, payOf ⊥̇ names the same value rather than omitting the clause.

payOf (a ∨̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (a ⇒̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf ⊥̇        = encℕ 
payOf (∃̇ a)    = ⌜ a ⌝
payOf (∀̇ a)    = ⌜ a ⌝

The bounded quantifiers complete payOf, each pairing the code of its bounding term with the code of its body. Then shape records the bridge between the two directions: for every formula φ, the code ⌜ φ ⌝ equals mkTag (tagOf φ) (payOf φ). Since tagOf and payOf were transcribed from the clauses of ⌜_⌝, matching on φ reduces both sides to the same tagged pair, and each case holds by refl.

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

The clauses shown here carry the same justification for disjunction, implication, falsity and the unbounded existential: in every case the equation is definitional, because ⌜_⌝, tagOf and payOf were built from the same recursion on the formula. The next block finishes the remaining constructors and then turns to the converse direction.

shape (a ∧̇ b)  = refl
shape (a ∨̇ b)  = refl
shape (a ⇒̇ b)  = refl
shape ⊥̇        = refl
shape (∃̇ a)    = refl

The last shape clauses close the bounded cases, and the construction now turns around: given a tag, describe what a formula with that tag looks like. The type family Match does this. For tag k, Match k φ is the type of ways φ can arise from a constructor of index k: one dependent-pair layer per subformula slot, ending in a path φ ≡ the constructor applied to those slots. For tags 0 and 1 the slots are two terms, closing with the constructors _∈̇_ and _≐_.

shape (∀̇ a)    = refl
shape (∀̇∈ t a) = refl
shape (∃̇∈ t a) = refl

Match : ∀ {n} → ℕ → Formula S n → Type ℓ
Match {n}   φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ∈̇ u)))

Tags 2 through 4 repeat the pattern for the three binary connectives, each demanding two formulas of the same arity n. Tag 5 is the degenerate case: falsity has no slots, so Match 5 φ is just the single path φ ≡ ⊥̇, with no pair at all. This shows how the family adapts to the constructor's shape rather than imposing a uniform arity.

Match {n}   φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ≐ u)))
Match {n}   φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∧̇ b)))
Match {n}   φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∨̇ b)))
Match {n}   φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ⇒̇ b)))
Match      φ = φ ≡ ⊥̇

The quantifier tags carry the arity shift. For tags 6 and 7 the single slot is a formula of arity suc n; for tags 8 and 9 a term of arity n and a body of arity suc n fill the two slots, matching the constructors ∀̇∈ and ∃̇∈. Any other tag has no formulas to describe, so the family closes with the empty type Empty.⊥*; Match is thereby defined for every natural-number tag.

Match {n}  φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∃̇ a))
Match {n}  φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∀̇ a))
Match {n}  φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∀̇∈ t a))
Match {n}  φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∃̇∈ t a))
Match     _  _ = Empty.⊥*

The direction that computes witnesses is easy: matches φ builds an inhabitant of Match (tagOf φ) φ by recursion on φ. A binary formula a ∧̇ b supplies the two slots a and b, and the final path is refl because a ∧̇ b reassembles from its parts definitionally. For example, the witness for t ∈̇ u is the triple t , (u , refl).

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)

The remaining constructors follow the shape of their Match rows: falsity contributes just refl, each unbounded quantifier pairs its body with refl, and each bounded quantifier supplies its bounding term and body. Once the last constructor is covered, matches shows that every formula matches its own tag, so the tag alone narrows any formula down to one constructor shape.

matches (a ⇒̇ b)  = a , (b , refl)
matches ⊥̇        = refl
matches (∃̇ a)    = a , refl
matches (∀̇ a)    = a , refl
matches (∀̇∈ t a) = t , (a , refl)

The theorem ⌜⌝-inj is now within reach: for formulas φ and ψ of the same arity, an equality ⌜ φ ⌝ ≡ ⌜ ψ ⌝ should force φ ≡ ψ. The proof reduces to a helper go, stated inside a private block so only the theorem is exported. What go assumes is exactly what tag separation provides: ψ re-presented as a match of φ's tag, and an equality of the payloads payOf φ ≡ payOf ψ. From these it must return φ ≡ ψ.

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 =

The membership clause shows the whole mechanics, so it deserves a slow reading. The match presents ψ as t' ∈̇ u' up to a path q : ψ ≡ (t' ∈̇ u'), but the hypothesis p only equates the payloads of φ and of ψ, not of t' ∈̇ u'. Composing p with cong payOf q transports the equation along q, producing pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ ≡ pr ⌜ t' ⌝ᵗ ⌜ u' ⌝ᵗ, which pr-inj splits into equations of the term codes. Each goes through the already-proven ⌜⌝ᵗ-inj, cong₂ _∈̇_ rebuilds the constructor on both sides, and sym q retargets the right-hand side from t' ∈̇ u' to ψ. The equality clause repeats this word for word with _≐_.

    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

Every binary connective is handled by this one pattern, so the conjunction clause is worth stating as the general recipe. The match is a triple a' , (b' , q) with q : ψ ≡ (a' ∧̇ b'). The transported payload equation has the shape pr _ _ ≡ pr _ _, so pr-inj yields equations of the two sub-codes, ⌜⌝-inj lifts each recursively to an equality of subformulas, cong₂ _∧̇_ rebuilds a ∧̇ b ≡ a' ∧̇ b', and sym q points the right side at ψ. This recipe is the whole content of the remaining connective clauses.

  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))

The disjunction and implication clauses instantiate the recipe with their own constructors, changing nothing else. Falsity is the only case with no payload work at all: the match is just q : ψ ≡ ⊥̇, so sym q : ⊥̇ ≡ ψ is already the required equation, and the payload hypothesis p goes unused.

              (⌜⌝-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 ⊥̇ ψ q p = sym q

The unbounded quantifiers simplify the recipe: the payload is a single sub-code, so the transported equation is directly ⌜ a ⌝ ≡ ⌜ a' ⌝, and one recursive call wrapped in cong ∃̇_ or cong ∀̇_, closed with sym q, suffices. The bounded quantifier ∀̇∈ is where the two levels of coding meet in one constructor: after the pr-inj split, the term component is resolved by ⌜⌝ᵗ-inj and the formula component by the recursive ⌜⌝-inj, and cong₂ ∀̇∈ reassembles both, with sym q finishing as always.

  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

The bounded existential mirrors the bounded universal, completing the ten cases. The top level then assembles the theorem. Given e : ⌜ φ ⌝ ≡ ⌜ ψ ⌝, go needs a match of ψ against the tag of φ, but matches ψ lives at the tag of ψ. These may differ as numbers, so the match is transported: tp .fst is a path tagOf φ ≡ tagOf ψ, and subst along its symmetry re-indexes matches ψ to the type Match (tagOf φ) ψ, which is exactly what go expects.

  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)

The local definition tp produces the pair of equations this transport needs. Chaining sym (shape φ), the hypothesis e, and shape ψ rewrites the assumed equality of codes into an equality mkTag (tagOf φ) (payOf φ) ≡ mkTag (tagOf ψ) (payOf ψ) of tagged pairs, and mkTag-inj splits it into the tag equation and the payload equation. The tag equation drives the subst, the payload equation is go's second argument, and the theorem is complete: no ten-by-ten comparison of constructors, only the tag arithmetic plus recursion on payloads.

  where
  tp = mkTag-inj (sym (shape φ) ∙ e ∙ shape ψ)

Recap

Terms and formulas now have codes in S: ⌜_⌝ attaches a constructor tag to the codes of the parts, while constants carry their underlying set as payload. The file records the constant and membership cases of relational coding, then proves that one code determines at most one formula of a fixed arity. The construction is generic in an injective pairing and an injection of the naturals.