Algebraic Structure of IL Denotation Domains

@cite{dowty-wall-peters-1981} @cite{gallin-1975} @cite{partee-rooth-1983}

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 F.Denot τ:

• 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

@cite{partee-rooth-1983}'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).

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

theorem Core.Logic.Intensional.Algebra.neg_eq_compl {F : Frame} (p : F.Denot Ty.t) : neg p = (have this := p; this)ᶜ

theorem Core.Logic.Intensional.Algebra.conj_eq_inf {F : Frame} (p q : F.Denot Ty.t) : conj p q = min (have this := p; this) q

theorem Core.Logic.Intensional.Algebra.disj_eq_sup {F : Frame} (p q : F.Denot Ty.t) : disj p q = max (have this := p; this) q

theorem Core.Logic.Intensional.Algebra.impl_eq_himp {F : Frame} (p q : F.Denot 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 Core.Logic.Intensional.Algebra.box_eq_iInf {F : Frame} (p : F.Denot Ty.prop) : box p = ⨅ (i : F.Index), have this := p i; this

theorem Core.Logic.Intensional.Algebra.diamond_eq_iSup {F : Frame} (p : F.Denot Ty.prop) : diamond p = ⨆ (i : F.Index), have this := p i; this

theorem Core.Logic.Intensional.Algebra.box_mono {F : Frame} {p q : F.Denot Ty.prop} (h : ∀ (i : F.Index), p i → q i) : box p → box q

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

theorem Core.Logic.Intensional.Algebra.diamond_mono {F : Frame} {p q : F.Denot Ty.prop} (h : ∀ (i : F.Index), p i → q i) : diamond p → diamond q

diamond is monotone.

theorem Core.Logic.Intensional.Algebra.forallEntity_eq_iInf {F : Frame} (body : F.Entity → F.Denot Ty.t) : forallEntity body = ⨅ (x : F.Entity), have this := body x; this

theorem Core.Logic.Intensional.Algebra.existsEntity_eq_iSup {F : Frame} (body : F.Entity → F.Denot Ty.t) : existsEntity body = ⨆ (x : F.Entity), have this := body x; this

@cite{partee-rooth-1983}'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 Core.Logic.Intensional.Algebra.genConj_eq_inf_t {F : Frame} (p q : F.Denot Ty.t) : Conjunction.genConj Ty.t F p q = min (have this := p; this) q

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

theorem Core.Logic.Intensional.Algebra.genDisj_eq_sup_t {F : Frame} (p q : F.Denot Ty.t) : Conjunction.genDisj Ty.t F 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 Core.Logic.Intensional.Algebra.neg_conj {F : Frame} (p q : F.Denot Ty.t) : neg (conj p q) = disj (neg p) (neg q)

theorem Core.Logic.Intensional.Algebra.neg_disj {F : Frame} (p q : F.Denot Ty.t) : neg (disj p q) = conj (neg p) (neg q)

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

theorem Core.Logic.Intensional.Algebra.genConj_et_eq_inter {F : Frame} (f g : F.Denot (Ty.e ⇒ Ty.t)) : predicateToSet (Conjunction.genConj (Ty.e ⇒ Ty.t) F f g) = predicateToSet f ∩ predicateToSet g

Predicate conjunction = set intersection of extensions.

theorem Core.Logic.Intensional.Algebra.genDisj_et_eq_union {F : Frame} (f g : F.Denot (Ty.e ⇒ Ty.t)) : predicateToSet (Conjunction.genDisj (Ty.e ⇒ Ty.t) F f g) = predicateToSet f ∪ predicateToSet g

Predicate disjunction = set union of extensions.

Model-theoretic notions from @cite{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 Core.Logic.Intensional.Algebra.trueAt {F : Frame} (p : F.Denot Ty.prop) (i : F.Index) : 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

• Core.Logic.Intensional.Algebra.trueAt p i = p i

def Core.Logic.Intensional.Algebra.valid {F : Frame} (p : F.Denot Ty.prop) : Prop

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

Equations

• Core.Logic.Intensional.Algebra.valid p = ∀ (i : F.Index), p i

def Core.Logic.Intensional.Algebra.satisfiable {F : Frame} (p : F.Denot Ty.prop) : Prop

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

Equations

• Core.Logic.Intensional.Algebra.satisfiable p = ∃ (i : F.Index), p i

def Core.Logic.Intensional.Algebra.entails {F : Frame} (premises : List (F.Denot Ty.prop)) (q : F.Denot Ty.prop) : Prop

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

Equations

• Core.Logic.Intensional.Algebra.entails premises q = ∀ (i : F.Index), (∀ p ∈ premises, Core.Logic.Intensional.Algebra.trueAt p i) → Core.Logic.Intensional.Algebra.trueAt q i

theorem Core.Logic.Intensional.Algebra.valid_eq_box {F : Frame} (p : F.Denot Ty.prop) : valid p = box p

theorem Core.Logic.Intensional.Algebra.satisfiable_eq_diamond {F : Frame} (p : F.Denot Ty.prop) : satisfiable p = diamond p

theorem Core.Logic.Intensional.Algebra.valid_trueAt {F : Frame} (p : F.Denot Ty.prop) (i : F.Index) (h : valid p) : trueAt p i

Validity implies truth at any particular index.

theorem Core.Logic.Intensional.Algebra.valid_satisfiable {F : Frame} [Inhabited F.Index] (p : F.Denot Ty.prop) (h : valid p) : satisfiable p

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

theorem Core.Logic.Intensional.Algebra.not_satisfiable_not_valid {F : Frame} [Inhabited F.Index] (p : F.Denot Ty.prop) (h : ¬satisfiable p) : ¬valid p

An unsatisfiable proposition is not valid (contrapositively).

theorem Core.Logic.Intensional.Algebra.entails_nil {F : Frame} (q : F.Denot Ty.prop) : entails [] q = valid q

Entailment from an empty premise set is validity.

theorem Core.Logic.Intensional.Algebra.entails_singleton {F : Frame} (p q : F.Denot Ty.prop) : entails [p] q = box fun (i : F.Index) => impl (p i) (q i)

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