Geurts 2005: Disjunctions as Modals

[Geu05]

Single-paper study of Bart Geurts, Entertaining Alternatives: Disjunctions as Modals (Natural Language Semantics 13:383–410). Following [Zim00], disjunctions are conjunctions of modal propositions: "S₁ or … or Sₙ" has logical form A₁M₁B₁ ∧ … ∧ AₙMₙBₙ, where

• Aᵢ is a modal domain (subset of background C, context-dependent),
• Mᵢ is a modal quantifier (∃ or ∀, paper p.394),
• Bᵢ is the descriptive content of the disjunct.

Three departures from Zimmermann (paper §3, p.391)

1. Modal flavour is not restricted to epistemic. The background C may be epistemic, deontic, circumstantial, etc.; Geurts: "I will drop the premiss that disjunctions are always epistemic modals" (p.391). Force (∃ vs ∀) is a separate dimension carried by ModalForce.
2. Overt and covert modals fuse: two operators per disjunct, not four.
3. Context dependence of modal domains Aᵢ does the work of Zimmermann's Self-Reflection Principle.

Three constraints on interpretation (paper §3, p.395)

• Exhaustivity: C ⊆ ⋃(Aᵢ ∩ Bᵢ).
• Disjointness: (Aᵢ ∩ Bᵢ) ∩ (Aⱼ ∩ Bⱼ) = ∅ for i ≠ j.
• Non-triviality: Aᵢ ≠ ∅.

Main declarations

