structure Semantics.Presupposition.OntologicalPreconditions.EventPhase (W : Type u_2) : Type u_2

An event decomposed into temporal phases:

1. Precondition: State that must hold BEFORE for the event to be possible
2. The event occurrence itself
3. Consequence: State that holds AFTER the event

• precondition : W → Bool

  Precondition: must hold before the event for it to be possible

• eventOccurs : W → Bool

  The event actually occurs

• consequence : W → Bool

  Consequence: holds after the event (result state)

def Semantics.Presupposition.OntologicalPreconditions.EventPhase.wellFormed {W : Type u_1} (e : EventPhase W) : Prop

Well-formed event: precondition enables the event.

This is the ontological constraint: you can't stop smoking unless you were smoking.

Equations

• e.wellFormed = ∀ (w : W), e.eventOccurs w = true → e.precondition w = true

def Semantics.Presupposition.OntologicalPreconditions.stopAsEventPhase {W : Type u_1} (P : W → Bool) : EventPhase W

"Stop P" as an event phase

Equations

• Semantics.Presupposition.OntologicalPreconditions.stopAsEventPhase P = { precondition := P, eventOccurs := P, consequence := fun (w : W) => !P w }

def Semantics.Presupposition.OntologicalPreconditions.startAsEventPhase {W : Type u_1} (P : W → Bool) : EventPhase W

"Start P" as an event phase

Equations

• Semantics.Presupposition.OntologicalPreconditions.startAsEventPhase P = { precondition := fun (w : W) => !P w, eventOccurs := fun (w : W) => !P w, consequence := P }

def Semantics.Presupposition.OntologicalPreconditions.continueAsEventPhase {W : Type u_1} (P : W → Bool) : EventPhase W

"Continue P" as an event phase

Equations

• Semantics.Presupposition.OntologicalPreconditions.continueAsEventPhase P = { precondition := P, eventOccurs := P, consequence := P }

theorem Semantics.Presupposition.OntologicalPreconditions.stop_precondition_is_presup {W : Type u_1} (P : W → Bool) : (stopAsEventPhase P).precondition = Lexical.Verb.ChangeOfState.priorStatePresup Lexical.Verb.ChangeOfState.CoSType.cessation P

Event phase precondition = CoS presupposition.

theorem Semantics.Presupposition.OntologicalPreconditions.start_precondition_is_presup {W : Type u_1} (P : W → Bool) : (startAsEventPhase P).precondition = Lexical.Verb.ChangeOfState.priorStatePresup Lexical.Verb.ChangeOfState.CoSType.inception P

theorem Semantics.Presupposition.OntologicalPreconditions.continue_precondition_is_presup {W : Type u_1} (P : W → Bool) : (continueAsEventPhase P).precondition = Lexical.Verb.ChangeOfState.priorStatePresup Lexical.Verb.ChangeOfState.CoSType.continuation P

theorem Semantics.Presupposition.OntologicalPreconditions.stop_consequence_is_assertion {W : Type u_1} (P : W → Bool) : (stopAsEventPhase P).consequence = Lexical.Verb.ChangeOfState.resultStateAssertion Lexical.Verb.ChangeOfState.CoSType.cessation P

Event phase consequence = CoS assertion.

theorem Semantics.Presupposition.OntologicalPreconditions.start_consequence_is_assertion {W : Type u_1} (P : W → Bool) : (startAsEventPhase P).consequence = Lexical.Verb.ChangeOfState.resultStateAssertion Lexical.Verb.ChangeOfState.CoSType.inception P

theorem Semantics.Presupposition.OntologicalPreconditions.continue_consequence_is_assertion {W : Type u_1} (P : W → Bool) : (continueAsEventPhase P).consequence = Lexical.Verb.ChangeOfState.resultStateAssertion Lexical.Verb.ChangeOfState.CoSType.continuation P

