Describing the closed domain of formula codes

Agda already provides an inductive type of formulas and an external operation that assigns sets as their codes. To reason about syntax inside set theory, however, the model needs a formula in its own language that describes a candidate set of formula keys. This chapter constructs that bounded description: its shape half reads the immediate structure of keys already in the candidate domain, and its closure half generates compound keys from legal constituents.

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

The description will be constructive. It records only bounded membership, pairing, tags, and the immediate constituents of a formula key, so its definition requires no instance of excluded middle.

open import Base.Prelude

Fix a universe level. The main parameters introduced below are a candidate code domain C, a working set w that supplies constants, a set E intended to hold environment-tower entries, and ten named positions N for constructor tags. An intended entry of E pairs an arity with its environment set, but the formula defined here does not itself assert that E is the canonical tower; later adequacy hypotheses supply that fact.

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

The target is an object-language formula built from membership, equality, connectives, and bounded quantifiers. Its quantifiers will range only over sets already named in the description or over small containers used to unpack pairs. This is the syntactic reason the final formula can be certified as Δ₀.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using
  ( checkΔ₀; Δ₀ )

All formulas are interpreted over the constructible carrier. Ordered-pair and graph-application predicates let that internal language inspect keys of the form (arity, tagged payload) without assuming that set-coded pairs have primitive projections.

import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Model {ℓ} using ( prAtL; appAt )
open import L.Coding.Expressions {ℓ} using ( sucAtL )

Nested bounded quantifiers introduce temporary witnesses at the front of an environment. Named finite slots and their shifts keep C, w, the arity, and all ten tags referring to the same values while those witnesses are unpacked.

import L.Coding.Expressions {ℓ} as CodingExpressions
module E = CodingExpressions.PairExpression
open import L.Coding.Quantification {ℓ} using
  ( i0; i1; i2; i3; i4; i5; i6; i7; i8; sh
  ; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9

Pair readers expose both components while keeping every witness bounded. A finite disjunction will then combine the ten possible outer constructors into one shape test, and the corresponding bounded universal readers will express closure for all legal inputs.

  ; sndEx; sndAll; bothEx; bothAll; bigOr )

Finite indices and set-theoretic numerals have different roles here. The map N names ten positions in the surrounding environment, while toℕ identifies which numeral from zero through nine belongs at each tag position. Shifting preserves those references when bounded witnesses extend the environment. The arity stored in an entry of E is not certified as a numeral at this point; that identification comes later from the environment-tower hypotheses.

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.Unit using ( tt )
open import Cubical.Data.Vec using ( lookup )
open import Cubical.HITs.CumulativeHierarchy.Constructions

The ten constructor tags are represented by the von Neumann numerals from zero through nine. Their numerical separation will later distinguish the two atomic relations, three binary connectives, falsity, and four quantifiers.

  using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_ )

Write S for the carrier of constructible sets. The candidate domain, its keys, the working set, and the tower entries are all elements of this one carrier when the object-language formulas are interpreted.

open hPropStructure 𝒮ʟ using ( S )

Thus the formulas constructed below can be read in finite environments of constructible elements. We begin with the smallest local question: which tagged sets count as term codes at a fixed arity?

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ )

Describing shape and closure

The term predicate accepts either a pair tagged by slot N0 whose payload lies in the working set w, or a pair tagged by slot N1 whose payload lies in the arity set ar. Under the intended tag assignment these are, respectively, constants and free variables. At this stage ar is only a set; identifying it with a natural-number numeral requires the environment-tower facts used later.

isTm : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m
isTm t ar w N0 N1 =
    sndEx t N0 (var i0 ∈̇ var (sh  w))
  ∨̇ sndEx t N1 (var i0 ∈̇ var (sh  ar))

For a fixed payload r, keyUp C ar r says that the full key (ar + 1, r) belongs to C, where ar + 1 is expressed by the internal successor relation. Quantifier shape clauses use this predicate for their bodies. It asserts membership of that fixed successor-arity key, without independently checking the shape of r or that ar is a numeral.

keyUp : ∀ {m} → Fin m → Fin m → Fin m → Formula S m
keyUp C ar r =
  ∃̇∈ (var C) (∃̇∈ (var i0) (∃̇∈ (var i0)
    (prAtL i2 i0 (sh  r) ∧̇ sucAtL (sh  ar) i0)))

