Cylindric Algebras: Algebraic Foundation for Variable-Binding Semantics

@cite{henkin-monk-tarski-1971}

Cylindric algebras, introduced by Tarski and systematically developed in @cite{henkin-monk-tarski-1971}, provide the algebraic foundation for first-order predicate logic with equality. A cylindric algebra of dimension α is a Boolean algebra enriched with cylindrification operators cκ (existential quantification over coordinate κ) and diagonal elements dκl (equality between coordinates κ and l), satisfying axioms (C₀)–(C₇).

Every framework in this library that binds variables — whether over entities, times, situations, or discourse referents — operates on assignments ℕ → D and therefore lives inside the same cylindric set algebra of dimension ω. The two primitive operations, cylindrification (∃d. φ(g[n↦d])) and diagonal (g(n) = g(m)), recur across the entire codebase under different names. This module provides the single algebraic source.

Connections across the library

Proved bridges (Core/CylindricAlgebra/)

The bridge modules in Core/CylindricAlgebra/ prove algebraic identities (not analogies) between framework-specific operations and cylindric ops.

Framework	Operation	= Cylindric	Bridge
VarAssignment	∃ d, p (updateVar g n d)	cylindrify n p g	VarAssignment.lean
VarAssignment	lookupVar n g = lookupVar m g	diagonal n m g	VarAssignment.lean
CDRT (@cite{muskens-1996})	closure (new n ;; φ)	cylindrify n (closure φ)	DynamicSemantics.lean
CDRT	eq' (dref n) (dref m)	diagonal n m	DynamicSemantics.lean
Charlow (@cite{charlow-2019})	staticExists x body	cylindrify x body	DynamicSemantics.lean
Charlow	dynamicExists x body	cylindrify x body	DynamicSemantics.lean
DRS/Accessibility	closure (introReg n ;; D)	cylindrify n (closure D)	Accessibility.lean
DPL (@cite{groenendijk-stokhof-1991})	closure (DPLRel.exists_ x φ)	cylindrify x (closure φ)	DPL/Bridge.lean
DPL	closure (atom (g(x) = g(y)))	diagonal x y	DPL/Bridge.lean

Unproved connections (same algebra, bridges not yet formalized)

These frameworks use Assignment.update or VarAssignment.updateVar internally, so their quantificational operations are instances of cylindrification by the same argument — the bridge theorems just haven't been written yet.

Framework	Its existential	Cylindric reading
DPL (@cite{groenendijk-stokhof-1991})	moved to Proved bridges	see DPL/Bridge.lean
PLA (@cite{dekker-2012})	exists_ i φ	cylindrify i (⟦φ⟧)
DynamicGQ (@cite{chierchia-1995})	{p \| ∃ x, P x ∧ p.2 = q.2.update v x}	cylindrify v P
Bilateral Update (@cite{aloni-2022})	exists_ x domain φ	cylindrify x (domain ∩ φ)
PIP (@cite{keshet-abney-2024})	exists_ v domain body	cylindrify v (domain ∩ body)
File Change (@cite{heim-1982})	indefinite extends Dom, widens Sat	cylindrify n (⟦φ⟧)
Kamp & Reyle DRS (@cite{kamp-reyle-1993})	box [n] [conds]	cylindrify n (interp conds)
IntensionalCDRT (@cite{hofmann-2025})	intensional new n ;; φ	cylindrify n (closure φ)

Same algebra, different base type

These frameworks instantiate VarAssignment D at a non-entity domain. The cylindric axioms (C1–C7) hold for any D; only the base type differs.

Framework	Domain D	Its binder	Cylindric reading
@cite{partee-1973} tense	Time	λt. φ(g[n↦t])	cylindrify n φ over temporal assignments
@cite{percus-2000} situations	Situation	λs. φ(g[n↦s])	cylindrify n φ over situation assignments
@cite{heim-kratzer-1998}	Entity	λx. φ(g[n↦x])	cylindrify n φ over entity assignments
@cite{abusch-1997} tense	Time	temporal updateVar	cylindrify n φ over temporal assignments

