Wang (2025): Presupposition, Competition, and Coherence

Wang's dissertation explains when a presupposition trigger of Mandarin is obligatory and when it is dropped by a competition between the presuppositional sentence and its non-presuppositional alternative, a sentence with the same assertion that is obtained by deleting or replacing the trigger. Three constraints decide the competition, ranked in this order. Internal Coherence requires the utterance to be consistent with the common ground, Felicity Presupposition requires a presupposition to be entailed by it, and Maximize Presupposition, after Heim, bars a form that has a presuppositionally stronger alternative. An utterance commits the speaker to a set of information states and a context admits a set of them, so coherence is overlap, and the context entails a proposition when every state it admits believes the proposition.

Main statements

• obligatory_of_entailed, omitted_of_not_entailed: the trigger is obligatory where the context entails its presupposition and dropped where the context is silent about it.
• obligatory_of_positive_evidence, omitted_of_denied, omitted_of_ignorance: against the exhaustified alternative the trigger is obligatory under positive evidence for the presupposition, and dropped where the context denies it or the speaker is ignorant of it.
• presup_beats_of_mp_over_fp: were Maximize Presupposition ranked above Felicity Presupposition, every trigger with an alternative would be obligatory.
• notNow_two_maxima, optional_of_two_readings: the alternative of buzai 'no longer' has two exhaustified readings, and the trigger is optional because it loses on one and wins on the other.

Implementation notes

• Information states are nonempty sets of worlds; the belief operator K p is the set of states included in p, and possibility and ignorance are the corresponding overlap conditions.
• Maximize Presupposition is blocking, Competition.Blocked. A sentence without a presupposition violates it in every context, as in the dissertation's tableaux, and its rank below Felicity Presupposition confines its effect to contexts that entail the presupposition.
• The aspectual triggers take their meanings from Presupposition.again and Aspect.Phasal.denote, with the earlier time, a free variable of the dissertation's entries, existentially closed.
• Trigger lists the lexical rows of Table 4.1 without its cleft row. The experiments of Chapters 3 and 5 and the de re and postsupposition analyses of Chapters 5 and 6 are not represented.

References

• [Wan25a]
• [Kat07]
• [Hei91]

Information states, commitments and contexts

def Wang2025.K {W : Type u_1} (p : Set W) : Set (Set W)

K p is the set of nonempty information states included in p, those in which the speaker believes p.

Equations

• Wang2025.K p = {s : Set W | s.Nonempty ∧ s ⊆ p}

def Wang2025.Poss {W : Type u_1} (p : Set W) : Set (Set W)

Poss p is the set of states meeting p, those in which the speaker holds p possible.

Equations

• Wang2025.Poss p = {s : Set W | (s ∩ p).Nonempty}

def Wang2025.Ignorant {W : Type u_1} (p : Set W) : Set (Set W)

Ignorant p is the set of states in which p and its negation are both possible.

Equations

• Wang2025.Ignorant p = Wang2025.Poss p ∩ Wang2025.Poss pᶜ

structure Wang2025.Candidate (W : Type u_2) : Type u_2

A candidate is an utterance in the competition, given by the states its use commits the speaker to and by its presupposition if it has one.

• commitment : Set (Set W)
• presup : Option (Set W)

def Wang2025.presupSentence {W : Type u_1} (p a : Set W) : Candidate W

The presuppositional sentence with presupposition p and assertion a commits the speaker to both.

Equations

• Wang2025.presupSentence p a = { commitment := Wang2025.K (p ∩ a), presup := some p }

def Wang2025.plain {W : Type u_1} (a : Set W) : Candidate W

The unexhaustified non-presuppositional alternative commits the speaker to a.

Equations

• Wang2025.plain a = { commitment := Wang2025.K a, presup := none }

def Wang2025.plainExhBelowK {W : Type u_1} (a q : Set W) : Candidate W

The alternative exhaustified against q below the belief operator commits the speaker to a and to the negation of q.

