inductive Semantics.Modality.Disjunction.Force : Type

Modal force: existential (◇) or universal (□).

• existential : Force
• universal : Force

instance Semantics.Modality.Disjunction.instDecidableEqForce : DecidableEq Force

Equations

• Semantics.Modality.Disjunction.instDecidableEqForce x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Modality.Disjunction.instReprForce.repr : Force → ℕ → Std.Format

Equations

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

instance Semantics.Modality.Disjunction.instReprForce : Repr Force

Equations

• Semantics.Modality.Disjunction.instReprForce = { reprPrec := Semantics.Modality.Disjunction.instReprForce.repr }

structure Semantics.Modality.Disjunction.Disjunct (W : Type u_2) : Type u_2

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

• domain : BProp W

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

• force : Force

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

• content : BProp W

  Descriptive content Bᵢ.

@[reducible, inline]

abbrev Semantics.Modality.Disjunction.MDisjunction (W : Type u_2) : Type u_2

A modal disjunction: conjunction of modal propositions.

Equations

• Semantics.Modality.Disjunction.MDisjunction W = List (Semantics.Modality.Disjunction.Disjunct W)

def Semantics.Modality.Disjunction.Disjunct.holds {W : Type u_1} [Core.Proposition.FiniteWorlds W] (d : Disjunct W) : Bool

A single disjunct is true iff its modal claim holds. ◇: ∃w ∈ A, B(w). □: ∀w ∈ A, B(w).

Equations

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

def Semantics.Modality.Disjunction.MDisjunction.holds {W : Type u_1} [Core.Proposition.FiniteWorlds W] (disj : MDisjunction W) : Bool

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

Equations

• disj.holds = List.all disj fun (d : Semantics.Modality.Disjunction.Disjunct W) => d.holds

def Semantics.Modality.Disjunction.Disjunct.cell {W : Type u_1} (d : Disjunct W) : BProp W

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

Equations

• d.cell w = (d.domain w && d.content w)

def Semantics.Modality.Disjunction.exhaustivity {W : Type u_1} (C : BProp W) (disj : MDisjunction W) : Prop

Exhaustivity: C ⊆ ∪(Aᵢ ∩ Bᵢ). All background worlds are covered by some disjunct's modal cell.

Equations

• Semantics.Modality.Disjunction.exhaustivity C disj = ∀ (w : W), C w = true → (List.any disj fun (d : Semantics.Modality.Disjunction.Disjunct W) => d.cell w) = true

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

Disjointness for binary disjunctions: cells don't overlap. (Aᵢ ∩ Bᵢ) ∩ (Aⱼ ∩ Bⱼ) = ∅ for i ≠ j.

Equations

• Semantics.Modality.Disjunction.disjointness₂ d₁ d₂ = ∀ (w : W), ¬(d₁.cell w = true ∧ d₂.cell w = true)

def Semantics.Modality.Disjunction.nonTriviality {W : Type u_1} [Core.Proposition.FiniteWorlds W] (disj : MDisjunction W) : Prop

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

Equations

• Semantics.Modality.Disjunction.nonTriviality disj = ∀ d ∈ disj, Core.Proposition.FiniteWorlds.worlds.any d.domain = true

theorem Semantics.Modality.Disjunction.free_choice {W : Type u_1} [Core.Proposition.FiniteWorlds W] (disj : MDisjunction W) (h_holds : disj.holds = true) (d : Disjunct W) (hd : d ∈ disj) : d.holds = true

Free choice: for a modal disjunction, each disjunct's modal claim holds individually.

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.

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 = true) : d₂.cell w = false

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.

theorem Semantics.Modality.Disjunction.partition_unique {W : Type u_1} (C : BProp W) (d₁ d₂ : Disjunct W) (_h_exh : exhaustivity C [d₁, d₂]) (h_dis : disjointness₂ d₁ d₂) (w : W) (_hw : C w = true) (h1 : d₁.cell w = true) : d₂.cell w = false

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

def Semantics.Modality.Disjunction.defaultBinding {W : Type u_1} (C : BProp W) (content : List (BProp 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 : BProp W) => { domain := C, force := f, content := b }) content