Structural parallels (not assignment-based)

These are not instances of assignment cylindrification but share the same algebraic shape. Formalizing these would require showing they satisfy C0–C7 over a different carrier.

Framework	Analogue of cylindrify	Notes
Team Semantics	{s[x↦d] \| s ∈ T, d ∈ D}	Powerset lifting of cylindrify
Update Semantics (@cite{veltman-1996})	state elimination	Weaker — no diagonal
Continuation semantics	shift/reset scope	Different algebraic structure

Structure

• §1: Abstract cylindric algebra class (HMT Def 1.1.1)
• §2: Support and cylindrification on assignments
• §3: Cylindric algebra axioms C1–C4 for the assignment algebra
• §4: Diagonal elements on assignments
• §5: Axioms C5–C7 for the assignment algebra
• §6: Substitution via cylindrification + diagonal (HMT §1.5)
• §7: Derived theorems (HMT §1.2)

class Core.CylindricAlgebra.CylAlg (α : Type u_1) (A : Type u_2) [BooleanAlgebra A] : Type (max u_1 u_2)

A cylindric algebra of dimension α (@cite{henkin-monk-tarski-1971}, Def 1.1.1).

An algebraic structure 𝔄 = ⟨A, +, ·, -, 0, 1, cκ, dκl⟩ where ⟨A, +, ·, -, 0, 1⟩ is a Boolean algebra (axiom C₀) and the cylindrifications cκ and diagonal elements dκl satisfy axioms (C₁)–(C₇).

• cyl : α → A → A

  Cylindrification at coordinate κ.

• diag : α → α → A

  Diagonal element for coordinates κ, l.

• cyl_bot (κ : α) : cyl κ ⊥ = ⊥
• le_cyl (κ : α) (x : A) : x ≤ cyl κ x
• cyl_inf_cyl (κ : α) (x y : A) : cyl κ (x ⊓ cyl κ y) = cyl κ x ⊓ cyl κ y
• cyl_comm (κ l : α) (x : A) : cyl κ (cyl l x) = cyl l (cyl κ x)
• diag_refl (κ : α) : diag κ κ = ⊤
• diag_cyl (κ l m : α) : κ ≠ l → κ ≠ m → diag l m = cyl κ (diag l κ ⊓ diag κ m)
• cyl_diag_compl (κ l : α) (x : A) : κ ≠ l → cyl κ (diag κ l ⊓ x) ⊓ cyl κ (diag κ l ⊓ xᶜ) = ⊥

def Core.CylindricAlgebra.invariantOn {E : Type u_1} (p : Assignment E → Prop) (B : List ℕ) : Prop

A predicate on assignments is invariant on B if it only depends on the values of registers in B: assignments that agree on B satisfy p identically.

Equations

• Core.CylindricAlgebra.invariantOn p B = ∀ (g₁ g₂ : Core.Assignment E), (∀ (n : ℕ), n ∈ B → g₁ n = g₂ n) → (p g₁ ↔ p g₂)

def Core.CylindricAlgebra.cylindrify {E : Type u_1} (n : ℕ) (p : Assignment E → Prop) : Assignment E → Prop

Cylindrification at register n: existentially quantify over the value at slot n, leaving all other slots fixed.

In cylindric algebra notation, cₙ(p)(g) = ∃e. p(g[n↦e]).

Equations

• Core.CylindricAlgebra.cylindrify n p g = ∃ (e : E), p (g.update n e)

def Core.CylindricAlgebra.cylClosed {E : Type u_1} (n : ℕ) (p : Assignment E → Prop) : Prop

A predicate is cylindrification-closed at register n if abstracting over n doesn't change the predicate: cₙ(p) = p. This means p doesn't depend on register n.

Equations

• Core.CylindricAlgebra.cylClosed n p = (Core.CylindricAlgebra.cylindrify n p = p)

theorem Core.CylindricAlgebra.cylClosed_of_invariantOn {E : Type u_1} {p : Assignment E → Prop} {B : List ℕ} {n : ℕ} (hinv : invariantOn p B) (hn : ¬n ∈ B) : cylClosed n p