Equations

• Wang2025.plainExhBelowK a q = { commitment := Wang2025.K (a ∩ qᶜ), presup := none }

def Wang2025.plainExhAboveK {W : Type u_1} (a q : Set W) : Candidate W

The alternative exhaustified against q above the belief operator commits the speaker to a while the speaker does not believe q.

Equations

• Wang2025.plainExhAboveK a q = { commitment := Wang2025.K a \ Wang2025.K q, presup := none }

The constraints and their ranking, (3)

def Wang2025.ViolIC {W : Type u_1} (ctx : Set (Set W)) (c : Candidate W) : Prop

Internal Coherence is violated when the commitment excludes every admissible state.

Equations

• Wang2025.ViolIC ctx c = Disjoint ctx c.commitment

def Wang2025.ViolFP {W : Type u_1} (ctx : Set (Set W)) (c : Candidate W) : Prop

Felicity Presupposition is violated by a presuppositional sentence whose presupposition the context does not entail.

Equations

• Wang2025.ViolFP ctx c = ∃ (p : Set W), c.presup = some p ∧ ¬ctx ⊆ Wang2025.K p

def Wang2025.Candidate.admits {W : Type u_1} (c : Candidate W) : Set (Set (Set W))

A context admits a candidate when every admissible state believes its presupposition, if it has one.

Equations

• c.admits = {ctx : Set (Set W) | ∀ (p : Set W), c.presup = some p → ctx ⊆ Wang2025.K p}

theorem Wang2025.Candidate.admits_of_presup_none {W : Type u_1} {c : Candidate W} (h : c.presup = none) : c.admits = Set.univ

theorem Wang2025.Candidate.admits_of_presup_some {W : Type u_1} {c : Candidate W} {p : Set W} (h : c.presup = some p) : c.admits = {ctx : Set (Set W) | ctx ⊆ K p}

theorem Wang2025.Candidate.admits_ssubset_univ {W : Type u_1} {c : Candidate W} {p : Set W} (h : c.presup = some p) : c.admits ⊂ Set.univ

A presuppositional candidate is admitted by fewer contexts than a plain one, since the context {∅} admits no presupposition.

def Wang2025.ViolMP {W : Type u_1} (rival c : Candidate W) : Prop

Maximize Presupposition is violated by a candidate that its rival blocks, the rival being presuppositionally stronger, admitted by strictly fewer contexts, (3c).

Equations

• Wang2025.ViolMP rival c = Competition.Blocked (fun (x : Wang2025.Candidate W) => {rival}) Wang2025.Candidate.admits c

theorem Wang2025.violMP_iff {W : Type u_1} {rival c : Candidate W} : ViolMP rival c ↔ rival.admits ⊂ c.admits

theorem Wang2025.violMP_of_presup_none {W : Type u_1} {rival c : Candidate W} {p : Set W} (hc : c.presup = none) (hr : rival.presup = some p) : ViolMP rival c

A candidate without a presupposition violates Maximize Presupposition against a presuppositional rival, whatever the context.

theorem Wang2025.not_violMP_self {W : Type u_1} (c : Candidate W) : ¬ViolMP c c

def Wang2025.Beats {W : Type u_1} : List (Candidate W → Prop) → Candidate W → Candidate W → Prop

Beats cs a b compares two candidates by strict domination along the list cs of violation predicates, a beating b at the first constraint on which they differ.

Equations

• Wang2025.Beats [] x✝¹ x✝ = False
• Wang2025.Beats (C :: cs) x✝¹ x✝ = (¬C x✝¹ ∧ C x✝ ∨ (C x✝¹ ↔ C x✝) ∧ Wang2025.Beats cs x✝¹ x✝)

def Wang2025.ranking {W : Type u_1} (ctx : Set (Set W)) (sp : Candidate W) : List (Candidate W → Prop)