structure Semantics.Presupposition.OntologicalPreconditions.EventSentence (W : Type u_2) : Type u_2

A sentence that refers to an event type and makes a claim about it.

The event type referenced is independent of the claim made. Both affirmative and negative sentences can refer to the same event type.

• eventType : EventPhase W

  The event type this sentence is about

• polarity : Core.Polarity

  The polarity of the claim

def Semantics.Presupposition.OntologicalPreconditions.EventSentence.aboutness {W : Type u_1} (s : EventSentence W) : EventPhase W

The "aboutness" of a sentence: what event type it refers to.

This is independent of polarity: both "John stopped" and "John didn't stop" are about the same event type (the stopping).

Equations

• s.aboutness = s.eventType

def Semantics.Presupposition.OntologicalPreconditions.EventSentence.assertion {W : Type u_1} (s : EventSentence W) : W → Bool

The assertion made by a sentence depends on polarity.

• Affirmed: The event occurred (consequence holds)
• Negated: The event didn't occur (consequence doesn't hold)

Equations

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

def Semantics.Presupposition.OntologicalPreconditions.EventSentence.presupposition {W : Type u_1} (s : EventSentence W) : W → Bool

The presupposition comes from aboutness, not from the assertion.

Presuppositions are tied to event reference, not to the claim being made.

Equations

• s.presupposition = s.aboutness.precondition

def Semantics.Presupposition.OntologicalPreconditions.affirmative {W : Type u_1} (e : EventPhase W) : EventSentence W

Construct an affirmative sentence about an event type.

Equations

• Semantics.Presupposition.OntologicalPreconditions.affirmative e = { eventType := e, polarity := Core.Polarity.positive }

def Semantics.Presupposition.OntologicalPreconditions.negative {W : Type u_1} (e : EventPhase W) : EventSentence W

Construct a negative sentence about an event type.

Equations

• Semantics.Presupposition.OntologicalPreconditions.negative e = { eventType := e, polarity := Core.Polarity.negative }

theorem Semantics.Presupposition.OntologicalPreconditions.same_aboutness {W : Type u_1} (e : EventPhase W) : (affirmative e).aboutness = (negative e).aboutness

Affirmative and negative sentences have the same aboutness.

Both "John stopped smoking" and "John didn't stop smoking" are about the same event type, the stopping event. This is the structural basis for presupposition projection.

theorem Semantics.Presupposition.OntologicalPreconditions.presupposition_projects {W : Type u_1} (e : EventPhase W) : (affirmative e).presupposition = (negative e).presupposition

Presuppositions project because they come from shared aboutness.

Since presuppositions are derived from aboutness, and aboutness is shared across polarities, presuppositions must be shared too.

theorem Semantics.Presupposition.OntologicalPreconditions.assertion_differs {W : Type u_1} (e : EventPhase W) (w : W) : (negative e).assertion w = !(affirmative e).assertion w

Assertions differ by polarity.

While presuppositions are shared, assertions differ: the negative asserts the opposite of the affirmative.

theorem Semantics.Presupposition.OntologicalPreconditions.presupposition_independent_of_assertion {W : Type u_1} (s : EventSentence W) : s.presupposition = s.eventType.precondition

Presupposition is independent of assertion content.

The presupposition depends only on the event type, not on what is asserted. This is what makes presuppositions "backgrounded": they're part of what we're talking about, not what we're saying about it.

structure Semantics.Presupposition.OntologicalPreconditions.AssertionOnlyMeaning (W : Type u_2) : Type u_2

Under the assertion-only view, we just have truth conditions.

• truthConditions : W → Bool

def Semantics.Presupposition.OntologicalPreconditions.assertionOnly_stop {W : Type u_1} (P : W → Bool) : AssertionOnlyMeaning W

Under assertion-only, "stop P" just means: was P and now ¬P.

