Algebraic Structure of IL Denotation Domains

[dowty-wall-peters-1981] [Gal75] [PR83]

The IL operators in Frame.lean, Quantification.lean, and Conjunction.lean are instances of general algebraic operations from mathlib's order theory.

The central observation: Montague's type-driven semantics is a hierarchy of pointwise Boolean algebras. Every conjoinable type τ (one that "ends in t") induces a CompleteLattice on Denot E W τ:

• At type t: the Boolean algebra of propositions (Prop)
• At type ⟨a, t⟩: the pointwise Boolean algebra of predicates
• At type ⟨s, t⟩: the Boolean algebra of propositions (= sets of indices)
• At type ⟨a, ⟨b, t⟩⟩: the doubly-pointwise Boolean algebra

The IL operators are lattice operations in this hierarchy:

IL operator	Lattice operation	mathlib name
neg	complement	compl (ᶜ)
conj	meet	inf (⊓)
disj	join	sup (⊔)
impl	Heyting implication	himp (⇨)
box	indexed infimum	iInf (⨅)
diamond	indexed supremum	iSup (⨆)
forallEntity	indexed infimum	iInf (⨅)
existsEntity	indexed supremum	iSup (⨆)
genConj	pointwise meet	Pi.inf
genDisj	pointwise join	Pi.sup

[PR83]'s generalized conjunction is the pointwise meet in the lattice of type τ — a fact that explains why conjunction is defined recursively over types and why it only works for conjoinable types (those admitting a lattice structure).