The ranking Internal Coherence ≫ Felicity Presupposition ≫ Maximize Presupposition, evaluated for the competition between sp and its alternative.

Equations

• Wang2025.ranking ctx sp = [Wang2025.ViolIC ctx, Wang2025.ViolFP ctx, Wang2025.ViolMP sp]

@[simp]

theorem Wang2025.violFP_presupSentence {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} : ViolFP ctx (presupSentence p a) ↔ ¬ctx ⊆ K p

A presuppositional sentence violates Felicity Presupposition exactly when the context does not entail its presupposition. A trigger without an alternative, such as jiu 'only', enters no competition, so this alone bars it from every context short of entailing the presupposition.

The three decisive facts

theorem Wang2025.presup_beats_of_incoherent {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} {c : Candidate W} (hsp : ¬Disjoint ctx (K (p ∩ a))) (hc : Disjoint ctx c.commitment) : Beats (ranking ctx (presupSentence p a)) (presupSentence p a) c

A coherent presuppositional sentence beats an incoherent alternative.

theorem Wang2025.plain_beats_of_not_entailed {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} {c : Candidate W} (hc0 : c.presup = none) (hsp : ¬Disjoint ctx (K (p ∩ a))) (hc : ¬Disjoint ctx c.commitment) (hp : ¬ctx ⊆ K p) : Beats (ranking ctx (presupSentence p a)) c (presupSentence p a)

A coherent alternative beats a presuppositional sentence whose presupposition is not entailed, when both are coherent.

theorem Wang2025.presup_beats_of_entailed {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} {c : Candidate W} (hc0 : c.presup = none) (hsp : ¬Disjoint ctx (K (p ∩ a))) (hc : ¬Disjoint ctx c.commitment) (hp : ctx ⊆ K p) : Beats (ranking ctx (presupSentence p a)) (presupSentence p a) c

A presuppositional sentence whose presupposition is entailed beats a coherent non-presuppositional alternative.

Felicity Presupposition above Maximize Presupposition

theorem Wang2025.presup_beats_of_mp_over_fp {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} {c : Candidate W} (hc0 : c.presup = none) (hsp : ¬Disjoint ctx (K (p ∩ a))) (hc : ¬Disjoint ctx c.commitment) : Beats [ViolIC ctx, ViolMP (presupSentence p a), ViolFP ctx] (presupSentence p a) c

Were Maximize Presupposition ranked above Felicity Presupposition, a coherent presuppositional sentence would beat a coherent alternative whatever the context entails, so every trigger with an alternative would be obligatory.

The tableaux

theorem Wang2025.obligatory_of_entailed {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} (hp : ctx ⊆ K p) (hwit : ∃ s ∈ ctx, s ⊆ a) : Beats (ranking ctx (presupSentence p a)) (presupSentence p a) (plain a)

In Table 4.2 the context entails the presupposition, so the trigger is obligatory.

theorem Wang2025.omitted_of_not_entailed {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} (hp : ¬ctx ⊆ K p) (hwit : ∃ s ∈ ctx, s.Nonempty ∧ s ⊆ p ∩ a) : Beats (ranking ctx (presupSentence p a)) (plain a) (presupSentence p a)

In Table 4.3 the context does not entail the presupposition, so the trigger is dropped.

theorem Wang2025.obligatory_of_positive_evidence {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} (hposs : ctx ⊆ Poss p) (hwit : ∃ s ∈ ctx, s.Nonempty ∧ s ⊆ p ∩ a) : Beats (ranking ctx (presupSentence p a)) (presupSentence p a) (plainExhBelowK a p)

In Table 4.4, with positive evidence for the presupposition and the alternative exhaustified below the belief operator, the exhaustive implicature contradicts the context and the trigger is obligatory, although its presupposition is not entailed.

theorem Wang2025.omitted_of_denied {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} (hneg : ctx ⊆ K pᶜ) (hwit : ∃ s ∈ ctx, s ⊆ a) : Beats (ranking ctx (presupSentence p a)) (plainExhBelowK a p) (presupSentence p a)