theorem Semantics.Modality.Disjunction.default_existential_holds_iff {W : Type u_1} [Core.Proposition.FiniteWorlds W] (C : BProp W) (bs : List (BProp W)) : (defaultBinding C bs Force.existential).holds = bs.all fun (b : BProp W) => Core.Proposition.FiniteWorlds.worlds.any fun (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.

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.

theorem Semantics.Modality.Disjunction.fromPrProp_presup_eq_orFlex {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) : (List.any (fromPrProp p q) fun (d : Disjunct W) => 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.

theorem Semantics.Modality.Disjunction.fromPrProp_cell_eq_orFlex {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) : (List.any (fromPrProp p q) fun (d : Disjunct W) => 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).

theorem Semantics.Modality.Disjunction.conflicting_presups_disjoint {W : Type u_1} (p q : Core.Presupposition.PrProp W) (h_conflict : ∀ (w : W), ¬(p.presup w = true ∧ q.presup w = true)) : disjointness₂ { domain := p.presup, force := Force.existential, content := p.assertion } { domain := q.presup, force := Force.existential, content := q.assertion }

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

inductive Semantics.Modality.Disjunction.Loc : Type

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

instance Semantics.Modality.Disjunction.instDecidableEqLoc : DecidableEq Loc

Equations

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

instance Semantics.Modality.Disjunction.instReprLoc : Repr Loc

Equations

• Semantics.Modality.Disjunction.instReprLoc = { reprPrec := Semantics.Modality.Disjunction.instReprLoc.repr }

def Semantics.Modality.Disjunction.instReprLoc.repr : Loc → ℕ → Std.Format

Equations

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

instance Semantics.Modality.Disjunction.instInhabitedLoc : Inhabited Loc

Equations

• Semantics.Modality.Disjunction.instInhabitedLoc = { default := Semantics.Modality.Disjunction.instInhabitedLoc.default }

def Semantics.Modality.Disjunction.instInhabitedLoc.default : Loc

Equations

• Semantics.Modality.Disjunction.instInhabitedLoc.default = Semantics.Modality.Disjunction.Loc.here

instance Semantics.Modality.Disjunction.instFiniteWorldsLoc : Core.Proposition.FiniteWorlds Loc

Equations

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

def Semantics.Modality.Disjunction.isHere : BProp Loc

Equations

• Semantics.Modality.Disjunction.isHere Semantics.Modality.Disjunction.Loc.here = true
• Semantics.Modality.Disjunction.isHere x✝ = false

def Semantics.Modality.Disjunction.isThere : BProp Loc

Equations

• Semantics.Modality.Disjunction.isThere Semantics.Modality.Disjunction.Loc.there = true
• Semantics.Modality.Disjunction.isThere x✝ = false

def Semantics.Modality.Disjunction.bgHereOrThere : BProp Loc

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

Equations

• Semantics.Modality.Disjunction.bgHereOrThere Semantics.Modality.Disjunction.Loc.here = true
• Semantics.Modality.Disjunction.bgHereOrThere Semantics.Modality.Disjunction.Loc.there = true
• Semantics.Modality.Disjunction.bgHereOrThere Semantics.Modality.Disjunction.Loc.elsewhere = false

def Semantics.Modality.Disjunction.dHere : Disjunct Loc

Disjunct 1: □(here) over domain {here}.

Equations

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

def Semantics.Modality.Disjunction.dThere : Disjunct Loc

Disjunct 2: □(there) over domain {there}.

Equations

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

def Semantics.Modality.Disjunction.mustHereOrThere : MDisjunction Loc

"It must be here or it must be there" with domain restriction. Exhaustivity+Disjointness force A = {here}, A' = {there}.

Equations

• Semantics.Modality.Disjunction.mustHereOrThere = [Semantics.Modality.Disjunction.dHere, Semantics.Modality.Disjunction.dThere]

theorem Semantics.Modality.Disjunction.mustHereOrThere_holds : mustHereOrThere.holds = true

The disjunction holds: □(here) over {here} ∧ □(there) over {there}.

theorem Semantics.Modality.Disjunction.mustHereOrThere_exhaustive : exhaustivity bgHereOrThere mustHereOrThere

Exhaustivity: bgHereOrThere ⊆ {here} ∪ {there}.

theorem Semantics.Modality.Disjunction.mustHereOrThere_disjoint : disjointness₂ dHere dThere

Disjointness: {here} ∩ {there} = ∅.

theorem Semantics.Modality.Disjunction.must_here_not_entailed : (Core.Proposition.FiniteWorlds.worlds.all fun (w : Loc) => !bgHereOrThere w || isHere w) = false

Key prediction: "It must be here or it must be there" does NOT entail "it must be here". The necessity over the full background fails.

def Semantics.Modality.Disjunction.mayHereOrThere : MDisjunction Loc

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

Equations

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

theorem Semantics.Modality.Disjunction.mayHereOrThere_holds : mayHereOrThere.holds = true

The disjunction holds: ◇(here) w.r.t. C ∧ ◇(there) w.r.t. C.

theorem Semantics.Modality.Disjunction.mayHereOrThere_fc_here : { domain := bgHereOrThere, force := Force.existential, content := isHere }.holds = true

Free choice: ◇(here) holds individually.

theorem Semantics.Modality.Disjunction.mayHereOrThere_fc_there : { domain := bgHereOrThere, force := Force.existential, content := isThere }.holds = true

Free choice: ◇(there) holds individually.