Geurts (2005): Entertaining Alternatives: Disjunctions as Modals

This file formalizes Geurts's modal analysis of disjunction. "S₁ or … or Sₙ" is a conjunction of modal propositions AᵢMᵢBᵢ, each a domain Aᵢ drawn from a contextual background C, a force Mᵢ, and a descriptive content Bᵢ, constrained by Exhaustivity, Disjointness, and Non-triviality. Following Zimmermann, or merely presents a list of alternatives; unlike Zimmermann, an overt modal fuses with the covert one, and the context dependence of the domains does the work of the Self-Reflection Principle.

The case studies of section 3 are theorems about the constraints. Existential disjuncts bind their domains to the background by default, so each alternative is possible (holds_defaultBinding) and under Exhaustivity the background lies within the union of the contents (exhaustive_defaultBinding). Two universal disjuncts cannot both be bound to the background, since Disjointness and Non-triviality would fail together (not_disjoint_of_necessity); their domains partition it instead (partition_of_necessity) and neither "It must be here" nor "It must be there" follows (mustHereOrThere). In a mixed disjunction the universal disjunct's domain is the background minus the existential disjunct's content (domain_eq_diff), so the form with the universal disjunct first refers forward (rows_forward_reference). If-clauses restrict the domain of a covert necessity modal, as for Kratzer, so a disjunction of conditionals entails the disjunction of its consequents (consequents_of_conditionals), Woods's intuition against Johnson-Laird and Savary's illusory inference; and Disjointness yields the exclusive reading of section 5 (exclusive_of_disjoint).

Implementation notes

Force is the project's Modality.ModalForce; the paper's ∃ is possibility and its ∀ covers both necessities. The specialisation of the analysis to trivalent propositions lives in the study of the later paper that draws it, Studies/Yagi2025.lean.

References

• [Geu05]
• [Zim00]
• [Kra91]
• [Woo97a]
• [JLS99]

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

A modal proposition AMB consists of a domain, a modal force, and a descriptive content.

• domain : Set W
• force : Modality.ModalForce
• content : Set W

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

AMB holds when an existential domain meets the content and a universal one lies within it.

Equations

• d.Holds = if d.force = Modality.ModalForce.possibility then (d.domain ∩ d.content).Nonempty else d.domain ⊆ d.content

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

A disjunct entertains the worlds of its domain within its content.

Equations

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

theorem Geurts2005.Disjunct.holds_iff_nonempty {W : Type u_1} (d : Disjunct W) (h : d.force = Modality.ModalForce.possibility) : d.Holds ↔ (d.domain ∩ d.content).Nonempty

theorem Geurts2005.Disjunct.holds_iff_subset {W : Type u_1} (d : Disjunct W) (h : d.force ≠ Modality.ModalForce.possibility) : d.Holds ↔ d.domain ⊆ d.content

theorem Geurts2005.Disjunct.cell_eq_domain {W : Type u_1} (d : Disjunct W) (h : d.force ≠ Modality.ModalForce.possibility) (hd : d.Holds) : d.cell = d.domain

A universal disjunct that holds entertains exactly its domain.

@[reducible, inline]

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

The logical form of "S₁ or … or Sₙ" is a conjunction of modal propositions.

Equations

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

def Geurts2005.Disjunction.Holds {W : Type u_1} (ds : Disjunction W) : Prop

Every disjunct's modal claim holds.

Equations

• ds.Holds = ∀ d ∈ ds, d.Holds

def Geurts2005.Disjunction.Exhaustive {W : Type u_1} (C : Set W) (ds : Disjunction W) : Prop

Exhaustivity holds when the background lies within the union of the cells.

Equations

• Geurts2005.Disjunction.Exhaustive C ds = (C ⊆ ⋃ d ∈ ds, d.cell)

def Geurts2005.Disjunction.PairwiseDisjoint {W : Type u_1} (ds : Disjunction W) : Prop

Disjointness holds when distinct disjuncts have disjoint cells.

Equations

• ds.PairwiseDisjoint = List.Pairwise (Function.onFun Disjoint Geurts2005.Disjunct.cell) ds

def Geurts2005.Disjunction.Nontrivial {W : Type u_1} (ds : Disjunction W) : Prop

Non-triviality holds when every domain is nonempty.

Equations

