inductive Semantics.Lexical.Verb.ChangeOfState.CoSType : Type

Classification of change-of-state verbs by the direction of state change.

• cessation: Activity ceases (stop, quit, cease, finish)

• Presupposes: P was happening

• Asserts: P is no longer happening

• Example: "stopped smoking" → was smoking, now isn't

• inception: Activity begins (start, begin, commence)

• Presupposes: P was NOT happening

• Asserts: P is now happening

• Example: "started smoking" → wasn't smoking, now is

• continuation: Activity persists (continue, keep, remain)

• Presupposes: P was happening

• Asserts: P is still happening

• Example: "continued smoking" → was smoking, still is

• cessation : CoSType
• inception : CoSType
• continuation : CoSType

instance Semantics.Lexical.Verb.ChangeOfState.instDecidableEqCoSType : DecidableEq CoSType

Equations

• Semantics.Lexical.Verb.ChangeOfState.instDecidableEqCoSType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Verb.ChangeOfState.instReprCoSType.repr : CoSType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.ChangeOfState.instReprCoSType : Repr CoSType

Equations

• Semantics.Lexical.Verb.ChangeOfState.instReprCoSType = { reprPrec := Semantics.Lexical.Verb.ChangeOfState.instReprCoSType.repr }

instance Semantics.Lexical.Verb.ChangeOfState.instBEqCoSType : BEq CoSType

Equations

• Semantics.Lexical.Verb.ChangeOfState.instBEqCoSType = { beq := Semantics.Lexical.Verb.ChangeOfState.instBEqCoSType.beq }

def Semantics.Lexical.Verb.ChangeOfState.instBEqCoSType.beq : CoSType → CoSType → Bool

Equations

• Semantics.Lexical.Verb.ChangeOfState.instBEqCoSType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Lexical.Verb.ChangeOfState.instInhabitedCoSType.default : CoSType

Equations

• Semantics.Lexical.Verb.ChangeOfState.instInhabitedCoSType.default = Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation

instance Semantics.Lexical.Verb.ChangeOfState.instInhabitedCoSType : Inhabited CoSType

Equations

• Semantics.Lexical.Verb.ChangeOfState.instInhabitedCoSType = { default := Semantics.Lexical.Verb.ChangeOfState.instInhabitedCoSType.default }

structure Semantics.Lexical.Verb.ChangeOfState.CoSEntry : Type

A lexical entry for a change-of-state verb.

Bundles:

• Surface form ("stop", "start", etc.)
• Change type (cessation, inception, continuation)
• Whether the state change is reversible (default: true)

The activity predicate P is NOT part of the entry — it's supplied compositionally.

• form : String

  Surface form

• cosType : CoSType

  Type of state change

• reversible : Bool

  Can the state change be undone? (stop → start → stop)

instance Semantics.Lexical.Verb.ChangeOfState.instReprCoSEntry : Repr CoSEntry

Equations

• Semantics.Lexical.Verb.ChangeOfState.instReprCoSEntry = { reprPrec := Semantics.Lexical.Verb.ChangeOfState.instReprCoSEntry.repr }

def Semantics.Lexical.Verb.ChangeOfState.instReprCoSEntry.repr : CoSEntry → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.ChangeOfState.instBEqCoSEntry : BEq CoSEntry

Equations

• Semantics.Lexical.Verb.ChangeOfState.instBEqCoSEntry = { beq := Semantics.Lexical.Verb.ChangeOfState.instBEqCoSEntry.beq }

def Semantics.Lexical.Verb.ChangeOfState.instBEqCoSEntry.beq : CoSEntry → CoSEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Lexical.Verb.ChangeOfState.instBEqCoSEntry.beq x✝¹ x✝ = false

def Semantics.Lexical.Verb.ChangeOfState.stop : CoSEntry

"stop" — cessation verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.stop = { form := "stop", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation }

def Semantics.Lexical.Verb.ChangeOfState.quit : CoSEntry