Without temporal indices, this collapses to P w ∧ ¬P w at a single world — always false. This demonstrates that purely extensional (single-index) semantics cannot represent CoS verbs: the pre-state and post-state refer to different temporal indices, and flattening them into one evaluation point produces a contradiction.

Equations

• Semantics.Presupposition.OntologicalPreconditions.assertionOnly_stop P = { truthConditions := fun (w : W) => P w && !P w }

def Semantics.Presupposition.OntologicalPreconditions.assertionOnly_notStop {W : Type u_1} (P : W → Bool) : AssertionOnlyMeaning W

Under assertion-only, "not stop P" just means: ¬(was P and now ¬P).

Equations

• Semantics.Presupposition.OntologicalPreconditions.assertionOnly_notStop P = { truthConditions := fun (w : W) => !(P w && !P w) }

theorem Semantics.Presupposition.OntologicalPreconditions.assertionOnly_no_presupposition {W : Type u_1} (P : W → Bool) (w : W) (_hNotP : P w = false) : (assertionOnly_notStop P).truthConditions w = true

Under assertion-only, the negation does not entail the precondition.

The negated assertion !(P w && !P w) = !P w ∨ P w is true when P w is false. So we cannot infer P from the negated sentence.

This demonstrates the inadequacy of the assertion-only view: it cannot explain why "John didn't stop smoking" presupposes he was smoking.

theorem Semantics.Presupposition.OntologicalPreconditions.aboutness_predicts_projection {W : Type u_1} (P : W → Bool) : (affirmative (stopAsEventPhase P)).presupposition = (negative (stopAsEventPhase P)).presupposition

Under the aboutness view, both sentences refer to the stopping event. The stopping event has precondition P (was smoking). Therefore, both sentences presuppose P.

theorem Semantics.Presupposition.OntologicalPreconditions.shared_presupposition_is_precondition {W : Type u_1} (P : W → Bool) : (affirmative (stopAsEventPhase P)).presupposition = P

The shared presupposition IS the precondition of the event type.

theorem Semantics.Presupposition.OntologicalPreconditions.stop_presupposes_P {W : Type u_1} (P : W → Bool) (pol : Core.Polarity) : { eventType := stopAsEventPhase P, polarity := pol }.presupposition = P

For "stop P", both affirmative and negative presuppose P.

This is the core empirical prediction that the aboutness view explains and the assertion-only view cannot.

def Semantics.Presupposition.OntologicalPreconditions.EventPhase.hasConsequence {W : Type u_1} (e : EventPhase W) : Prop

Consequential event: the event entails its consequence when it occurs.

Equations

• e.hasConsequence = ∀ (w : W), e.eventOccurs w = true → e.consequence w = true

theorem Semantics.Presupposition.OntologicalPreconditions.consequence_requires_occurrence {W : Type u_1} (e : EventPhase W) (h : e.hasConsequence) (w : W) (hOccur : e.eventOccurs w = true) : e.consequence w = true

Consequences do not project through negation.

Under "not E", the event didn't occur, so we can't infer the consequence. This explains why "John didn't stop smoking" doesn't entail he's not smoking.

The asymmetry:

• Preconditions: tied to event reference, so they project
• Consequences: tied to event occurrence, so they don't project under negation

theorem Semantics.Presupposition.OntologicalPreconditions.structural_asymmetry {W : Type u_1} (e : EventPhase W) (p : Core.Polarity) : { eventType := e, polarity := p }.presupposition = e.precondition

Structural explanation: why preconditions project and consequences don't.

1. Presupposition = aboutness.precondition (comes from event reference)
2. Assertion = depends on polarity (comes from claim about occurrence)
3. Consequence = entailed by occurrence (part of assertion, not aboutness)

Under negation:

• Event reference is preserved → presupposition preserved
• Occurrence is denied → consequence not entailed

theorem Semantics.Presupposition.OntologicalPreconditions.assertions_differ_at_definite_worlds {W : Type u_1} (e : EventPhase W) (w : W) : (negative e).assertion w = !(affirmative e).assertion w