• ds.Nontrivial = ∀ d ∈ ds, d.domain.Nonempty

def Geurts2005.Disjunction.defaultBinding {W : Type u_1} (C : Set W) (f : Modality.ModalForce) (bs : List (Set W)) : Disjunction W

Under default binding the hearer first equates every domain with the background.

Equations

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

theorem Geurts2005.holds_defaultBinding {W : Type u_1} (C : Set W) (bs : List (Set W)) : (Disjunction.defaultBinding C Modality.ModalForce.possibility bs).Holds ↔ ∀ b ∈ bs, (C ∩ b).Nonempty

Under default binding each alternative is possible in the background, and free choice is the projection of a conjunct (case 1).

theorem Geurts2005.exhaustive_defaultBinding {W : Type u_1} (C : Set W) (f : Modality.ModalForce) (bs : List (Set W)) : Disjunction.Exhaustive C (Disjunction.defaultBinding C f bs) ↔ C ⊆ ⋃ b ∈ bs, b

In case 1 Exhaustivity places the background within the union of the contents, so "It may be here or it may be there" says that it must be here or there.

theorem Geurts2005.not_disjoint_of_necessity {W : Type u_1} (C : Set W) {d d' : Disjunct W} (hf : d.force ≠ Modality.ModalForce.possibility) (hf' : d'.force ≠ Modality.ModalForce.possibility) (hd : d.Holds) (hd' : d'.Holds) (hC : d.domain = C) (hC' : d'.domain ⊆ C) (hne : d'.domain.Nonempty) : ¬Disjoint d.cell d'.cell

Two universal disjuncts cannot both be bound to the background (case 3). With one domain the background and the other within it, Disjointness and Non-triviality fail together.

theorem Geurts2005.partition_of_necessity {W : Type u_1} (C : Set W) {d d' : Disjunct W} (hf : d.force ≠ Modality.ModalForce.possibility) (hf' : d'.force ≠ Modality.ModalForce.possibility) (hd : d.Holds) (hd' : d'.Holds) (hex : Disjunction.Exhaustive C [d, d']) (hdis : Disjoint d.cell d'.cell) : C ⊆ d.domain ∪ d'.domain ∧ Disjoint d.domain d'.domain

Universal disjuncts that hold, exhaust the background, and have disjoint cells partition the background by their domains (case 3).

theorem Geurts2005.domain_eq_diff {W : Type u_1} (C : Set W) {d d' : Disjunct W} (hf' : d'.force ≠ Modality.ModalForce.possibility) (hd' : d'.Holds) (hC : d.domain = C) (hC' : d'.domain ⊆ C) (hex : Disjunction.Exhaustive C [d, d']) (hdis : Disjoint d.cell d'.cell) : d'.domain = C \ d.content

In "It may be here or else it must be there" (case 5) the existential disjunct is bound to the background and the universal disjunct's domain is the background minus the existential content, so the second domain is fixed by the first content.

def Geurts2005.conditional {W : Type u_1} (C A B : Set W) : Disjunct W

A conditional "if S₁ then S₂" against the background, whose if-clause restricts the domain of a covert necessity modal to the antecedent worlds ([Kra91]).

Equations

• Geurts2005.conditional C A B = { domain := C ∩ A, force := Modality.ModalForce.necessity, content := B }

theorem Geurts2005.conditional_holds_iff {W : Type u_1} (C A B : Set W) : (conditional C A B).Holds ↔ C ∩ A ⊆ B

theorem Geurts2005.exhaustive_conditionals_iff {W : Type u_1} (C : Set W) {A₁ B₁ A₂ B₂ : Set W} (h₁ : (conditional C A₁ B₁).Holds) (h₂ : (conditional C A₂ B₂).Holds) : Disjunction.Exhaustive C [conditional C A₁ B₁, conditional C A₂ B₂] ↔ C ⊆ A₁ ∪ A₂

For conditionals that hold, Exhaustivity is exhaustivity of the antecedents.

theorem Geurts2005.consequents_of_conditionals {W : Type u_1} (C : Set W) {A₁ B₁ A₂ B₂ : Set W} (h₁ : (conditional C A₁ B₁).Holds) (h₂ : (conditional C A₂ B₂).Holds) (hex : Disjunction.Exhaustive C [conditional C A₁ B₁, conditional C A₂ B₂]) : C ⊆ B₁ ∪ B₂

A disjunction of conditionals that holds and exhausts the background entails the disjunction of its consequents (section 4). This is [Woo97a]'s intuition about "Either he will stay in America if he is offered tenure or he will return to Europe if he isn't", and [JLS99]'s "illusory inference" to an ace in the hand.

theorem Geurts2005.exclusive_of_disjoint {W : Type u_1} (C : Set W) {A B B' : Set W} (hA : A ⊆ C) (h : Disjunction.Holds [{ domain := A, force := Modality.ModalForce.possibility, content := B }, { domain := C, force := Modality.ModalForce.possibility, content := B ∩ B' }]) (hex : Disjunction.Exhaustive C [{ domain := A, force := Modality.ModalForce.possibility, content := B }, { domain := C, force := Modality.ModalForce.possibility, content := B ∩ B' }]) (hdis : Disjoint (A ∩ B) (C ∩ (B ∩ B'))) : C ⊆ B ∧ (C ∩ B').Nonempty ∧ (C \ B').Nonempty