"quit" — cessation verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.quit = { form := "quit", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation }

def Semantics.Lexical.Verb.ChangeOfState.cease : CoSEntry

"cease" — cessation verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.cease = { form := "cease", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation }

def Semantics.Lexical.Verb.ChangeOfState.finish : CoSEntry

"finish" — cessation verb (often irreversible in context)

Equations

• Semantics.Lexical.Verb.ChangeOfState.finish = { form := "finish", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation, reversible := false }

def Semantics.Lexical.Verb.ChangeOfState.start : CoSEntry

"start" — inception verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.start = { form := "start", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.inception }

def Semantics.Lexical.Verb.ChangeOfState.begin_ : CoSEntry

"begin" — inception verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.begin_ = { form := "begin", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.inception }

def Semantics.Lexical.Verb.ChangeOfState.commence : CoSEntry

"commence" — inception verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.commence = { form := "commence", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.inception }

def Semantics.Lexical.Verb.ChangeOfState.continue_ : CoSEntry

"continue" — continuation verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.continue_ = { form := "continue", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation }

def Semantics.Lexical.Verb.ChangeOfState.keep : CoSEntry

"keep" — continuation verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.keep = { form := "keep", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation }

def Semantics.Lexical.Verb.ChangeOfState.remain : CoSEntry

"remain" — continuation verb

Equations

• Semantics.Lexical.Verb.ChangeOfState.remain = { form := "remain", cosType := Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation }

def Semantics.Lexical.Verb.ChangeOfState.priorStatePresup {W : Type u_1} (t : CoSType) (P : W → Bool) : W → Bool

The presupposition triggered by a CoS type, given the activity predicate P.