Assertions differ at any world where the consequence is definite (true or false).

If the consequence is true at w, affirmative says true and negative says false. If the consequence is false at w, affirmative says false and negative says true.

theorem Semantics.Presupposition.OntologicalPreconditions.presupposition_constant_assertion_varies {W : Type u_1} (e : EventPhase W) (w : W) : (affirmative e).presupposition w = (negative e).presupposition w ∧ (negative e).assertion w = !(affirmative e).assertion w

Presuppositions are constant across polarity; assertions vary with polarity.

Presuppositions are tied to event reference (which is constant), not to the claim (which varies).

theorem Semantics.Presupposition.OntologicalPreconditions.negation_preserves_precondition_denies_consequence {W : Type u_1} (e : EventPhase W) (w : W) : (negative e).presupposition w = e.precondition w ∧ (negative e).assertion w = !e.consequence w

The precondition/consequence asymmetry under negation.

Under negation, precondition content survives (via presupposition) but consequence content is denied (via assertion). This is the structural basis for why preconditions are the default accommodation target (@cite{roberts-simons-2024} p. 721): accommodating preconditions is consistent with both affirming and denying the event, while accommodating consequences is only consistent with affirmation.

theorem Semantics.Presupposition.OntologicalPreconditions.affirmation_preserves_precondition_asserts_consequence {W : Type u_1} (e : EventPhase W) (w : W) : (affirmative e).presupposition w = e.precondition w ∧ (affirmative e).assertion w = e.consequence w

The converse: under affirmation, precondition survives AND consequence is asserted. Preconditions are consistent with BOTH polarities; consequences are consistent with only one.

def Semantics.Presupposition.OntologicalPreconditions.EventPhase.isTelic {W : Type u_1} (e : EventPhase W) : Prop

An event is telic if its consequence differs from its precondition.

This is the existential property: there exists some world where precondition ≠ consequence, indicating a state change.

Equations

• e.isTelic = ∃ (w : W), e.precondition w ≠ e.consequence w

def Semantics.Presupposition.OntologicalPreconditions.EventPhase.isAtelic {W : Type u_1} (e : EventPhase W) : Prop

An event is atelic if precondition and consequence are the same.

This is the universal property: in all worlds, the state persists.

Equations

• e.isAtelic = ∀ (w : W), e.precondition w = e.consequence w

theorem Semantics.Presupposition.OntologicalPreconditions.stop_is_telic {W : Type u_1} (P : W → Bool) (w : W) (hP : P w = true) : (stopAsEventPhase P).precondition w ≠ (stopAsEventPhase P).consequence w

"Stop P" is telic: state changes from P to ¬P

theorem Semantics.Presupposition.OntologicalPreconditions.continue_is_atelic {W : Type u_1} (P : W → Bool) : (continueAsEventPhase P).isAtelic

"Continue P" is atelic: no state change

theorem Semantics.Presupposition.OntologicalPreconditions.start_is_telic {W : Type u_1} (P : W → Bool) (w : W) (hNotP : P w = false) : (startAsEventPhase P).precondition w ≠ (startAsEventPhase P).consequence w

"Start P" is telic: state changes from ¬P to P

def Semantics.Presupposition.OntologicalPreconditions.cosTypeToAspectualProfile : Lexical.Verb.ChangeOfState.CoSType → Tense.Aspect.LexicalAspect.AspectualProfile

Aspectual profile for CoS verb types.

• "stop": Achievement profile (telic, punctual change to ¬P)
• "start": Achievement profile (telic, punctual change to P)
• "continue": Activity profile (atelic, durative persistence)

Equations