In Table 4.5 the context denies the presupposition, so the presuppositional sentence is incoherent and the alternative wins.

theorem Wang2025.omitted_of_ignorance {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} (hign : ctx ⊆ Ignorant p) (hwit : ∃ s ∈ ctx, s ⊆ a) : Beats (ranking ctx (presupSentence p a)) (plainExhAboveK a p) (presupSentence p a)

In Table 4.6, an ignorance context with the alternative exhaustified above the belief operator, the presuppositional sentence commits the speaker to the presupposition and so contradicts the ignorance, while the alternative is coherent; the trigger is dropped.

theorem Wang2025.optional_of_two_readings {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} (hposs : ctx ⊆ Poss p) (hp : ¬ctx ⊆ K p) (hwit : ∃ s ∈ ctx, s.Nonempty ∧ s ⊆ p ∩ a) : Beats (ranking ctx (presupSentence p a)) (plainExhBelowK a pᶜ) (presupSentence p a) ∧ Beats (ranking ctx (presupSentence p a)) (presupSentence p a) (plainExhBelowK a p)

In Tables 4.7 and 4.9 the context gives positive evidence for the presupposition without entailing it, and the alternative has two exhaustified readings. Exhaustified against the failure of the presupposition, so that it conveys that the presupposition holds, the alternative wins. Exhaustified against the presupposition, it loses, so the trigger is optional.

theorem Wang2025.obligatory_of_entailed_of_two_readings {W : Type u_1} {ctx : Set (Set W)} {p a : Set W} (hp : ctx ⊆ K p) (hwit : ∃ s ∈ ctx, s ⊆ a) : Beats (ranking ctx (presupSentence p a)) (presupSentence p a) (plainExhBelowK a pᶜ) ∧ Beats (ranking ctx (presupSentence p a)) (presupSentence p a) (plainExhBelowK a p)

In Tables 4.8 and 4.10 the context entails the presupposition, and the trigger wins on both readings of the alternative.

The alternative structure of the triggers, Table 4.1

inductive Wang2025.AltStructure : Type

A trigger's non-presuppositional alternative is obtained by deleting the trigger, by replacing it, or not at all.

• deletion : AltStructure
• replacement : AltStructure
• none : AltStructure

@[instance_reducible]

instance Wang2025.instDecidableEqAltStructure : DecidableEq AltStructure

Equations

• Wang2025.instDecidableEqAltStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Wang2025.instReprAltStructure : Repr AltStructure

Equations

• Wang2025.instReprAltStructure = { reprPrec := Wang2025.instReprAltStructure.repr }

def Wang2025.instReprAltStructure.repr : AltStructure → ℕ → Std.Format

Equations

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

inductive Wang2025.Trigger : Type

The lexical triggers of Table 4.1 are the adverbs ye 'also', fan'er 'instead', reng 'still', you and zai 'again', buzai 'no longer' and jiu 'only', and the verbs kaishi 'start', zhidao 'know' and houhui 'regret'.

• ye : Trigger
• faner : Trigger
• reng : Trigger
• you : Trigger
• zai : Trigger
• kaishi : Trigger
• buzai : Trigger
• zhidao : Trigger
• jiu : Trigger
• houhui : Trigger

@[instance_reducible]

instance Wang2025.instDecidableEqTrigger : DecidableEq Trigger

Equations

• Wang2025.instDecidableEqTrigger x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wang2025.instReprTrigger.repr : Trigger → ℕ → Std.Format

Equations

• Wang2025.instReprTrigger.repr Wang2025.Trigger.ye prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.ye")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.faner prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.faner")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.reng prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.reng")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.you prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.you")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.zai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.zai")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.kaishi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.kaishi")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.buzai prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.buzai")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.zhidao prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.zhidao")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.jiu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.jiu")).group prec✝
• Wang2025.instReprTrigger.repr Wang2025.Trigger.houhui prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Trigger.houhui")).group prec✝