Denot E W .t = Prop is a CompleteBooleanAlgebra (via mathlib's Prop.instCompleteLattice and Prop.instHeytingAlgebra). The IL sentential operators are its algebraic operations.

theorem Intensional.Algebra.neg_eq_compl {E W : Type} (p : Denot E W Ty.t) : neg p = (have this := p; this)ᶜ

theorem Intensional.Algebra.conj_eq_inf {E W : Type} (p q : Denot E W Ty.t) : conj p q = min (have this := p; this) q

theorem Intensional.Algebra.disj_eq_sup {E W : Type} (p q : Denot E W Ty.t) : disj p q = max (have this := p; this) q

theorem Intensional.Algebra.impl_eq_himp {E W : Type} (p q : Denot E W Ty.t) : impl p q = (have this := p; this) ⇨ q

box and diamond are the indexed infimum and supremum over the index set — the lattice-theoretic formulation of S5 necessity and possibility.

theorem Intensional.Algebra.box_eq_iInf {E W : Type} (p : Denot E W Ty.prop) : box p = ⨅ (i : W), have this := p i; this

theorem Intensional.Algebra.diamond_eq_iSup {E W : Type} (p : Denot E W Ty.prop) : diamond p = ⨆ (i : W), have this := p i; this

theorem Intensional.Algebra.box_mono {E W : Type} {p q : Denot E W Ty.prop} (h : ∀ (i : W), p i → q i) : box p → box q

box is monotone: if p i → q i at every index, then □p → □q.

theorem Intensional.Algebra.diamond_mono {E W : Type} {p q : Denot E W Ty.prop} (h : ∀ (i : W), p i → q i) : diamond p → diamond q

diamond is monotone.

theorem Intensional.Algebra.forallEntity_eq_iInf {E W : Type} (body : E → Denot E W Ty.t) : forallEntity body = ⨅ (x : E), have this := body x; this

theorem Intensional.Algebra.existsEntity_eq_iSup {E W : Type} (body : E → Denot E W Ty.t) : existsEntity body = ⨆ (x : E), have this := body x; this

[PR83]'s generalized conjunction is the pointwise meet in the lattice of the codomain type. This explains why genConj is defined recursively: it follows the recursive lattice construction on Pi types.

The proofs are rfl because genConj unfolds to exactly the same function as the pointwise inf from Pi.instLattice.

theorem Intensional.Algebra.genConj_eq_inf_t {E W : Type} (p q : Denot E W Ty.t) : Conjunction.genConj Ty.t E W p q = min (have this := p; this) q

At type t: generalized conjunction is propositional ∧ = ⊓.

theorem Intensional.Algebra.genDisj_eq_sup_t {E W : Type} (p q : Denot E W Ty.t) : Conjunction.genDisj Ty.t E W p q = max (have this := p; this) q

At type t: generalized disjunction is propositional ∨ = ⊔.

At function and intension types, genConj/genDisj distribute pointwise (Conjunction.lean, Facts 6a–6c). The recursive structure mirrors the pointwise lattice construction Pi.instLattice: at each layer, genConj applies ⊓ on the codomain / base type. The base case above closes the induction.

With the lattice bridge in place, De Morgan laws follow directly from mathlib's compl_inf / compl_sup rather than requiring manual proof.

theorem Intensional.Algebra.neg_conj {E W : Type} (p q : Denot E W Ty.t) : neg (conj p q) = disj (neg p) (neg q)

theorem Intensional.Algebra.neg_disj {E W : Type} (p q : Denot E W Ty.t) : neg (disj p q) = conj (neg p) (neg q)

Properties (Denot E W (.e ⇒ .t) = E → Prop) are elements of a complete lattice. The lattice operations correspond to set-theoretic operations on the extensions of predicates.

theorem Intensional.Algebra.genConj_et_eq_inter {E W : Type} (f g : Denot E W (Ty.e ⇒ Ty.t)) : predicateToSet (Conjunction.genConj (Ty.e ⇒ Ty.t) E W f g) = predicateToSet f ∩ predicateToSet g

Predicate conjunction = set intersection of extensions.

theorem Intensional.Algebra.genDisj_et_eq_union {E W : Type} (f g : Denot E W (Ty.e ⇒ Ty.t)) : predicateToSet (Conjunction.genDisj (Ty.e ⇒ Ty.t) E W f g) = predicateToSet f ∪ predicateToSet g

Predicate disjunction = set union of extensions.

Model-theoretic notions from [dowty-wall-peters-1981] Def C.1. Since we work denotationally (Lean's type system is the metalanguage), these definitions apply to closed propositions — those already evaluated under some assignment.

def Intensional.Algebra.trueAt {E W : Type} (p : Denot E W Ty.prop) (i : W) : Prop

A proposition is true at index i iff it holds there. DWP Def C.1: "φ is true with respect to M and to ⟨w, t⟩ iff ⟦φ⟧^{M,w,t,g} is 1 for all value assignments g."

Equations

• Intensional.Algebra.trueAt p i = p i

def Intensional.Algebra.valid {E W : Type} (p : Denot E W Ty.prop) : Prop

A proposition is valid iff it is true at every index. Equivalently: box p.

Equations

• Intensional.Algebra.valid p = ∀ (i : W), p i

def Intensional.Algebra.satisfiable {E W : Type} (p : Denot E W Ty.prop) : Prop

A proposition is satisfiable iff it is true at some index. Equivalently: diamond p.

Equations

• Intensional.Algebra.satisfiable p = ∃ (i : W), p i

def Intensional.Algebra.entails {E W : Type} (premises : List (Denot E W Ty.prop)) (q : Denot E W Ty.prop) : Prop

Semantic entailment: p₁, ..., pₙ ⊨ q iff at every index where all premises are true, the conclusion is true.

Equations

• Intensional.Algebra.entails premises q = ∀ (i : W), (∀ p ∈ premises, Intensional.Algebra.trueAt p i) → Intensional.Algebra.trueAt q i

theorem Intensional.Algebra.valid_eq_box {E W : Type} (p : Denot E W Ty.prop) : valid p = box p

theorem Intensional.Algebra.satisfiable_eq_diamond {E W : Type} (p : Denot E W Ty.prop) : satisfiable p = diamond p

theorem Intensional.Algebra.valid_trueAt {E W : Type} (p : Denot E W Ty.prop) (i : W) (h : valid p) : trueAt p i

Validity implies truth at any particular index.

theorem Intensional.Algebra.valid_satisfiable {E W : Type} [Inhabited W] (p : Denot E W Ty.prop) (h : valid p) : satisfiable p

A valid proposition is satisfiable (when Index is inhabited).

theorem Intensional.Algebra.not_satisfiable_not_valid {E W : Type} [Inhabited W] (p : Denot E W Ty.prop) (h : ¬satisfiable p) : ¬valid p

An unsatisfiable proposition is not valid (contrapositively).

theorem Intensional.Algebra.entails_nil {E W : Type} (q : Denot E W Ty.prop) : entails [] q = valid q

Entailment from an empty premise set is validity.

theorem Intensional.Algebra.entails_singleton {E W : Type} (p q : Denot E W Ty.prop) : entails [p] q = box fun (i : W) => impl (p i) (q i)

Single-premise entailment: p ⊨ q iff □(p → q).

The pointwise Boolean-algebra structure of conjoinable types, registered explicitly by recursion on τ (base Prop, then the Pi lift for fn/intens). Instance resolution cannot synthesize these on its own — it does not unfold the Denot def — so the recursion instances make BooleanAlgebra (Denot E W τ) available for every conjoinable type. Non-conjoinable types (.e) get no instance, which is exactly correct: ⊓/⊔ are a type error on entities.

With these in scope, [PR83]'s genConj/genDisj are ⊓/⊔ at every conjoinable type (not just the t base case proved above), so the bespoke recursion is provably the pointwise lattice operation.

@[implicit_reducible]

instance Intensional.Algebra.instBooleanAlgebraDenotT {E W : Type} : BooleanAlgebra (Denot E W Ty.t)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Intensional.Algebra.instBooleanAlgebraDenotFn {E W : Type} (a b : Ty) [BooleanAlgebra (Denot E W b)] : BooleanAlgebra (Denot E W (a ⇒ b))

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Intensional.Algebra.instBooleanAlgebraDenotIntens {E W : Type} (a : Ty) [BooleanAlgebra (Denot E W a)] : BooleanAlgebra (Denot E W a.intens)

Equations

• One or more equations did not get rendered due to their size.

theorem Intensional.Algebra.genConj_eq_inf_et {E W : Type} (f g : Denot E W (Ty.e ⇒ Ty.t)) : Conjunction.genConj (Ty.e ⇒ Ty.t) E W f g = f ⊓ g

Generalized conjunction is ⊓ at ⟨e,t⟩ — the inductive step, where the earlier genConj_eq_inf_t only covered the t base case.

theorem Intensional.Algebra.genConj_eq_inf_eet {E W : Type} (f g : Denot E W (Ty.e ⇒ Ty.e ⇒ Ty.t)) : Conjunction.genConj (Ty.e ⇒ Ty.e ⇒ Ty.t) E W f g = f ⊓ g

Generalized conjunction is ⊓ at ⟨e,⟨e,t⟩⟩ (binary relations).

theorem Intensional.Algebra.genDisj_eq_sup_et {E W : Type} (f g : Denot E W (Ty.e ⇒ Ty.t)) : Conjunction.genDisj (Ty.e ⇒ Ty.t) E W f g = f ⊔ g

Generalized disjunction is ⊔ at ⟨e,t⟩.