A formula key has the uniform form (ar, (N, p)): ar is its arity, N is its constructor tag, and p is its payload. The inner tagged payload (N, p) is formed first and is then paired with the arity. Different constructors change the structure of p, while leaving this outer layout fixed.

keyExpr : ∀ {m} → Fin m → Fin m → E.Expr m → E.Expr m
keyExpr ar N p = E.pair (E.slot ar) (E.pair (E.slot N) p)

For either atomic relation, the payload has the form ((Nx, x), (Ny, y)). Each inner pair records both the kind of term and its payload, so the left and right terms may independently be constants or variables while the atomic formula keeps one uniform key shape.

atomKeyExpr : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → E.Expr m
atomKeyExpr ar N Nx x Ny y = keyExpr ar N
  (E.pair (E.pair (E.slot Nx) (E.slot x))
    (E.pair (E.slot Ny) (E.slot y)))

A bounded-quantifier payload pairs a tagged bound term (Nx, x) with a body payload a. The surrounding key records the current arity; a separate keyUp condition is what requires the full key (arity + 1, a) for the body to lie in the domain.

bndKeyExpr : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → E.Expr m
bndKeyExpr ar N Nx x a = keyExpr ar N
  (E.pair (E.pair (E.slot Nx) (E.slot x)) (E.slot a))

The first membership template says that a nested pair (ar, (N, a)) lies in the candidate domain. It merely records this set membership; whether N is the tag of an appropriate unary constructor and whether a is a legal constituent are conditions imposed by the surrounding clause.

unKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Formula S m
unKey C ar N a = E.member (keyExpr ar N (E.slot a)) (var C)

The binary template replaces the unary payload by the pair (a, b). Later clauses use it for conjunction, disjunction, and implication after separately requiring both same-arity subkeys to belong to C.

binKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m
binKey C ar N a b = E.member (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C)

The atomic template puts two tagged term payloads into the key. Membership in C is again the only assertion made here; the atomic shape and closure clauses supply the term bounds and select tag zero or one for the outer relation.

atomKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m
atomKey C ar N Nx x Ny y = E.member (atomKeyExpr ar N Nx x Ny y) (var C)

A bounded quantifier differs from an unbounded one by carrying a bound term as well as a body. Its payload ((Nx, x), a) records the tagged bound term and the body payload, but this membership template alone asserts no legality. The surrounding shape condition checks the term at the current arity and the full body key at the successor arity; the closure condition uses the same two constituents in the generating direction.

bndKey : ∀ {m} → Fin m → Fin m → Fin m → Fin m → Fin m → Fin m → Formula S m
bndKey C ar N Nx x a = E.member (bndKeyExpr ar N Nx x a) (var C)

The tag agreement says that the ten slots carry exactly the numerals zero through nine, each slot matched to its position. This is what lets every later formula refer to "the tag of the membership atom" and mean the same slot everywhere.

Tags : ∀ {m} (γ : S ^ m) (N : Fin  → Fin m) → Type (ℓ-suc ℓ)
Tags γ N = (k : Fin ) → fst (lookup (N k) γ) ≡ # (toℕ k)

When a formula is read in an environment extended by bound variables, the ten tag slots shift with the environment; the shifted naming keeps every clause aligned with the same tags.

shN : ∀ {m} (j : ℕ) → (Fin  → Fin m) → Fin  → Fin (j + m)
shN j N k = sh j (N k)

We can now ask the inward question for a member of the candidate domain: which evidence makes its payload one of the permitted constructor forms? Although there are ten constructor tags, only five kinds of payload condition are needed, because the two atomic relations, the three binary connectives, the two unbounded quantifiers, and the two bounded quantifiers share their respective component patterns.

module Shape {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) where
  private
    C9 w9 : Fin ( + m)
    C9 = sh  C
    w9 = sh  w

The five payload shapes are written out. Atomic payloads demand two legal terms; binary payloads demand two same-arity subkeys already in the domain; the falsity payload is the numeral zero; and the unbounded-quantifier payload demands a body key at the successor arity.

  atomPay binPay conPay quPay bqPay : Formula S ( + m)
  atomPay = bothEx i0 (isTm i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) ∧̇ isTm i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)))
  binPay  = bothEx i0 (appAt (sh  C) i8 i1 ∧̇ appAt (sh  C) i8 i0)
  conPay  = var i0 ≐ var (sh  (N f0))
  quPay   = keyUp C9 i5 i0