@[instance_reducible]

instance Wang2025.instReprTrigger : Repr Trigger

Equations

• Wang2025.instReprTrigger = { reprPrec := Wang2025.instReprTrigger.repr }

def Wang2025.Trigger.entry : Trigger → Presupposition.TriggerItem ⊕ Mandarin.Verb

The fragment entry of a trigger, an adverb or a verb.

Equations

• Wang2025.Trigger.ye.entry = Sum.inl Mandarin.Adverbs.ye
• Wang2025.Trigger.faner.entry = Sum.inl Mandarin.Adverbs.faner
• Wang2025.Trigger.reng.entry = Sum.inl Mandarin.Adverbs.reng
• Wang2025.Trigger.you.entry = Sum.inl Mandarin.Adverbs.you
• Wang2025.Trigger.zai.entry = Sum.inl Mandarin.Adverbs.zai
• Wang2025.Trigger.buzai.entry = Sum.inl Mandarin.Adverbs.buzai
• Wang2025.Trigger.jiu.entry = Sum.inl Mandarin.Adverbs.jiu
• Wang2025.Trigger.kaishi.entry = Sum.inr Mandarin.kaishi
• Wang2025.Trigger.zhidao.entry = Sum.inr Mandarin.zhidao
• Wang2025.Trigger.houhui.entry = Sum.inr Mandarin.houhui

def Wang2025.Trigger.altStructure : Trigger → AltStructure

Table 4.1. A trigger whose assertion is its prejacent deletes, as the additive, contrastive, continuative, repetitive and inchoative ones do. The cessative and the factive replace, buzai by negation and zhidao by renwei 'believe'. No sequence of deletions and replacements yields a sentence with the assertion of jiu 'only' or of houhui 'regret', which have no alternative.

Equations

• Wang2025.Trigger.ye.altStructure = Wang2025.AltStructure.deletion
• Wang2025.Trigger.faner.altStructure = Wang2025.AltStructure.deletion
• Wang2025.Trigger.reng.altStructure = Wang2025.AltStructure.deletion
• Wang2025.Trigger.you.altStructure = Wang2025.AltStructure.deletion
• Wang2025.Trigger.zai.altStructure = Wang2025.AltStructure.deletion
• Wang2025.Trigger.kaishi.altStructure = Wang2025.AltStructure.deletion
• Wang2025.Trigger.buzai.altStructure = Wang2025.AltStructure.replacement
• Wang2025.Trigger.zhidao.altStructure = Wang2025.AltStructure.replacement
• Wang2025.Trigger.jiu.altStructure = Wang2025.AltStructure.none
• Wang2025.Trigger.houhui.altStructure = Wang2025.AltStructure.none

theorem Wang2025.isTrigger_of_entry {t : Trigger} {v : Mandarin.Verb} (h : t.entry = Sum.inr v) : v.IsTrigger

The verbal triggers are presupposition triggers by their fragment entries.

theorem Wang2025.not_isTrigger_renwei : ¬Mandarin.renwei.IsTrigger

The replacement for zhidao is non-presuppositional, as (1) requires, since renwei 'believe' is not a trigger.

The aspectual triggers

The repetitive you and zai, (12), the continuative reng, (24), the inchoative kaishi, (38), and the cessative buzai, (19), relate their prejacent at the index of evaluation to the prejacent at an earlier index, presupposing that it held or failed then and asserting that it holds or fails now.

def Wang2025.Candidate.ofTrivalent {W : Type u_1} (φ : W → SignType) : Candidate W

The candidate for a sentence with the trivalent meaning φ commits the speaker to its presupposition, where φ is defined, and to its assertion, where φ is true.

Equations

• Wang2025.Candidate.ofTrivalent φ = Wang2025.presupSentence (Function.support φ) (Trivalent.posExt φ)

