Karttunen (1971): implicative verbs

[Kar71] identifies a class of complement-taking verbs — manage, remember, bother, dare, happen, … (his (2)) — whose assertion commits the speaker to the complement and whose negation commits the speaker to its negation, and analyzes such a sentence as a presupposition–proposition pair: the proposition v(S) is what is asserted, negated, or questioned, and the presupposition says what condition v(S) is for the complement S. Schema (37) makes v(S) necessary and sufficient for S (manage); (41) necessary and sufficient for ¬S (fail, forget); (54) necessary only (be able, be possible); (59) sufficient only (force, cause); non-implicatives (hope, want, try) carry no such presupposition and are plain PartialProp.ofProp. Condition is the presupposed condition, Schema pairs it with the polarity of the complement, and Schema.sentence is the presupposition–proposition pair as a PartialProp. The paper's entailment facts follow: an affirmative assertion entails the (polarity-adjusted) complement when the condition is sufficient (holds_imp), a negated one entails its negation when the condition is necessary (neg_holds_imp), double negation cancels, his (13) (manage_neg_neg_holds_imp), and the one-way cells and the non-implicatives leave the other direction open (force_neg_not_entails, beAble_not_entails, ofProp_not_entails).

inductive Karttunen1971.Condition : Type

The condition v(S) is presupposed to be for the complement.

• sufficient : Condition

  (59): force, cause, make.

• necessary : Condition

  (54): be able, be possible.

• necessaryAndSufficient : Condition

  (37) and (41): manage, fail.

@[instance_reducible]

instance Karttunen1971.instDecidableEqCondition : DecidableEq Condition

Equations

• Karttunen1971.instDecidableEqCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Karttunen1971.instReprCondition.repr : Condition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Karttunen1971.instReprCondition : Repr Condition

Equations

• Karttunen1971.instReprCondition = { reprPrec := Karttunen1971.instReprCondition.repr }

def Karttunen1971.Condition.presup : Condition → Prop → Prop → Prop

The presupposition: v stands in the condition to S.

Equations

• Karttunen1971.Condition.sufficient.presup x✝¹ x✝ = (x✝¹ → x✝)
• Karttunen1971.Condition.necessary.presup x✝¹ x✝ = (x✝ → x✝¹)
• Karttunen1971.Condition.necessaryAndSufficient.presup x✝¹ x✝ = (x✝¹ ↔ x✝)

def Karttunen1971.Condition.IsSufficient : Condition → Prop

The condition is at least sufficient.

Equations

• Karttunen1971.Condition.necessary.IsSufficient = False
• x✝.IsSufficient = True

def Karttunen1971.Condition.IsNecessary : Condition → Prop

The condition is at least necessary.

Equations

• Karttunen1971.Condition.sufficient.IsNecessary = False
• x✝.IsNecessary = True

theorem Karttunen1971.Condition.presup_imp {v S : Prop} {c : Condition} : c.IsSufficient → c.presup v S → v → S

theorem Karttunen1971.Condition.presup_imp_rev {v S : Prop} {c : Condition} : c.IsNecessary → c.presup v S → S → v

structure Karttunen1971.Schema : Type

The presupposition–proposition schema of an implicative verb: the condition v(S) is presupposed to be, and whether the complement in question is S (manage) or ¬S (fail).

• condition : Condition
• polarity : Implicative

def Karttunen1971.instDecidableEqSchema.decEq (x✝ x✝¹ : Schema) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Karttunen1971.instDecidableEqSchema : DecidableEq Schema

Equations

• Karttunen1971.instDecidableEqSchema = Karttunen1971.instDecidableEqSchema.decEq

@[instance_reducible]

instance Karttunen1971.instReprSchema : Repr Schema

Equations

• Karttunen1971.instReprSchema = { reprPrec := Karttunen1971.instReprSchema.repr }

def Karttunen1971.instReprSchema.repr : Schema → ℕ → Std.Format

Equations

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

def Karttunen1971.Schema.manage : Schema

(37): manage, remember, bother.

Equations

• Karttunen1971.Schema.manage = { condition := Karttunen1971.Condition.necessaryAndSufficient, polarity := Implicative.positive }

def Karttunen1971.Schema.fail : Schema

