inductive Features.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

@[implicit_reducible]

instance Features.ChangeOfState.instDecidableEqCoSType : DecidableEq CoSType

Equations

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

def Features.ChangeOfState.instReprCoSType.repr : CoSType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.ChangeOfState.instReprCoSType : Repr CoSType

Equations

• Features.ChangeOfState.instReprCoSType = { reprPrec := Features.ChangeOfState.instReprCoSType.repr }

@[implicit_reducible]

instance Features.ChangeOfState.instInhabitedCoSType : Inhabited CoSType

Equations

• Features.ChangeOfState.instInhabitedCoSType = { default := Features.ChangeOfState.instInhabitedCoSType.default }

def Features.ChangeOfState.instInhabitedCoSType.default : CoSType

Equations

• Features.ChangeOfState.instInhabitedCoSType.default = Features.ChangeOfState.CoSType.cessation

structure Features.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)

def Features.ChangeOfState.instReprCoSEntry.repr : CoSEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.ChangeOfState.instReprCoSEntry : Repr CoSEntry

Equations

• Features.ChangeOfState.instReprCoSEntry = { reprPrec := Features.ChangeOfState.instReprCoSEntry.repr }

@[implicit_reducible]

instance Features.ChangeOfState.instBEqCoSEntry : BEq CoSEntry

Equations

• Features.ChangeOfState.instBEqCoSEntry = { beq := Features.ChangeOfState.instBEqCoSEntry.beq }

def Features.ChangeOfState.instBEqCoSEntry.beq : CoSEntry → CoSEntry → Bool

Equations

• Features.ChangeOfState.instBEqCoSEntry.beq { form := a, cosType := a_1, reversible := a_2 } { form := b, cosType := b_1, reversible := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Features.ChangeOfState.instBEqCoSEntry.beq x✝¹ x✝ = false

def Features.ChangeOfState.stop : CoSEntry

"stop" — cessation verb

Equations

• Features.ChangeOfState.stop = { form := "stop", cosType := Features.ChangeOfState.CoSType.cessation }

def Features.ChangeOfState.quit : CoSEntry

"quit" — cessation verb

Equations

• Features.ChangeOfState.quit = { form := "quit", cosType := Features.ChangeOfState.CoSType.cessation }

def Features.ChangeOfState.cease : CoSEntry

"cease" — cessation verb

Equations

• Features.ChangeOfState.cease = { form := "cease", cosType := Features.ChangeOfState.CoSType.cessation }

def Features.ChangeOfState.finish : CoSEntry

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

Equations

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

def Features.ChangeOfState.start : CoSEntry

"start" — inception verb

Equations

• Features.ChangeOfState.start = { form := "start", cosType := Features.ChangeOfState.CoSType.inception }

def Features.ChangeOfState.begin_ : CoSEntry

"begin" — inception verb

Equations

• Features.ChangeOfState.begin_ = { form := "begin", cosType := Features.ChangeOfState.CoSType.inception }

def Features.ChangeOfState.commence : CoSEntry

"commence" — inception verb

Equations

• Features.ChangeOfState.commence = { form := "commence", cosType := Features.ChangeOfState.CoSType.inception }

def Features.ChangeOfState.continue_ : CoSEntry

"continue" — continuation verb

Equations

• Features.ChangeOfState.continue_ = { form := "continue", cosType := Features.ChangeOfState.CoSType.continuation }

def Features.ChangeOfState.keep : CoSEntry

"keep" — continuation verb

Equations

• Features.ChangeOfState.keep = { form := "keep", cosType := Features.ChangeOfState.CoSType.continuation }

def Features.ChangeOfState.remain : CoSEntry

"remain" — continuation verb

Equations

• Features.ChangeOfState.remain = { form := "remain", cosType := Features.ChangeOfState.CoSType.continuation }

def Features.ChangeOfState.priorStatePresup {W : Type u_1} (t : CoSType) (P : W → Prop) : W → Prop

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

• Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.cessation P = P
• Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.inception P = fun (w : W) => ¬P w
• Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.continuation P = P

def Features.ChangeOfState.resultStateAssertion {W : Type u_1} (t : CoSType) (P : W → Prop) : W → Prop

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

• Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.cessation P = fun (w : W) => ¬P w
• Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.inception P = P
• Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.continuation P = P

def Features.ChangeOfState.cosSemantics {W : Type u_1} (t : CoSType) (P : W → Prop) : 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

• Features.ChangeOfState.cosSemantics t P = { presup := Features.ChangeOfState.priorStatePresup t P, assertion := Features.ChangeOfState.resultStateAssertion t P }

def Features.ChangeOfState.entrySemantics {W : Type u_1} (e : CoSEntry) (P : W → Prop) : Core.Presupposition.PrProp W

Semantics for a lexical entry applied to an activity predicate.

Equations

• Features.ChangeOfState.entrySemantics e P = Features.ChangeOfState.cosSemantics e.cosType P

theorem Features.ChangeOfState.negation_preserves_presup {W : Type u_1} (t : CoSType) (P : W → Prop) : (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 Features.ChangeOfState.cessation_inception_complementary {W : Type u_1} (P : W → Prop) (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, the cessation presupposition holds iff the inception presupposition fails.

theorem Features.ChangeOfState.cessation_continuation_same_presup {W : Type u_1} (P : W → Prop) : 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 Features.ChangeOfState.cessation_assertion_negates_presup {W : Type u_1} (P : W → Prop) (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 Features.ChangeOfState.inception_assertion_negates_presup {W : Type u_1} (P : W → Prop) (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 Features.ChangeOfState.continuation_assertion_equals_presup {W : Type u_1} (P : W → Prop) : 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 Features.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

• Features.ChangeOfState.shiftsUnderBelief _e = true

def Features.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

• Features.ChangeOfState.hasOLE _e = true

def Features.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

• Features.ChangeOfState.hasSCF _e = false