If p is invariant on B and n ∉ B, then p is cylindrification-closed at n. Invariance on B implies p doesn't depend on any register outside B.

theorem Core.CylindricAlgebra.invariantOn_nil_iff {E : Type u_1} {p : Assignment E → Prop} : invariantOn p [] ↔ ∀ (g₁ g₂ : Assignment E), p g₁ ↔ p g₂

invariantOn p [] is equivalent to WeakestPrecondition.isProper: the predicate takes the same value everywhere.

We verify that cylindrify on Assignment E → Prop satisfies the cylindric set algebra axioms (@cite{henkin-monk-tarski-1971}, §1.1). Together with the Boolean algebra structure on Assignment E → Prop, this establishes that predicates on assignments form an ω-dimensional cylindric set algebra with base E.

theorem Core.CylindricAlgebra.cylindrify_bot {E : Type u_1} (n : ℕ) : (cylindrify n fun (x : Assignment E) => False) = fun (x : Assignment E) => False

C1: Cylindrification preserves the empty set. cₙ(⊥) = ⊥.

theorem Core.CylindricAlgebra.le_cylindrify {E : Type u_1} (n : ℕ) (p : Assignment E → Prop) (g : Assignment E) : p g → cylindrify n p g

C2: Every element is below its cylindrification. p ≤ cₙ(p).

Proof: witness the current value at register n.

theorem Core.CylindricAlgebra.cylindrify_inter_cylindrify {E : Type u_1} (n : ℕ) (p q : Assignment E → Prop) : (cylindrify n fun (g : Assignment E) => p g ∧ cylindrify n q g) = fun (g : Assignment E) => cylindrify n p g ∧ cylindrify n q g

C3: Cylindrification distributes over conjunction with a cylindrified factor. cₙ(p ∧ cₙ(q)) = cₙ(p) ∧ cₙ(q).

theorem Core.CylindricAlgebra.cylindrify_comm {E : Type u_1} (n m : ℕ) (p : Assignment E → Prop) : cylindrify n (cylindrify m p) = cylindrify m (cylindrify n p)

C4: Cylindrifications commute. cₙ(cₘ(p)) = cₘ(cₙ(p)).

def Core.CylindricAlgebra.diagonal {E : Type u_1} (κ l : ℕ) : Assignment E → Prop

Diagonal element: the set of assignments where registers κ and l agree. Dκl = {g ∈ ωU : g(κ) = g(l)}.

In DRT, this is the denotation of the identity condition uκ is ul. In predicate logic, it corresponds to the equation vκ = vl.

Equations

• Core.CylindricAlgebra.diagonal κ l g = (g κ = g l)

theorem Core.CylindricAlgebra.diagonal_refl {E : Type u_1} (κ : ℕ) : diagonal κ κ = fun (x : Assignment E) => True

C₅: Every assignment agrees with itself at any register. Dκκ = ωU.

theorem Core.CylindricAlgebra.diagonal_cyl {E : Type u_1} (κ l m : ℕ) (hκl : κ ≠ l) (hκm : κ ≠ m) : diagonal l m = cylindrify κ fun (g : Assignment E) => diagonal l κ g ∧ diagonal κ m g

C₆: Diagonal composition via cylindrification.

If κ ≠ l and κ ≠ m, then Dlm = Cκ(Dlκ ∩ Dκm): two registers agree iff there exists a witness value at a third register matching both. This is the algebraic expression of transitivity of equality.

theorem Core.CylindricAlgebra.cyl_diag_compl {E : Type u_1} (κ l : ℕ) (p : Assignment E → Prop) (hκl : κ ≠ l) : (fun (g : Assignment E) => cylindrify κ (fun (g' : Assignment E) => diagonal κ l g' ∧ p g') g ∧ cylindrify κ (fun (g' : Assignment E) => diagonal κ l g' ∧ ¬p g') g) = fun (x : Assignment E) => False

C₇: Substitution is functional.

If κ ≠ l, then Cκ(Dκl ∩ X) ∩ Cκ(Dκl ∩ Xᶜ) = ∅. Both witnesses must equal g l, so both conjuncts operate on the same updated assignment, contradicting p and ¬p.