For a bounded quantifier, the payload contains a legal bound term at the current arity and a body payload whose full key belongs to the domain at arity increased by one. The conjunction records both obligations; it does not choose a decoded body formula.

  bqPay   = bothEx i0 (isTm i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) ∧̇ keyUp (sh  C) i8 i0)

The first four tags separate the two atomic relations and the first two binary connectives: tag zero is membership, tag one is equality, tag two is conjunction, and tag three is disjunction. The first pair shares the atomic payload condition, while the second pair shares the binary one; their distinct numerals still retain the outer constructor.

  payN : ℕ → Formula S ( + m)
  payN  = atomPay
  payN  = atomPay
  payN  = binPay
  payN  = binPay

Tag four is implication, tag five is falsity, tags six and seven are the unbounded existential and universal quantifiers, and tag eight is the bounded universal quantifier. Their payload conditions are, respectively, two same-arity subkeys, the fixed numeral zero, a body key at the successor arity, and a current-arity bound term together with such a body.

  payN  = binPay
  payN  = conPay
  payN  = quPay
  payN  = quPay
  payN  = bqPay

Tag nine is the bounded existential quantifier and uses the same bounded-quantifier payload condition as tag eight. The final equation makes payN total on natural numbers by returning falsity above nine; since pay calls it only through an index in Fin 10, that fallback is unreachable in the ten-way shape test.

  payN  = bqPay
  payN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) = ⊥̇

At this point every one of the ten tags has a payload test. The next step is to connect the test indexed by k with an actual tagged payload, and then combine all ten indexed alternatives into the shape condition.

  pay : Fin  → Formula S ( + m)
  pay k = payN (toℕ k)

For a chosen constructor index k, the outer payload is required to split as (N k, r), and the remaining component r must satisfy the payload condition for that tag. The arity has already been exposed by the surrounding shape formula; this clause decomposes the tagged payload, rather than quantifying over a member of the arity.

  at : Fin  → Formula S ( + m)
  at k = sndEx i0 (sh  (N k)) (pay k)

The ten shape clauses are collected into one finite disjunction. Thus a single formula states that the tagged payload matches at least one of the ten constructor shapes, without introducing an additional unbounded quantifier.

  ten : Formula S ( + m)
  ten = bigOr  at

The shape half starts from each existing member c of the candidate domain. It chooses an entry (ar, F) from E, decomposes c as (ar, p), and requires p to match one of the ten tagged payload shapes. Composite shapes already require their immediate formula subkeys to lie in C. Semantically, these bounded existential witnesses are propositionally truncated, so this condition supplies no chosen decomposition and asserts no uniqueness of decoding.

shapeAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
shapeAt C w E N =
  ∀̇∈ (var C) (∃̇∈ (var (sh  E)) (bothEx i0 (sndEx i4 i1 (Shape.ten C w N))))

The second half turns to the outward question. Fix an entry of E and use its first component as the common arity. The closure clauses state which compound keys must enter C whenever their terms are legal at that arity and their immediate formula keys already belong to C at the required current or successor arity.

module Close {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) where
  private
    C4 w4 : Fin ( + m)
    C4 = sh  C
    w4 = sh  w

An atomic generation clause fixes an outer relation tag and one tag for each term. It ranges the two payloads over the corresponding bounds X and Y, then places the resulting atomic key in C. The eight later instances choose each term tag as constant or variable and choose X and Y as the working set or the current arity.

  atomClose : (k Nx Ny : Fin ) (X : Fin ( + m)) (Y : Fin ( + m)) → Formula S ( + m)
  atomClose k Nx Ny X Y =
    ∀̇∈ (var X) (∀̇∈ (var Y) (atomKey (sh  C) i3 (sh  (N k)) (sh  (N Nx)) i1 (sh  (N Ny)) i0))

Binary closure demands that any two same-arity members of the domain generate the key of each binary connective applied to them.

  binClose : (k : Fin ) → Formula S ( + m)
  binClose k =
    ∀̇∈ (var C4) (sndAll i0 i2 (∀̇∈ (var (sh  C)) (sndAll i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0))))

Falsity closure places the key of the falsity symbol, with its zero payload, into the domain.

  conClose : (k : Fin ) → Formula S ( + m)
  conClose k = unKey C4 i1 (sh  (N k)) (sh  (N f0))

For an unbounded quantifier, take any member of C that decomposes as a body key at arity ar + 1. The clause then requires the corresponding quantified key at arity ar to belong to C. This is the generating direction from an existing immediate constituent to the compound formula.

  quClose : (k : Fin ) → Formula S ( + m)
  quClose k = ∀̇∈ (var C4) (bothAll i0 (sucAtL i5 i1 ⇒̇ unKey (sh  C) i5 (sh  (N k)) i0))

