IL Quantification, Modality, and Identity

[dowty-wall-peters-1981] Ch. 6, Semantic Rules B.5, B.9–B.13

Completes the IL semantic rule toolkit with:

• impl, biconditional — material implication and biconditional (B.9–B.10)
• forallEntity, existsEntity — quantification over entities (B.11–B.12)
• ident — typed identity (B.5)
• box, diamond — necessity and possibility as IL primitives (B.13)

These are the IL-level operators — the primitives from which Kratzer's modal semantics, tense operators, and PTQ translations are all derived. Kratzer's richer framework (modal base + ordering source) in Semantics/Modality/ generalizes box/diamond here.

def Intensional.impl {E W : Type} (p q : Denot E W Ty.t) : Denot E W Ty.t

Material implication. DWP Semantic Rule B.9.

Equations

• Intensional.impl p q = (p → q)

def Intensional.biconditional {E W : Type} (p q : Denot E W Ty.t) : Denot E W Ty.t

Material biconditional. DWP Semantic Rule B.10.

Equations

• Intensional.biconditional p q = (p ↔ q)

theorem Intensional.impl_neg_disj {E W : Type} (p q : Denot E W Ty.t) : impl p q = disj (neg p) q

theorem Intensional.biconditional_conj_impl {E W : Type} (p q : Denot E W Ty.t) : biconditional p q = conj (impl p q) (impl q p)

theorem Intensional.impl_refl {E W : Type} (p : Denot E W Ty.t) : impl p p

theorem Intensional.impl_trans {E W : Type} {p q r : Denot E W Ty.t} (hpq : impl p q) (hqr : impl q r) : impl p r

theorem Intensional.contrapositive {E W : Type} {p q : Denot E W Ty.t} (h : impl p q) : impl (neg q) (neg p)

theorem Intensional.biconditional_comm {E W : Type} (p q : Denot E W Ty.t) : biconditional p q = biconditional q p

def Intensional.forallEntity {E W : Type} (body : E → Denot E W Ty.t) : Denot E W Ty.t

Universal quantification over entities. ⟦∀x.φ⟧ = 1 iff ⟦φ⟧^{g[x↦a]} = 1 for all a ∈ A. DWP Semantic Rule B.11.

Equations

• Intensional.forallEntity body = ∀ (x : E), body x

def Intensional.existsEntity {E W : Type} (body : E → Denot E W Ty.t) : Denot E W Ty.t

Existential quantification over entities. ⟦∃x.φ⟧ = 1 iff ⟦φ⟧^{g[x↦a]} = 1 for some a ∈ A. DWP Semantic Rule B.12.

Equations

• Intensional.existsEntity body = ∃ (x : E), body x

theorem Intensional.forallEntity_neg_existsEntity {E W : Type} (body : E → Denot E W Ty.t) : forallEntity body = neg (existsEntity fun (x : E) => neg (body x))

Duality: ∀x.φ ↔ ¬∃x.¬φ.

theorem Intensional.existsEntity_neg_forallEntity {E W : Type} (body : E → Denot E W Ty.t) : existsEntity body = neg (forallEntity fun (x : E) => neg (body x))

Duality: ∃x.φ ↔ ¬∀x.¬φ.

theorem Intensional.forallEntity_instantiate {E W : Type} (body : E → Denot E W Ty.t) (a : E) (h : forallEntity body) : body a

∀x.φ → φ[a/x] — universal instantiation.

theorem Intensional.existsEntity_generalize {E W : Type} (body : E → Denot E W Ty.t) (a : E) (h : body a) : existsEntity body

φ[a/x] → ∃x.φ — existential generalization.

theorem Intensional.forallEntity_conj {E W : Type} (p q : E → Denot E W Ty.t) : (forallEntity fun (x : E) => conj (p x) (q x)) = conj (forallEntity p) (forallEntity q)

∀ distributes over ∧.

def Intensional.ident {E W : Type} {a : Ty} (x y : Denot E W a) : Denot E W Ty.t

Typed identity: α = β is a formula whenever α, β have the same type. DWP Semantic Rule B.5.

In IL, identity is extensional: ⟦α = β⟧^{M,w,t,g} = 1 iff α and β have the same extension at ⟨w,t⟩. For intensional identity (same intension at all indices), use identIntens.

Equations

• Intensional.ident x y = (x = y)

def Intensional.identIntens {E W : Type} {a : Ty} (x y : Denot E W a.intens) : Denot E W Ty.t