• Semantics.Presupposition.OntologicalPreconditions.cosTypeToAspectualProfile Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation = Semantics.Tense.Aspect.LexicalAspect.achievementProfile
• Semantics.Presupposition.OntologicalPreconditions.cosTypeToAspectualProfile Semantics.Lexical.Verb.ChangeOfState.CoSType.inception = Semantics.Tense.Aspect.LexicalAspect.achievementProfile
• Semantics.Presupposition.OntologicalPreconditions.cosTypeToAspectualProfile Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation = Semantics.Tense.Aspect.LexicalAspect.activityProfile

def Semantics.Presupposition.OntologicalPreconditions.cosTypeToVendlerClass (t : Lexical.Verb.ChangeOfState.CoSType) : Tense.Aspect.LexicalAspect.VendlerClass

CoS verbs have specific Vendler classifications (derived from profile).

Equations

• Semantics.Presupposition.OntologicalPreconditions.cosTypeToVendlerClass t = (Semantics.Presupposition.OntologicalPreconditions.cosTypeToAspectualProfile t).toVendlerClass

theorem Semantics.Presupposition.OntologicalPreconditions.cessation_is_achievement : cosTypeToVendlerClass Lexical.Verb.ChangeOfState.CoSType.cessation = Tense.Aspect.LexicalAspect.VendlerClass.achievement

Cessation is classified as achievement (telic, punctual).

theorem Semantics.Presupposition.OntologicalPreconditions.continuation_is_activity : cosTypeToVendlerClass Lexical.Verb.ChangeOfState.CoSType.continuation = Tense.Aspect.LexicalAspect.VendlerClass.activity

Continuation is classified as activity (atelic, durative).

theorem Semantics.Presupposition.OntologicalPreconditions.cos_vendler_telicity_correct (t : Lexical.Verb.ChangeOfState.CoSType) : (cosTypeToVendlerClass t).telicity = match t with | Lexical.Verb.ChangeOfState.CoSType.cessation => Tense.Aspect.LexicalAspect.Telicity.telic | Lexical.Verb.ChangeOfState.CoSType.inception => Tense.Aspect.LexicalAspect.Telicity.telic | Lexical.Verb.ChangeOfState.CoSType.continuation => Tense.Aspect.LexicalAspect.Telicity.atelic

The Vendler class determines the telicity correctly.

inductive Semantics.Presupposition.OntologicalPreconditions.EntailmentRelation : Type

Classification of entailment relations between a sentence and its implied content (@cite{roberts-simons-2024} §2.1).

• precondition : EntailmentRelation

  Temporally prior, enables the event. Projects by pragmatic default.

• consequence : EntailmentRelation

  Temporally posterior, results from the event. At-issue.

• concomitant : EntailmentRelation

  Mereological part or co-occurring state. At-issue. Example: "Jane shouted" entails "Jane made sound" — the sound-making is part of the shouting, not a precondition for it.

instance Semantics.Presupposition.OntologicalPreconditions.instDecidableEqEntailmentRelation : DecidableEq EntailmentRelation

Equations

• Semantics.Presupposition.OntologicalPreconditions.instDecidableEqEntailmentRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Presupposition.OntologicalPreconditions.instReprEntailmentRelation : Repr EntailmentRelation

Equations

• Semantics.Presupposition.OntologicalPreconditions.instReprEntailmentRelation = { reprPrec := Semantics.Presupposition.OntologicalPreconditions.instReprEntailmentRelation.repr }

def Semantics.Presupposition.OntologicalPreconditions.instReprEntailmentRelation.repr : EntailmentRelation → ℕ → Std.Format

Equations

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

def Semantics.Presupposition.OntologicalPreconditions.instBEqEntailmentRelation.beq : EntailmentRelation → EntailmentRelation → Bool

Equations

• Semantics.Presupposition.OntologicalPreconditions.instBEqEntailmentRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Presupposition.OntologicalPreconditions.instBEqEntailmentRelation : BEq EntailmentRelation

Equations

• Semantics.Presupposition.OntologicalPreconditions.instBEqEntailmentRelation = { beq := Semantics.Presupposition.OntologicalPreconditions.instBEqEntailmentRelation.beq }