The bounded-quantifier clause adds a bound term at the current arity. Once a member of C is recognized as a body key at arity ar + 1, every payload in the chosen term bound X generates the bounded-quantifier key at arity ar; later instances choose the constant and variable cases separately.

  bqClose : (k Nx : Fin ) (X : Fin ( + m)) → Formula S ( + m)
  bqClose k Nx X =
    ∀̇∈ (var C4) (bothAll i0 (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1)))

The closure conjunction opens with the eight atomic clauses: two atomic symbols with two term slots each, every slot being either a constant or a variable, give eight combinations.

  all : Formula S ( + m)
  all =
      atomClose f0 f0 f0 w4 (sh  w4) ∧̇ (atomClose f0 f0 f1 w4 i2
    ∧̇ (atomClose f0 f1 f0 i1 (sh  w4) ∧̇ (atomClose f0 f1 f1 i1 i2
    ∧̇ (atomClose f1 f0 f0 w4 (sh  w4) ∧̇ (atomClose f1 f0 f1 w4 i2

The conjunction continues with the last two atomic clauses, completing all four term-shape combinations for equality. It then adds three binary clauses, one falsity clause, two unbounded-quantifier clauses, and four bounded-quantifier clauses. Thus the complete count is eight atomic, three binary, one falsity, two unbounded, and four bounded clauses, for eighteen in total.

    ∧̇ (atomClose f1 f1 f0 i1 (sh  w4) ∧̇ (atomClose f1 f1 f1 i1 i2
    ∧̇ (binClose f2 ∧̇ (binClose f3 ∧̇ (binClose f4
    ∧̇ (conClose f5 ∧̇ (quClose f6 ∧̇ (quClose f7
    ∧̇ (bqClose f8 f0 (sh  w) ∧̇ (bqClose f8 f1 i5
    ∧̇ (bqClose f9 f0 (sh  w) ∧̇ bqClose f9 f1 i5))))))))))))))))

The closure half applies all eighteen generation clauses at every entry of the set named by E. Once an entry is unpacked, its first component supplies the common arity for the constructors. This formula does not certify that the entries form the canonical environment tower or even that every recorded arity is a numeral; later hypotheses provide those facts. At any valid tower entry, the direction remains from legal constituents to the corresponding compound key, rather than from an arbitrary member of C back to its parts.

closeAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
closeAt C w E N = ∀̇∈ (var E) (bothAll i0 (Close.all C w N))

The full description conjoins the two directions. shapeAt reads every existing member inward and requires its immediate subkeys to remain in the candidate domain; closeAt starts with legal constituents and generates the corresponding compound key. Either condition alone is insufficient: shape alone may omit genuine keys, while closure alone may permit additional members. The conjunction is still only a specification relative to w, E, and N; it does not by itself construct the domain or prove it is the canonical one.

codesAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
codesAt C w E N = shapeAt C w E N ∧̇ closeAt C w E N

The final computation produces a certificate that every quantifier in codesAt is bounded, so codesAt lies in the class Δ₀. This is a classification of the object-language formula that describes the candidate domain. It neither classifies individual codes as Δ₀ objects nor by itself proves existence, canonicity, or an absoluteness theorem for the described domain.

Δ₀-codesAt : ∀ {m} (C w E : Fin m) (N : Fin  → Fin m) → Δ₀ (codesAt C w E N)
Δ₀-codesAt C w E N = checkΔ₀ (codesAt C w E N) tt

Recap

The candidate-domain specification has two complementary directions. shapeAt reads each existing member as one of ten tagged constructor forms and requires every immediate formula subkey demanded by that form to lie in C; closeAt packages eighteen generation clauses that build the corresponding keys from legal terms and existing current- or successor-arity subkeys. Their conjunction is a bounded specification relative to w, E, and N.

The semantic witnesses hidden by its bounded existentials are available only under propositional truncation, so the specification selects neither a decomposition nor a decoding function. In the next chapter, the correct alphabet, tag, and environment-tower hypotheses, together with excluded middle, support two separate adequacy arguments: every candidate member merely decodes to a genuine formula key, and induction on external formulas places every genuine key in the candidate domain. External injectivity can then show that two recovered formulas of one fixed arity agree, but that separate result does not make codesAt a chosen or globally unique syntax decoder.