def Core.CylindricAlgebra.substitute {E : Type u_1} (κ l : ℕ) (p : Assignment E → Prop) : Assignment E → Prop

Algebraic substitution: replace coordinate κ with the value at l.

σ^κ_l(x) = cκ(dκl · x) (@cite{henkin-monk-tarski-1971}, §1.5). The substitution first constrains register κ to equal register l (via the diagonal dκl), then existentially abstracts over the old value at κ (via cylindrification cκ).

In DRT, this is anaphora resolution: "uκ refers to whatever ul refers to."

Equations

• Core.CylindricAlgebra.substitute κ l p = Core.CylindricAlgebra.cylindrify κ fun (g : Core.Assignment E) => Core.CylindricAlgebra.diagonal κ l g ∧ p g

def Core.CylindricAlgebra.directSubst {E : Type u_1} (κ l : ℕ) (p : Assignment E → Prop) : Assignment E → Prop

Direct (semantic) substitution: evaluate p with register κ reading from register l.

Equations

• Core.CylindricAlgebra.directSubst κ l p g = p (g.update κ (g l))

theorem Core.CylindricAlgebra.substitute_eq_directSubst {E : Type u_1} (κ l : ℕ) (p : Assignment E → Prop) (h : κ ≠ l) : substitute κ l p = directSubst κ l p

Algebraic substitution equals direct substitution (HMT §1.5).

The cylindric algebra expression cκ(dκl · x) computes the same predicate as directly evaluating x with register κ replaced by the value at register l.

For DRT: resolving an anaphoric link uκ = ul (diagonal) followed by dref closure (cylindrification) gives the same result as directly reading register l in place of register κ.

theorem Core.CylindricAlgebra.substitute_self {E : Type u_1} (κ : ℕ) (p : Assignment E → Prop) : substitute κ κ p = cylindrify κ p

Self-substitution is cylindrification. σ^κ_κ(x) = cκ(x).

theorem Core.CylindricAlgebra.substitute_invariant {E : Type u_1} (κ l : ℕ) (p : Assignment E → Prop) (h : κ ≠ l) (hinv : cylClosed κ p) : substitute κ l p = p

Substitution preserves invariance: if p doesn't depend on register κ, then substituting at κ doesn't change the predicate.

theorem Core.CylindricAlgebra.cylindrify_eq_bot_iff {E : Type u_1} (κ : ℕ) (p : Assignment E → Prop) : (cylindrify κ p = fun (x : Assignment E) => False) ↔ p = fun (x : Assignment E) => False

HMT Theorem 1.2.1: cκ(x) = 0 iff x = 0.

theorem Core.CylindricAlgebra.cylindrify_top {E : Type u_1} [Nonempty E] (κ : ℕ) : (cylindrify κ fun (x : Assignment E) => True) = fun (x : Assignment E) => True

HMT Theorem 1.2.2: cκ(1) = 1.

theorem Core.CylindricAlgebra.cylindrify_idem {E : Type u_1} (κ : ℕ) (p : Assignment E → Prop) : cylindrify κ (cylindrify κ p) = cylindrify κ p

HMT Theorem 1.2.3: cκ(cκ(x)) = cκ(x). Cylindrification is idempotent.

theorem Core.CylindricAlgebra.cylClosed_iff_range {E : Type u_1} (κ : ℕ) (p : Assignment E → Prop) : cylClosed κ p ↔ ∃ (q : Assignment E → Prop), p = cylindrify κ q

HMT Corollary 1.2.4: cylClosed κ p ↔ p = cκ(q) for some q.

theorem Core.CylindricAlgebra.cylindrify_or {E : Type u_1} (κ : ℕ) (p q : Assignment E → Prop) : (cylindrify κ fun (g : Assignment E) => p g ∨ q g) = fun (g : Assignment E) => cylindrify κ p g ∨ cylindrify κ q g

HMT Theorem 1.2.6(ii): Cylindrification distributes over join. cκ(x + y) = cκ(x) + cκ(y).