IL Quantification, Modality, and Identity

@cite{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 Theories/Semantics/Modality/ generalizes box/diamond here.

def Core.Logic.Intensional.impl {F : Frame} (p q : F.Denot Ty.t) : F.Denot Ty.t

Material implication. DWP Semantic Rule B.9.

Equations

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

def Core.Logic.Intensional.biconditional {F : Frame} (p q : F.Denot Ty.t) : F.Denot Ty.t

Material biconditional. DWP Semantic Rule B.10.

Equations

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

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

theorem Core.Logic.Intensional.biconditional_conj_impl {F : Frame} (p q : F.Denot Ty.t) : biconditional p q = conj (impl p q) (impl q p)

theorem Core.Logic.Intensional.impl_refl {F : Frame} (p : F.Denot Ty.t) : impl p p

theorem Core.Logic.Intensional.impl_trans {F : Frame} {p q r : F.Denot Ty.t} (hpq : impl p q) (hqr : impl q r) : impl p r

theorem Core.Logic.Intensional.contrapositive {F : Frame} {p q : F.Denot Ty.t} (h : impl p q) : impl (neg q) (neg p)

theorem Core.Logic.Intensional.biconditional_comm {F : Frame} (p q : F.Denot Ty.t) : biconditional p q = biconditional q p

def Core.Logic.Intensional.forallEntity {F : Frame} (body : F.Entity → F.Denot Ty.t) : F.Denot Ty.t

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

Equations

• Core.Logic.Intensional.forallEntity body = ∀ (x : F.Entity), body x

def Core.Logic.Intensional.existsEntity {F : Frame} (body : F.Entity → F.Denot Ty.t) : F.Denot Ty.t

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

Equations

• Core.Logic.Intensional.existsEntity body = ∃ (x : F.Entity), body x

theorem Core.Logic.Intensional.forallEntity_neg_existsEntity {F : Frame} (body : F.Entity → F.Denot Ty.t) : forallEntity body = neg (existsEntity fun (x : F.Entity) => neg (body x))

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

theorem Core.Logic.Intensional.existsEntity_neg_forallEntity {F : Frame} (body : F.Entity → F.Denot Ty.t) : existsEntity body = neg (forallEntity fun (x : F.Entity) => neg (body x))

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

theorem Core.Logic.Intensional.forallEntity_instantiate {F : Frame} (body : F.Entity → F.Denot Ty.t) (a : F.Entity) (h : forallEntity body) : body a

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

theorem Core.Logic.Intensional.existsEntity_generalize {F : Frame} (body : F.Entity → F.Denot Ty.t) (a : F.Entity) (h : body a) : existsEntity body

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

theorem Core.Logic.Intensional.forallEntity_conj {F : Frame} (p q : F.Entity → F.Denot Ty.t) : (forallEntity fun (x : F.Entity) => conj (p x) (q x)) = conj (forallEntity p) (forallEntity q)

∀ distributes over ∧.

def Core.Logic.Intensional.ident {F : Frame} {a : Ty} (x y : F.Denot a) : F.Denot 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

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

def Core.Logic.Intensional.identIntens {F : Frame} {a : Ty} (x y : F.Denot a.intens) : F.Denot 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

• Core.Logic.Intensional.identIntens x y = ∀ (i : F.Index), x i = y i

theorem Core.Logic.Intensional.ident_refl {F : Frame} {a : Ty} (x : F.Denot a) : ident x x

theorem Core.Logic.Intensional.ident_symm {F : Frame} {a : Ty} {x y : F.Denot a} (h : ident x y) : ident y x

theorem Core.Logic.Intensional.ident_trans {F : Frame} {a : Ty} {x y z : F.Denot a} (hxy : ident x y) (hyz : ident y z) : ident x z

theorem Core.Logic.Intensional.identIntens_implies_ident {F : Frame} {a : Ty} (x y : F.Denot a.intens) (i : F.Index) (h : identIntens x y) : ident (x i) (y i)

Intensional identity implies extensional identity at every index.

theorem Core.Logic.Intensional.identIntens_up {F : Frame} {a : Ty} (x y : F.Denot a) (h : ident x y) : identIntens (up x) (up y)

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

def Core.Logic.Intensional.box {F : Frame} (p : F.Denot Ty.prop) : F.Denot 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 (Theories/Semantics/Modality/Kratzer/) restricts quantification to accessible worlds via a modal base and ordering source.

Equations

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

def Core.Logic.Intensional.diamond {F : Frame} (p : F.Denot Ty.prop) : F.Denot Ty.t

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

Equations

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

theorem Core.Logic.Intensional.box_neg_diamond {F : Frame} (p : F.Denot Ty.prop) : box p = neg (diamond fun (i : F.Index) => neg (p i))

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

theorem Core.Logic.Intensional.diamond_neg_box {F : Frame} (p : F.Denot Ty.prop) : diamond p = neg (box fun (i : F.Index) => neg (p i))

◇p ↔ ¬□¬p.

theorem Core.Logic.Intensional.box_K {F : Frame} (p q : F.Denot Ty.prop) : impl (box fun (i : F.Index) => 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 Core.Logic.Intensional.box_T {F : Frame} (p : F.Denot Ty.prop) (i : F.Index) (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 Core.Logic.Intensional.necessitation {F : Frame} (p : F.Denot Ty.prop) (h : ∀ (i : F.Index), p i) : box p

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

theorem Core.Logic.Intensional.box_conj {F : Frame} (p q : F.Denot Ty.prop) : (box fun (i : F.Index) => conj (p i) (q i)) = conj (box p) (box q)

□ distributes over ∧.

theorem Core.Logic.Intensional.diamond_disj {F : Frame} (p q : F.Denot Ty.prop) : (diamond fun (i : F.Index) => disj (p i) (q i)) = disj (diamond p) (diamond q)

◇ distributes over ∨.

theorem Core.Logic.Intensional.box_implies_diamond {F : Frame} [Inhabited F.Index] (p : F.Denot Ty.prop) (h : box p) : diamond p

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

theorem Core.Logic.Intensional.box_ident_rigid {F : Frame} {a : Ty} (x y : F.Denot a) (h : ident x y) : box fun (i : F.Index) => 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 Core.Logic.Intensional.box_or_box_neg_of_up {F : Frame} (p : F.Denot Ty.t) : box (up p) ∨ box fun (i : F.Index) => neg (up p i)

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

theorem Core.Logic.Intensional.box_up_iff {F : Frame} [Inhabited F.Index] (p : F.Denot 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 Core.Logic.Intensional.box_down {F : Frame} (p : F.Denot Ty.prop) (i : F.Index) : 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.