Linglib.Theories.Semantics.Modality.Disjunction

Geurts §3 Case #1/2: "It may be here or it may be there" → each individual "may" claim holds. This is immediate from the structure: the disjunction IS a conjunction of modal claims.

source

theorem Semantics.Modality.Disjunction.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 exclusive reading.

If cells are disjoint and world w is in cell 1, it is not in cell 2. This is Geurts §5: exclusive 'or' from Disjointness, NOT scalar implicature.

source

theorem Semantics.Modality.Disjunction.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) (h1 : d₁.cell w) :

¬d₂.cell w

Exhaustivity + Disjointness → each C-world in exactly one cell.

source

def Semantics.Modality.Disjunction.defaultBinding {W : Type u_1} (C : Set W) (content : List (Set W)) (f : Force) :

MDisjunction W

Default domain binding: by default, each modal domain equals the background C. The hearer tries A = C first, and only restricts if constraints force it (Geurts p. 394).

Equations

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

Instances For

source

theorem Semantics.Modality.Disjunction.default_existential_holds_iff {W : Type u_1} (C : Set W) (bs : List (Set W)) :

(defaultBinding C bs Force.existential).holds ↔ ∀ b ∈ bs, ∃ (w : W), C w ∧ b w

With default binding and existential force, truth = each disjunct is possible w.r.t. C. This is the basic free choice structure.

source

def Semantics.Modality.Disjunction.fromPrProp {W : Type u_1} (p q : Core.Presupposition.PrProp W) :

MDisjunction W

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

Equations

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

Instances For

source

theorem Semantics.Modality.Disjunction.fromPrProp_presup_iff_orFlex {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) :

(∃ d ∈ fromPrProp p q, d.domain w) ↔ (p.orFlex q).presup w

The overall presupposition of a Geurts disjunction from PrProps is p.presup ∨ q.presup — matching PrProp.orFlex.

source

theorem Semantics.Modality.Disjunction.fromPrProp_cell_iff_orFlex {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) :

(∃ d ∈ fromPrProp p q, d.cell w) ↔ (p.orFlex q).assertion w

The assertion of a Geurts disjunction from PrProps matches orFlex: (p.presup ∧ p.assertion) ∨ (q.presup ∧ q.assertion).

source

theorem Semantics.Modality.Disjunction.fromPrProp_presup_iff_orBelnap {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) :

(∃ d ∈ fromPrProp p q, d.domain w) ↔ (p.orBelnap q).presup w

The three-way equivalence: Geurts (modal conjunction) = PrProp.orBelnap (conditional assertion, @cite{belnap-1970}). Transitivity via fromPrProp_presup_iff_orFlex + orFlex_eq_orBelnap.

source

theorem Semantics.Modality.Disjunction.fromPrProp_cell_iff_orBelnap {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) :

(∃ d ∈ fromPrProp p q, d.cell w) ↔ (p.orBelnap q).assertion w

The three-way equivalence (assertion side): Geurts cell = orBelnap assertion = orFlex assertion.

source

theorem Semantics.Modality.Disjunction.exhaustivity_implies_uninformative {W : Type u_1} (p q : Core.Presupposition.PrProp W) (C : Set W) (h_exh : exhaustivity C (fromPrProp p q)) (w : W) (hw : C w) :

(p.orFlex q).assertion w

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

This captures the essence of @cite{schlenker-2009}'s local context failure (@cite{yagi-2025} §2.4): the pragmatic condition on local contexts forces s₀ to contain only worlds where some disjunct is true, making the disjunction trivially satisfied. Geurts's exhaustivity constraint makes this explicit: it IS the constraint that contexts must be covered by disjunct cells.

source