(41): fail, forget, neglect.

Equations

• Karttunen1971.Schema.fail = { condition := Karttunen1971.Condition.necessaryAndSufficient, polarity := Implicative.negative }

def Karttunen1971.Schema.force : Schema

(59): force, cause, make.

Equations

• Karttunen1971.Schema.force = { condition := Karttunen1971.Condition.sufficient, polarity := Implicative.positive }

def Karttunen1971.Schema.prevent : Schema

(59) for the negated complement: prevent.

Equations

• Karttunen1971.Schema.prevent = { condition := Karttunen1971.Condition.sufficient, polarity := Implicative.negative }

def Karttunen1971.Schema.beAble : Schema

(54): be able, be possible.

Equations

• Karttunen1971.Schema.beAble = { condition := Karttunen1971.Condition.necessary, polarity := Implicative.positive }

def Karttunen1971.Schema.TwoWay (k : Schema) : Prop

The two-way implicatives of (37) and (41).

Equations

• k.TwoWay = (k.condition = Karttunen1971.Condition.necessaryAndSufficient)

@[instance_reducible]

instance Karttunen1971.Schema.instDecidableTwoWay (k : Schema) : Decidable k.TwoWay

Equations

• k.instDecidableTwoWay = Karttunen1971.Schema.instDecidableTwoWay._aux_1 k

def Karttunen1971.Schema.implied (k : Schema) (S : Prop) : Prop

The complement the schema speaks of: S or ¬S by polarity.

Equations

• k.implied S = match k.polarity with | Implicative.positive => S | Implicative.negative => ¬S

def Karttunen1971.Schema.sentence (k : Schema) {W : Type u_1} (v S : W → Prop) : Semantics.Presupposition.PartialProp W

The sentence v(S): the schema's presupposition, and v as the proposition.

Equations

• k.sentence v S = { presup := fun (w : W) => k.condition.presup (v w) (k.implied (S w)), assertion := v }

theorem Karttunen1971.Schema.holds_imp (k : Schema) {W : Type u_1} (v S : W → Prop) (w : W) (h : k.condition.IsSufficient) (hs : Semantics.Presupposition.PartialProp.holds w (k.sentence v S)) : k.implied (S w)

An affirmative assertion commits the speaker to the complement when v(S) is presupposed sufficient.

theorem Karttunen1971.Schema.neg_holds_imp (k : Schema) {W : Type u_1} (v S : W → Prop) (w : W) (h : k.condition.IsNecessary) (hs : Semantics.Presupposition.PartialProp.holds w (k.sentence v S).neg) : ¬k.implied (S w)

A negated assertion commits the speaker to the negation of the complement when v(S) is presupposed necessary.

theorem Karttunen1971.Schema.manage_neg_neg_holds_imp {W : Type u_1} (v S : W → Prop) (w : W) (hs : Semantics.Presupposition.PartialProp.holds w (manage.sentence v fun (w : W) => ¬S w).neg) : S w

Double negation cancels, (13): John didn't remember not to lock his door commits the speaker to John locked his door.

theorem Karttunen1971.Schema.force_neg_not_entails : ∃ (v : Unit → Prop) (S : Unit → Prop), Semantics.Presupposition.PartialProp.holds () (force.sentence v S).neg ∧ S ()

(58): John didn't force Mary to stay home leaves open whether she stayed.

theorem Karttunen1971.Schema.beAble_not_entails : ∃ (v : Unit → Prop) (S : Unit → Prop), Semantics.Presupposition.PartialProp.holds () (beAble.sentence v S) ∧ ¬S ()

(55): John was able to come leaves open whether he came.

theorem Karttunen1971.ofProp_not_entails : (∃ (v : Unit → Prop) (S : Unit → Prop), Semantics.Presupposition.PartialProp.holds () (Semantics.Presupposition.PartialProp.ofProp v) ∧ ¬S ()) ∧ ∃ (v : Unit → Prop) (S : Unit → Prop), Semantics.Presupposition.PartialProp.holds () (Semantics.Presupposition.PartialProp.ofProp v).neg ∧ S ()

(5): a non-implicative, which has no presupposition, commits the speaker to nothing about its complement in either polarity.