• cessation: presupposes P (the activity was happening)
• inception: presupposes ¬P (the activity wasn't happening)
• continuation: presupposes P (the activity was happening)

Equations

• Semantics.Lexical.Verb.ChangeOfState.priorStatePresup Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation P = P
• Semantics.Lexical.Verb.ChangeOfState.priorStatePresup Semantics.Lexical.Verb.ChangeOfState.CoSType.inception P = fun (w : W) => !P w
• Semantics.Lexical.Verb.ChangeOfState.priorStatePresup Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation P = P

def Semantics.Lexical.Verb.ChangeOfState.resultStateAssertion {W : Type u_1} (t : CoSType) (P : W → Bool) : W → Bool

The assertion made by a CoS type, given the activity predicate P.

• cessation: asserts ¬P (the activity is no longer happening)
• inception: asserts P (the activity is now happening)
• continuation: asserts P (the activity is still happening)

Equations

• Semantics.Lexical.Verb.ChangeOfState.resultStateAssertion Semantics.Lexical.Verb.ChangeOfState.CoSType.cessation P = fun (w : W) => !P w
• Semantics.Lexical.Verb.ChangeOfState.resultStateAssertion Semantics.Lexical.Verb.ChangeOfState.CoSType.inception P = P
• Semantics.Lexical.Verb.ChangeOfState.resultStateAssertion Semantics.Lexical.Verb.ChangeOfState.CoSType.continuation P = P

def Semantics.Lexical.Verb.ChangeOfState.cosSemantics {W : Type u_1} (t : CoSType) (P : W → Bool) : Core.Presupposition.PrProp W

Combined semantics of a CoS predicate as a presuppositional proposition.

Given an activity predicate P, returns a PrProp with:

• presupposition: the expected prior state
• assertion: the expected result state

This is the core semantic contribution: CoS predicates are presupposition triggers that constrain both the prior and current states.

Equations

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

def Semantics.Lexical.Verb.ChangeOfState.entrySemantics {W : Type u_1} (e : CoSEntry) (P : W → Bool) : Core.Presupposition.PrProp W

Semantics for a lexical entry applied to an activity predicate.

Equations

• Semantics.Lexical.Verb.ChangeOfState.entrySemantics e P = Semantics.Lexical.Verb.ChangeOfState.cosSemantics e.cosType P

theorem Semantics.Lexical.Verb.ChangeOfState.negation_preserves_presup {W : Type u_1} (t : CoSType) (P : W → Bool) : (cosSemantics t P).presup = (cosSemantics t P).neg.presup

Negation preserves presupposition (hole property).

"Mary didn't stop smoking" has the same presupposition as "Mary stopped smoking": both presuppose she was smoking.

This is a defining property of presupposition triggers and enables the classic test: if the presupposition projects through negation, it's a presupposition, not an entailment.

theorem Semantics.Lexical.Verb.ChangeOfState.cessation_inception_complementary {W : Type u_1} (P : W → Bool) (w : W) : priorStatePresup CoSType.cessation P w = !priorStatePresup CoSType.inception P w

Cessation and inception have complementary presuppositions.

• "stop P" presupposes P
• "start P" presupposes ¬P

These are exact complements: at any world, exactly one presupposition is satisfied.

theorem Semantics.Lexical.Verb.ChangeOfState.cessation_continuation_same_presup {W : Type u_1} (P : W → Bool) : priorStatePresup CoSType.cessation P = priorStatePresup CoSType.continuation P

Cessation and continuation have the same presupposition.

Both "stop P" and "continue P" presuppose that P was happening. The difference is only in the assertion about the result state.

theorem Semantics.Lexical.Verb.ChangeOfState.cessation_assertion_negates_presup {W : Type u_1} (P : W → Bool) (w : W) : resultStateAssertion CoSType.cessation P w = !priorStatePresup CoSType.cessation P w

For cessation, the assertion is the negation of the presupposition.

"stop P" presupposes P and asserts ¬P. This captures the change: from P being true to P being false.

theorem Semantics.Lexical.Verb.ChangeOfState.inception_assertion_negates_presup {W : Type u_1} (P : W → Bool) (w : W) : resultStateAssertion CoSType.inception P w = !priorStatePresup CoSType.inception P w

For inception, the assertion is the negation of the presupposition.

"start P" presupposes ¬P and asserts P. This captures the change: from P being false to P being true.

theorem Semantics.Lexical.Verb.ChangeOfState.continuation_assertion_equals_presup {W : Type u_1} (P : W → Bool) : resultStateAssertion CoSType.continuation P = priorStatePresup CoSType.continuation P

For continuation, the assertion equals the presupposition.

"continue P" presupposes P and asserts P. No change occurs; the predicate reports persistence.

def Semantics.Lexical.Verb.ChangeOfState.shiftsUnderBelief (_e : CoSEntry) : Bool

All CoS predicates shift under belief (@cite{tonhauser-beaver-roberts-simons-2013}: Class C).

The presupposition is attributed to the speaker by default, but shifts to a belief holder in embedded contexts:

"John believes Mary stopped smoking" → Presupposes that JOHN believes Mary was smoking (not the speaker)

This is captured by returning true for all entries.

Equations

• Semantics.Lexical.Verb.ChangeOfState.shiftsUnderBelief _e = true

def Semantics.Lexical.Verb.ChangeOfState.hasOLE (_e : CoSEntry) : Bool

All CoS predicates have OLE (Optional Local Effect) = yes.

The presupposition can be locally satisfied in conditionals and disjunctions:

"If Mary was smoking, she stopped" → No presupposition projects (locally satisfied by antecedent)

This is a defining characteristic of soft triggers.

Equations

• Semantics.Lexical.Verb.ChangeOfState.hasOLE _e = true

def Semantics.Lexical.Verb.ChangeOfState.hasSCF (_e : CoSEntry) : Bool

All CoS predicates have SCF (Strong Contextual Felicity) = no.

The presupposition need not be established in prior discourse:

A: "What's new with Mary?" B: "She stopped smoking." → Felicitous even though A didn't establish Mary smoked

This distinguishes soft triggers from hard triggers like "too".

Equations

• Semantics.Lexical.Verb.ChangeOfState.hasSCF _e = false