theorem Wang2025.Candidate.ofTrivalent_eq_presupSentence {W : Type u_1} {φ : W → SignType} {a : Set W} (h : ∀ (w : W), φ w ≠ 0 → (φ w = 1 ↔ w ∈ a)) : ofTrivalent φ = presupSentence (Function.support φ) a

A sentence that asserts a wherever its meaning is defined is the presuppositional sentence with that presupposition and the assertion a.

noncomputable def Wang2025.Trigger.aspectual {W : Type u_1} (R S : SetRel W W) (P : W → Prop) : Trigger → Option (W → SignType)

The meaning of an aspectual trigger with the prejacent P. R relates an index to the earlier ones, the < of (12), and S relates an index to the earlier index of (19), (24) and (38), a relation the dissertation writes ∞. The meaning of kaishi is that of the phasal class of its fragment entry, and the other triggers of Table 4.1 are not aspectual.

Equations

• Wang2025.Trigger.aspectual R S P Wang2025.Trigger.you = some (Presupposition.again R P)
• Wang2025.Trigger.aspectual R S P Wang2025.Trigger.zai = some (Presupposition.again R P)
• Wang2025.Trigger.aspectual R S P Wang2025.Trigger.reng = some (Aspect.Phasal.continuation.denote S P)
• Wang2025.Trigger.aspectual R S P Wang2025.Trigger.buzai = some (Aspect.Phasal.cessation.denote S P)
• Wang2025.Trigger.aspectual R S P Wang2025.Trigger.kaishi = Option.map (fun (x : Aspect.Phasal) => x.denote S P) Mandarin.kaishi.phasal
• Wang2025.Trigger.aspectual R S P x✝ = none

theorem Wang2025.eq_one_iff_of_altStructure_deletion {W : Type u_1} {R S : SetRel W W} {P : W → Prop} {t : Trigger} {φ : W → SignType} (h : Trigger.aspectual R S P t = some φ) (ht : t.altStructure = AltStructure.deletion) {w : W} (hw : φ w ≠ 0) : φ w = 1 ↔ P w

An aspectual trigger whose alternative is obtained by deletion asserts its prejacent, so the sentence without the trigger makes the same assertion, as (1) requires of the alternative.

theorem Wang2025.eq_one_iff_buzai {W : Type u_1} {R S : SetRel W W} {P : W → Prop} {φ : W → SignType} (h : Trigger.aspectual R S P Trigger.buzai = some φ) {w : W} (hw : φ w ≠ 0) : φ w = 1 ↔ ¬P w

Buzai asserts the negation of its prejacent, so its alternative replaces it by negation.

theorem Wang2025.aspectual_obligatory_of_entailed {W : Type u_1} {R S : SetRel W W} {P : W → Prop} {ctx : Set (Set W)} {t : Trigger} {φ : W → SignType} (h : Trigger.aspectual R S P t = some φ) (ht : t.altStructure = AltStructure.deletion) (hp : ctx ⊆ K (Function.support φ)) (hwit : ∃ s ∈ ctx, s ⊆ {w : W | P w}) : Beats (ranking ctx (Candidate.ofTrivalent φ)) (Candidate.ofTrivalent φ) (plain {w : W | P w})

A sentence with an aspectual trigger that asserts its prejacent is obligatory, against the sentence without the trigger, when the context entails its presupposition, as in Table 4.2.

theorem Wang2025.aspectual_omitted_of_not_entailed {W : Type u_1} {R S : SetRel W W} {P : W → Prop} {ctx : Set (Set W)} {t : Trigger} {φ : W → SignType} (h : Trigger.aspectual R S P t = some φ) (ht : t.altStructure = AltStructure.deletion) (hp : ¬ctx ⊆ K (Function.support φ)) (hwit : ∃ s ∈ ctx, s.Nonempty ∧ s ⊆ Function.support φ ∩ {w : W | P w}) : Beats (ranking ctx (Candidate.ofTrivalent φ)) (plain {w : W | P w}) (Candidate.ofTrivalent φ)