def Semantics.Presupposition.OntologicalPreconditions.EntailmentRelation.projects : EntailmentRelation → Bool

Only precondition entailments project by pragmatic default.

Equations

• Semantics.Presupposition.OntologicalPreconditions.EntailmentRelation.precondition.projects = true
• Semantics.Presupposition.OntologicalPreconditions.EntailmentRelation.consequence.projects = false
• Semantics.Presupposition.OntologicalPreconditions.EntailmentRelation.concomitant.projects = false

def Semantics.Presupposition.OntologicalPreconditions.knowAsEventPhase {W : Type u_1} (BEL C : W → Bool) : EventPhase W

"Know C" as an event phase: stative, atelic. Precondition: C is true. The knowing state cannot exist without its object. The state persists without change, so consequence = precondition = C.

Equations

• Semantics.Presupposition.OntologicalPreconditions.knowAsEventPhase BEL C = { precondition := C, eventOccurs := fun (w : W) => BEL w && C w, consequence := C }

def Semantics.Presupposition.OntologicalPreconditions.discoverAsEventPhase {W : Type u_1} (IGNORANT C : W → Bool) : EventPhase W

"Discover C" as an event phase: telic, achievement. Two preconditions: C is true AND the agent was previously ignorant. The discovery transitions from ignorance to knowledge. Consequence: C is (still) true and the agent is no longer ignorant.

Equations

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

def Semantics.Presupposition.OntologicalPreconditions.regretAsEventPhase {W : Type u_1} (BEL : W → Bool) : EventPhase W

"Regret p" as an event phase: emotive factive. Precondition: agent believes p (the emotion ontologically depends on the belief, not on truth directly).

@cite{roberts-simons-2024} (p. 731): regret's factivity arises from a pragmatic default to veridicality — in the absence of an explicit claim that the agent is mistaken, emotive attitudes are taken to be veridical. The ontological precondition is belief, not truth.

Equations

• Semantics.Presupposition.OntologicalPreconditions.regretAsEventPhase BEL = { precondition := BEL, eventOccurs := BEL, consequence := BEL }

theorem Semantics.Presupposition.OntologicalPreconditions.know_is_atelic {W : Type u_1} (BEL C : W → Bool) : (knowAsEventPhase BEL C).isAtelic

Know is atelic: no state change (precondition = consequence).

theorem Semantics.Presupposition.OntologicalPreconditions.discover_is_telic {W : Type u_1} (IGNORANT C : W → Bool) (w : W) (hC : C w = true) (hIgn : IGNORANT w = true) : (discoverAsEventPhase IGNORANT C).precondition w ≠ (discoverAsEventPhase IGNORANT C).consequence w

Discover is telic: state change from ignorant to knowing.

theorem Semantics.Presupposition.OntologicalPreconditions.factive_precondition_entails_complement {W : Type u_1} (IGNORANT C : W → Bool) (w : W) : (discoverAsEventPhase IGNORANT C).precondition w = true → C w = true

Both know and discover have C as (part of) their precondition. This is the shared factivity: complement truth is ontologically required.

theorem Semantics.Presupposition.OntologicalPreconditions.discover_precondition_requires_ignorance {W : Type u_1} (IGNORANT C : W → Bool) (w : W) : (discoverAsEventPhase IGNORANT C).precondition w = true → IGNORANT w = true

Discover's precondition additionally requires prior ignorance. This extra precondition (ignorance of C) explains why discover has weaker projection than know in conditional antecedents: in "If I discover p", the speaker's ignorance of p is salient, suppressing projection of C (@cite{roberts-simons-2024} §3.2.2).

theorem Semantics.Presupposition.OntologicalPreconditions.continue_has_precondition_without_state_change {W : Type u_1} (P : W → Bool) : (continueAsEventPhase P).precondition = P ∧ (continueAsEventPhase P).isAtelic