In "Gray is either a professor of law or a professor of law and a judge" (section 5), with the second domain the background and the first within it, Exhaustivity and Disjointness make every background world a B-world while B′ splits the background, so Gray must be a law professor and may or may not be a judge, an exclusive reading without a scalar implicature.

Case 3 does not entail either disjunct

inductive Geurts2005.Loc : Type

The two locations of "It must be here or it must be there".

• here : Loc
• there : Loc

@[instance_reducible]

instance Geurts2005.instDecidableEqLoc : DecidableEq Loc

Equations

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

def Geurts2005.mustHereOrThere : Disjunction Loc

Case 3 with the two-world background partitioned by the domains.

Equations

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

theorem Geurts2005.mustHereOrThere_holds : mustHereOrThere.Holds

theorem Geurts2005.mustHereOrThere_exhaustive : Disjunction.Exhaustive Set.univ mustHereOrThere

theorem Geurts2005.mustHereOrThere_pairwiseDisjoint : mustHereOrThere.PairwiseDisjoint

theorem Geurts2005.mustHereOrThere_nontrivial : mustHereOrThere.Nontrivial

theorem Geurts2005.not_must_here : ¬Set.univ ⊆ {Loc.here}

The disjunction holds and satisfies all three constraints, yet the background is not within the first content ("It does not follow from (27) that It must be here").

The orders of (1)–(2)

structure Geurts2005.Row : Type

An example of (1)–(2) records the forces of the two disjuncts, the flavour of the background, and the judgment.

• force₁ : Modality.ModalForce
• force₂ : Modality.ModalForce
• flavor : Modality.ModalFlavor
• judgment : Judgment

def Geurts2005.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Geurts2005.instDecidableEqRow : DecidableEq Row

Equations

• Geurts2005.instDecidableEqRow = Geurts2005.instDecidableEqRow.decEq

def Geurts2005.forces : List (String × Modality.ModalForce)

Equations

• Geurts2005.forces = [("may", Modality.ModalForce.possibility), ("must", Modality.ModalForce.necessity)]

def Geurts2005.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Geurts2005.rows : List Row

The deontic and epistemic disjunctions (1) and (2).

Equations

• Geurts2005.rows = List.filterMap Geurts2005.Row.ofDatum Geurts2005.Examples.all

def Geurts2005.ForwardReference (f₁ f₂ : Modality.ModalForce) : Prop

By domain_eq_diff the universal disjunct's domain is fixed by the existential disjunct's content; the dependence points forward when the universal disjunct comes first.

Equations

• Geurts2005.ForwardReference f₁ f₂ = (f₁ ≠ Modality.ModalForce.possibility ∧ f₂ = Modality.ModalForce.possibility)

@[instance_reducible]

instance Geurts2005.instDecidableRelModalForceForwardReference : DecidableRel ForwardReference

Equations

• Geurts2005.instDecidableRelModalForceForwardReference x✝¹ x✝ = id inferInstance

theorem Geurts2005.rows_forward_reference (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ ¬ForwardReference r.force₁ r.force₂)

A disjunction of modals is acceptable exactly when no domain refers forward, the paper's explanation of the odd "?It must be here or else it may be there" in (1)–(2).