A sentence with an aspectual trigger that asserts its prejacent loses to the sentence without the trigger when the context does not entail its presupposition, as in Table 4.3.

Exhaustification by maximal consistent subsets, (20) and (24)

def Wang2025.exhMx {W : Type u_1} [DecidableEq W] (φ : Finset W) (M : Finset (Finset W)) : Finset W

The reading of (24) for the maximal subset M is φ with every member of M negated.

Equations

• Wang2025.exhMx φ M = {w ∈ φ | ∀ q ∈ M, w ∉ q}

theorem Wang2025.exhIE_eq_exhMx_of_unique {W : Type u_1} [DecidableEq W] {φ : Finset W} {alts M₀ : Finset (Finset W)} (h₀ : Exhaustification.IsMaximalExclusion alts φ M₀) (huniq : ∀ (M : Finset (Finset W)), Exhaustification.IsMaximalExclusion alts φ M → M = M₀) : Exhaustification.exhIE (Exhaustification.asSetOfSets alts) ↑φ = ↑(exhMx φ M₀)

When the maximal consistent subset is unique, innocent exclusion, the operator of (20), and the operator of (24) agree, (25).

@[reducible, inline]

abbrev Wang2025.PQ : Type

The worlds of the disjunction example (26) are the pairs of truth values of p and q.

Equations

• Wang2025.PQ = (Bool × Bool)

def Wang2025.pAlt : Finset PQ

The alternative p of (26).

Equations

• Wang2025.pAlt = {x : Wang2025.PQ | x.1 = true}

def Wang2025.qAlt : Finset PQ

The alternative q of (26).

Equations

• Wang2025.qAlt = {x : Wang2025.PQ | x.2 = true}

theorem Wang2025.disjunction_two_maxima : Exhaustification.IsMaximalExclusion {pAlt, qAlt, pAlt ∩ qAlt} (pAlt ∪ qAlt) {pAlt, pAlt ∩ qAlt} ∧ Exhaustification.IsMaximalExclusion {pAlt, qAlt, pAlt ∩ qAlt} (pAlt ∪ qAlt) {qAlt, pAlt ∩ qAlt} ∧ exhMx (pAlt ∪ qAlt) {pAlt, pAlt ∩ qAlt} = qAlt \ pAlt ∧ exhMx (pAlt ∪ qAlt) {qAlt, pAlt ∩ qAlt} = pAlt \ qAlt

The disjunction p ∨ q with the alternatives p, q and p ∧ q, (26), has two maximal consistent subsets, yielding the readings q ∧ ¬p and p ∧ ¬q.

def Wang2025.cell (past now : Bool) : Finset PQ

The cell of (48) in which the state held in the past iff past and holds now iff now, a world being the pair of the two truth values.

Equations

• Wang2025.cell past now = {(past, now)}

def Wang2025.cells : Finset (Finset PQ)

The alternatives of (48), the four cells.

Equations

• Wang2025.cells = {Wang2025.cell false true, Wang2025.cell true false, Wang2025.cell true true, Wang2025.cell false false}

def Wang2025.notNow : Finset PQ

The prejacent of (46), that the state does not hold now, the alternative of a sentence with buzai 'no longer'.

Equations

• Wang2025.notNow = {x : Wang2025.PQ | x.2 = false}

theorem Wang2025.notNow_two_maxima : Exhaustification.IsMaximalExclusion cells notNow {cell false true, cell true true, cell false false} ∧ Exhaustification.IsMaximalExclusion cells notNow {cell false true, cell true false, cell true true} ∧ exhMx notNow {cell false true, cell true true, cell false false} = cell true false ∧ exhMx notNow {cell false true, cell true false, cell true true} = cell false false

The alternative of buzai has the two maximal consistent subsets of (49), on which it means that the state held in the past and that it did not.