Continue has a precondition (prior activity) but involves NO state change. @cite{roberts-simons-2024} (p. 734): "continue V-ing is atelic, without a pre-state" in the CoS sense. The CoSType.continuation classification is a convenience; the key structural fact is isAtelic.

def Semantics.Presupposition.OntologicalPreconditions.selectionalEventPhase {W : Type u_1} (requirement event : W → Bool) : EventPhase W

A selectional restriction as an event phase. The requirement is an ontological precondition of the event.

Equations

• Semantics.Presupposition.OntologicalPreconditions.selectionalEventPhase requirement event = { precondition := requirement, eventOccurs := event, consequence := event }

theorem Semantics.Presupposition.OntologicalPreconditions.selectional_wellFormed {W : Type u_1} (requirement event : W → Bool) (h : ∀ (w : W), event w = true → requirement w = true) : (selectionalEventPhase requirement event).wellFormed

Selectional restrictions are well-formed: the event entails the requirement.

theorem Semantics.Presupposition.OntologicalPreconditions.selectional_projects {W : Type u_1} (requirement event : W → Bool) : (affirmative (selectionalEventPhase requirement event)).presupposition = (negative (selectionalEventPhase requirement event)).presupposition

Selectional restrictions project through negation (same aboutness mechanism).

inductive Semantics.Presupposition.OntologicalPreconditions.SuppressionCondition : Type

Conditions under which projection of a precondition is suppressed. When any of these obtains, the hearer does not accommodate the precondition into the global context.

• preconditionKnownFalse : SuppressionCondition

  Interlocutors know or believe the precondition is false or controversial. Example: discussing politics with someone who denies the premise. (@cite{roberts-simons-2024} ex. 23)

• speakerNonCommitment : SuppressionCondition

  Evidence that the speaker does not believe the precondition. Example: "I doubt that. Mary would divorce him if she discovered he was drinking." — speaker explicitly doubts the drinking. (@cite{roberts-simons-2024} ex. 24)

• preconditionAtIssue : SuppressionCondition

  The precondition is at-issue (currently under discussion). Example: "Is there a decision on Jane's tenure case?" "She isn't aware that there's been a decision." — decision existence is QUD. (@cite{roberts-simons-2024} ex. 25)

instance Semantics.Presupposition.OntologicalPreconditions.instDecidableEqSuppressionCondition : DecidableEq SuppressionCondition

Equations

• Semantics.Presupposition.OntologicalPreconditions.instDecidableEqSuppressionCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Presupposition.OntologicalPreconditions.instReprSuppressionCondition.repr : SuppressionCondition → ℕ → Std.Format

Equations

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

instance Semantics.Presupposition.OntologicalPreconditions.instReprSuppressionCondition : Repr SuppressionCondition

Equations

• Semantics.Presupposition.OntologicalPreconditions.instReprSuppressionCondition = { reprPrec := Semantics.Presupposition.OntologicalPreconditions.instReprSuppressionCondition.repr }

def Semantics.Presupposition.OntologicalPreconditions.instBEqSuppressionCondition.beq : SuppressionCondition → SuppressionCondition → Bool

Equations

• Semantics.Presupposition.OntologicalPreconditions.instBEqSuppressionCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Presupposition.OntologicalPreconditions.instBEqSuppressionCondition : BEq SuppressionCondition

Equations

• Semantics.Presupposition.OntologicalPreconditions.instBEqSuppressionCondition = { beq := Semantics.Presupposition.OntologicalPreconditions.instBEqSuppressionCondition.beq }

def Semantics.Presupposition.OntologicalPreconditions.SuppressionCondition.globalProjection : SuppressionCondition → Bool

When suppression applies, precondition content is merely locally entailed, not globally accommodated. The content is still an entailment of the trigger — it simply isn't taken to be part of the speaker's presumptions.

Equations

• x✝.globalProjection = false