• Disjunct, MDisjunction — substrate types for one disjunct and the list of disjuncts.
• Disjunct.holds, MDisjunction.holds — truth conditions.
• Disjunct.cell, exhaustivity, disjointness, disjointness₂, nonTriviality — the three constraints (Disjointness in n-ary form via List.Pairwise, and a binary specialisation used by the bridge theorems and Case #3).
• defaultBinding — by default A = C (paper p.394).
• fromPartialProp, fromPartialProp_*_iff_orFlex, fromPartialProp_*_iff_orBelnap — specialisation to presuppositional propositions: when domain = presup and content = assertion, the Geurts disjunction coincides pointwise with PartialProp.orFlex = PartialProp.orBelnap ([Bel70]).
• exhaustivity_implies_uninformative — used by Studies/Yagi2025.lean as the formal residue of [Sch09a]'s local-context-failure observation.

Implementation notes

• Force is the project-canonical Semantics.Modality.ModalForce (necessity | weakNecessity | possibility, [vFI08]). Geurts treats only ∃/∀; we route weakNecessity to the universal branch (every weak-necessity claim still quantifies universally over its refined best-worlds set).
• The fromPartialProp_*_iff_* lemmas are structural: PartialProp.orFlex.presup is defined as the union of disjunct presuppositions, so the iff is unfolding, not stipulation. The architecture intentionally avoids the "stipulate then prove equivalence" anti-pattern.

Scope: wide-scope only

This file formalises Geurts's wide-scope analysis: every disjunction is treated as A₁M₁B₁ ∧ … ∧ AₙMₙBₙ at LF from the outset. Free choice "◇A ∧ ◇B follows" is immediate because the LF is the conjunction; the substantive move is the LF reanalysis (p.391), not a structural inference.

Todo

• Geurts §6 (pp.405–407) flags negated disjunctions, conditional antecedents, and attitude-embedded disjunctions as cases his modal analysis "runs into trouble" with; the speaker's-content / factual-content two-level patch in the §6 closing paragraphs is not formalised here.
• [CG26] argue "You may A or may B" gets free choice from the narrow-scope LF ◇(A ∨ B) via modal concord ([Zei07]), not from wide-scope ◇A ∧ ◇B. Truth-conditionally the two analyses agree; the cross-framework comparison belongs to the later paper's study file ([CG26]).
• Geurts §5 (pp.402–404) ultimately suggests Disjointness is itself a conversational effect grounded in exhaustivity; formalised here only as the stipulated constraint, not the deeper pragmatic derivation.

Modal disjuncts and disjunction

structure Geurts2005.Disjunct (W : Type u_2) : Type u_2

A single disjunct in a modal disjunction: AᵢMᵢBᵢ.

• domain : Set W

  Modal domain Aᵢ (subset of the background, determined by context).

• force : Semantics.Modality.ModalForce

  Modal force Mᵢ (from an overt modal or a covert default).

• content : Set W

  Descriptive content Bᵢ.

@[reducible, inline]

abbrev Geurts2005.MDisjunction (W : Type u_2) : Type u_2

A modal disjunction: a conjunction of modal propositions.

Equations

• Geurts2005.MDisjunction W = List (Geurts2005.Disjunct W)

Truth conditions

def Geurts2005.Disjunct.holds {W : Type u_1} (d : Disjunct W) : Prop

A single disjunct is true iff its modal claim holds.

Possibility: ∃ w ∈ A, B(w). Necessity (and weak necessity, which still universally quantifies over a refined domain): ∀ w ∈ A, B(w).

Equations

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

@[implicit_reducible]

instance Geurts2005.Disjunct.decidableHolds {W : Type u_1} [Fintype W] (d : Disjunct W) [DecidablePred d.domain] [DecidablePred d.content] : Decidable d.holds

Equations

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

def Geurts2005.MDisjunction.holds {W : Type u_1} (disj : MDisjunction W) : Prop

A modal disjunction is true iff every disjunct's modal claim holds.

Equations

• disj.holds = ∀ d ∈ disj, d.holds

The three constraints (paper §3, p.395)

@[reducible]

def Geurts2005.Disjunct.cell {W : Type u_1} (d : Disjunct W) : Set W

The "modal cell" of a disjunct: worlds in both domain and content.

Equations

• d.cell = d.domain ∩ d.content

def Geurts2005.exhaustivity {W : Type u_1} (C : Set W) (disj : MDisjunction W) : Prop

Exhaustivity: C ⊆ ⋃(Aᵢ ∩ Bᵢ). Every background world falls in some disjunct's modal cell.

Equations

• Geurts2005.exhaustivity C disj = ∀ (w : W), C w → ∃ d ∈ disj, d.cell w

def Geurts2005.disjointness {W : Type u_1} (disj : MDisjunction W) : Prop

Disjointness (n-ary, paper p.395): distinct disjuncts have disjoint cells.

Equations

• Geurts2005.disjointness disj = List.Pairwise (fun (d₁ d₂ : Geurts2005.Disjunct W) => ∀ (w : W), ¬(d₁.cell w ∧ d₂.cell w)) disj

def Geurts2005.disjointness₂ {W : Type u_1} (d₁ d₂ : Disjunct W) : Prop

Disjointness₂ — binary specialisation used by the bridge theorems and the Case #3 worked example.

Equations

• Geurts2005.disjointness₂ d₁ d₂ = ∀ (w : W), ¬(d₁.cell w ∧ d₂.cell w)

theorem Geurts2005.disjointness_pair_iff {W : Type u_1} (d₁ d₂ : Disjunct W) : disjointness [d₁, d₂] ↔ disjointness₂ d₁ d₂

def Geurts2005.nonTriviality {W : Type u_1} (disj : MDisjunction W) : Prop

Non-triviality: Aᵢ ≠ ∅. Each modal domain is non-empty.

Equations

• Geurts2005.nonTriviality disj = ∀ d ∈ disj, ∃ (w : W), d.domain w

Key predictions

theorem Geurts2005.free_choice {W : Type u_1} (disj : MDisjunction W) (h_holds : disj.holds) (d : Disjunct W) (hd : d ∈ disj) : d.holds

Each disjunct's modal claim holds individually.

Immediate because Geurts's wide-scope LF (p.391) is the conjunction A₁M₁B₁ ∧ … ∧ AₙMₙBₙ from the outset: free choice "◇A ∧ ◇B follows" is a direct projection of one conjunct, not a structural inference from ◇(A∨B). The substantive move is the LF reanalysis, not this lemma.

theorem Geurts2005.disjointness_gives_exclusivity {W : Type u_1} (d₁ d₂ : Disjunct W) (h_dis : disjointness₂ d₁ d₂) (w : W) (h_in_1 : d₁.cell w) : ¬d₂.cell w

Disjointness gives the exclusive reading (paper §5, pp.402–404): exclusivity of 'or' is derived from Disjointness, not from a scalar implicature.

theorem Geurts2005.partition_unique {W : Type u_1} (C : Set W) (d₁ d₂ : Disjunct W) (h_exh : exhaustivity C [d₁, d₂]) (h_dis : disjointness₂ d₁ d₂) (w : W) (hw : C w) : (d₁.cell w ∨ d₂.cell w) ∧ ¬(d₁.cell w ∧ d₂.cell w)

Exhaustivity + Disjointness: every C-world lies in at most one cell.

The exhaustivity hypothesis is the upper bound (every C-world lies in some cell); together they yield exact partition of C across the two disjuncts.

Default domain binding (paper §3, p.394)

def Geurts2005.defaultBinding {W : Type u_1} (C : Set W) (content : List (Set W)) (f : Semantics.Modality.ModalForce) : MDisjunction W

Default domain binding: by default each modal domain equals the background C. The hearer tries A = C first and only restricts if the constraints force it (paper p.394: "the hearer first attempts to equate the quantifier domain with the background set").

Equations

• Geurts2005.defaultBinding C content f = List.map (fun (b : Set W) => { domain := C, force := f, content := b }) content

theorem Geurts2005.default_existential_holds_iff {W : Type u_1} (C : Set W) (bs : List (Set W)) : (defaultBinding C bs Semantics.Modality.ModalForce.possibility).holds ↔ ∀ b ∈ bs, ∃ (w : W), C w ∧ b w

With default binding and possibility force, truth is equivalent to: each disjunct's content is satisfied somewhere in C. The basic free-choice structure.

Specialisation to PartialProp

When presuppositions conflict, modal domains coincide with presuppositional domains and Geurts's disjunction specialises to PartialProp.orFlex. These lemmas are structural (the orFlex domain is defined as the union of disjunct presuppositions in Semantics/Presupposition/Basic.lean), not stipulated bridges.

def Geurts2005.fromPartialProp {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) : MDisjunction W

Construct a Geurts possibility disjunction from two presuppositional propositions: domains = presuppositions, contents = assertions.

Equations

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

theorem Geurts2005.fromPartialProp_presup_iff_orFlex {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) (w : W) : (∃ d ∈ fromPartialProp p q, d.domain w) ↔ (p.orFlex q).presup w

The overall presupposition of a Geurts disjunction from PartialProps coincides with PartialProp.orFlex.presup: p.presup ∨ q.presup.

theorem Geurts2005.fromPartialProp_cell_iff_orFlex {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) (w : W) : (∃ d ∈ fromPartialProp p q, d.cell w) ↔ (p.orFlex q).assertion w

The assertion side: Geurts cells = PartialProp.orFlex.assertion.

theorem Geurts2005.fromPartialProp_presup_iff_orBelnap {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) (w : W) : (∃ d ∈ fromPartialProp p q, d.domain w) ↔ (p.orBelnap q).presup w

Via the definitional identity orFlex = orBelnap: Geurts presupposition = orBelnap presupposition ([Bel70] conditional assertion).

theorem Geurts2005.fromPartialProp_cell_iff_orBelnap {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) (w : W) : (∃ d ∈ fromPartialProp p q, d.cell w) ↔ (p.orBelnap q).assertion w

Via the definitional identity orFlex = orBelnap: Geurts cell = orBelnap assertion.

theorem Geurts2005.exhaustivity_implies_uninformative {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) (C : Set W) (h_exh : exhaustivity C (fromPartialProp p q)) (w : W) (hw : C w) : (p.orFlex q).assertion w

If Geurts's exhaustivity holds for C, the disjunction (orFlex/orBelnap) is already true throughout C — the disjunction is uninformative.

The formal residue of [Sch09a]'s local-context-failure discussion: pragmatic conditions on local contexts force s₀ to contain only worlds where some disjunct is true, making the disjunction trivially satisfied. Geurts's Exhaustivity is the explicit form of that constraint. Consumed by Studies/Yagi2025.lean.

theorem Geurts2005.conflicting_presups_disjoint {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) (h_conflict : ∀ (w : W), ¬(p.presup w ∧ q.presup w)) : disjointness₂ { domain := p.presup, force := Semantics.Modality.ModalForce.possibility, content := p.assertion } { domain := q.presup, force := Semantics.Modality.ModalForce.possibility, content := q.assertion }

When presuppositions conflict (p ∧ q = ⊥), the Geurts domains are automatically disjoint — Disjointness is satisfied for free.

Worked example: paper §3 Case #3, "It must be here or it must be there"

Universal force; A ⊊ C and A' ⊊ C; the constraints force A∪A' = C (partition of C by the two modal domains, paper p.397).

inductive Geurts2005.Loc : Type

• here : Loc
• there : Loc
• elsewhere : Loc

@[implicit_reducible]

instance Geurts2005.instDecidableEqLoc : DecidableEq Loc

Equations

• Geurts2005.instDecidableEqLoc x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Geurts2005.instReprLoc : Repr Loc

Equations

• Geurts2005.instReprLoc = { reprPrec := Geurts2005.instReprLoc.repr }

def Geurts2005.instReprLoc.repr : Loc → ℕ → Std.Format

Equations

• Geurts2005.instReprLoc.repr Geurts2005.Loc.here prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Geurts2005.Loc.here")).group prec✝
• Geurts2005.instReprLoc.repr Geurts2005.Loc.there prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Geurts2005.Loc.there")).group prec✝
• Geurts2005.instReprLoc.repr Geurts2005.Loc.elsewhere prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Geurts2005.Loc.elsewhere")).group prec✝

@[implicit_reducible]

instance Geurts2005.instInhabitedLoc : Inhabited Loc

Equations

• Geurts2005.instInhabitedLoc = { default := Geurts2005.instInhabitedLoc.default }

@[implicit_reducible]

instance Geurts2005.instFintypeLoc : Fintype Loc

Equations

• Geurts2005.instFintypeLoc = { elems := { val := ↑Geurts2005.Loc.enumList, nodup := Geurts2005.Loc.enumList_nodup }, complete := Geurts2005.instFintypeLoc._proof_1 }

def Geurts2005.isHere : Set Loc

Equations

• Geurts2005.isHere Geurts2005.Loc.here = True
• Geurts2005.isHere w = False

def Geurts2005.isThere : Set Loc

Equations

• Geurts2005.isThere Geurts2005.Loc.there = True
• Geurts2005.isThere w = False

@[implicit_reducible]

instance Geurts2005.instDecidablePredLocIsHere : DecidablePred isHere

Equations

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

@[implicit_reducible]

instance Geurts2005.instDecidablePredLocIsThere : DecidablePred isThere

Equations

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

def Geurts2005.bgHereOrThere : Set Loc

Background C: it's either here or there (not elsewhere).

Equations

• Geurts2005.bgHereOrThere Geurts2005.Loc.here = True
• Geurts2005.bgHereOrThere Geurts2005.Loc.there = True
• Geurts2005.bgHereOrThere Geurts2005.Loc.elsewhere = False

@[implicit_reducible]

instance Geurts2005.instDecidablePredLocBgHereOrThere : DecidablePred bgHereOrThere

Equations

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

def Geurts2005.dHere : Disjunct Loc

Disjunct 1: ∀ over domain {here}, content {here}.

Equations

• Geurts2005.dHere = { domain := Geurts2005.isHere, force := Semantics.Modality.ModalForce.necessity, content := Geurts2005.isHere }

def Geurts2005.dThere : Disjunct Loc

Disjunct 2: ∀ over domain {there}, content {there}.

Equations

• Geurts2005.dThere = { domain := Geurts2005.isThere, force := Semantics.Modality.ModalForce.necessity, content := Geurts2005.isThere }

def Geurts2005.mustHereOrThere : MDisjunction Loc

"It must be here or it must be there" with domain restriction.

Equations

• Geurts2005.mustHereOrThere = [Geurts2005.dHere, Geurts2005.dThere]

theorem Geurts2005.mustHereOrThere_holds : mustHereOrThere.holds

theorem Geurts2005.mustHereOrThere_exhaustive : exhaustivity bgHereOrThere mustHereOrThere

theorem Geurts2005.mustHereOrThere_disjoint : disjointness₂ dHere dThere

theorem Geurts2005.must_here_not_entailed : ¬∀ (w : Loc), bgHereOrThere w → isHere w

"It must be here or it must be there" does NOT entail "it must be here" (paper p.397): "it does not follow from (27) that It must be here, nor does it follow that It must be there."

Worked example: paper §3 Case #1, "It may be here or it may be there"

Existential force; default A = A' = C.

def Geurts2005.mayHereOrThere : MDisjunction Loc

"It may be here or it may be there" with default domain binding.

Equations

• Geurts2005.mayHereOrThere = Geurts2005.defaultBinding Geurts2005.bgHereOrThere [Geurts2005.isHere, Geurts2005.isThere] Semantics.Modality.ModalForce.possibility

theorem Geurts2005.mayHereOrThere_holds : mayHereOrThere.holds

theorem Geurts2005.mayHereOrThere_fc_here : { domain := bgHereOrThere, force := Semantics.Modality.ModalForce.possibility, content := isHere }.holds

Free choice: ◇(here) holds individually.

theorem Geurts2005.mayHereOrThere_fc_there : { domain := bgHereOrThere, force := Semantics.Modality.ModalForce.possibility, content := isThere }.holds

Free choice: ◇(there) holds individually.