Intensional identity: two expressions have the same intension (agree at every index). Stronger than ident at a single index. ^α = ^β in DWP notation.

Equations

• Intensional.identIntens x y = ∀ (i : W), x i = y i

theorem Intensional.ident_refl {E W : Type} {a : Ty} (x : Denot E W a) : ident x x

theorem Intensional.ident_symm {E W : Type} {a : Ty} {x y : Denot E W a} (h : ident x y) : ident y x

theorem Intensional.ident_trans {E W : Type} {a : Ty} {x y z : Denot E W a} (hxy : ident x y) (hyz : ident y z) : ident x z

theorem Intensional.identIntens_implies_ident {E W : Type} {a : Ty} (x y : Denot E W a.intens) (i : W) (h : identIntens x y) : ident (x i) (y i)

Intensional identity implies extensional identity at every index.

theorem Intensional.identIntens_up {E W : Type} {a : Ty} (x y : Denot E W a) (h : ident x y) : identIntens (up x) (up y)

Intensional identity of up — rigid intensions of the same value are intensionally identical.

def Intensional.box {E W : Type} (p : Denot E W Ty.prop) : Denot E W Ty.t

Necessity (□): a proposition (intension of type t) is necessary iff it is true at every index.

⟦□φ⟧^{M,w,t,g} = 1 iff ⟦φ⟧^{M,w',t',g} = 1 for all w' ∈ W, t' ∈ T.

DWP Semantic Rule B.13. In Montague's original IL, □ quantifies over all indices — it is S5 necessity. Kratzer's framework (Semantics/Modality/Kratzer/) restricts quantification to accessible worlds via a modal base and ordering source.

Equations

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

def Intensional.diamond {E W : Type} (p : Denot E W Ty.prop) : Denot E W Ty.t

Possibility (◇): a proposition is possible iff it is true at some index. Dual of box.

Equations

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

theorem Intensional.box_neg_diamond {E W : Type} (p : Denot E W Ty.prop) : box p = neg (diamond fun (i : W) => neg (p i))

□ and ◇ are duals: □p ↔ ¬◇¬p.

theorem Intensional.diamond_neg_box {E W : Type} (p : Denot E W Ty.prop) : diamond p = neg (box fun (i : W) => neg (p i))

◇p ↔ ¬□¬p.

theorem Intensional.box_K {E W : Type} (p q : Denot E W Ty.prop) : impl (box fun (i : W) => impl (p i) (q i)) (impl (box p) (box q))

K axiom: □(p → q) → (□p → □q). The fundamental distribution axiom of normal modal logic.

theorem Intensional.box_T {E W : Type} (p : Denot E W Ty.prop) (i : W) (h : box p) : p i

T axiom: □p → p at index i. Reflexivity — what is necessary is actual. Requires evaluating at a specific index (since box eliminates the index).

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

Necessitation: if p holds at all indices, then □p.

theorem Intensional.box_conj {E W : Type} (p q : Denot E W Ty.prop) : (box fun (i : W) => conj (p i) (q i)) = conj (box p) (box q)

□ distributes over ∧.

theorem Intensional.diamond_disj {E W : Type} (p q : Denot E W Ty.prop) : (diamond fun (i : W) => disj (p i) (q i)) = disj (diamond p) (diamond q)

◇ distributes over ∨.

theorem Intensional.box_implies_diamond {E W : Type} [Inhabited W] (p : Denot E W Ty.prop) (h : box p) : diamond p

□p → ◇p (seriality — holds vacuously when Index is inhabited).

theorem Intensional.box_ident_rigid {E W : Type} {a : Ty} (x y : Denot E W a) (h : ident x y) : box fun (i : W) => ident (up x i) (up y i)

Necessity of identity: if ^α = ^β necessarily (rigid intensions agree), this is itself necessary. Connects to Rigidity.lean's rigid_identity_necessary.

theorem Intensional.box_or_box_neg_of_up {E W : Type} (p : Denot E W Ty.t) : box (up p) ∨ box fun (i : W) => neg (up p i)

A rigid proposition (formed by up) is either necessarily true or necessarily false.

theorem Intensional.box_up_iff {E W : Type} [Inhabited W] (p : Denot E W Ty.t) : box (up p) = p

down (up p) i is the same as p — restated via box to show that up followed by box is equivalent to the original proposition.

theorem Intensional.box_down {E W : Type} (p : Denot E W Ty.prop) (i : W) : down (up (box p)) i = box p

□ applied to the intension of p is p evaluated at every index. When p is already an intension, box p is just ∀ i, p i.