Implicative verbs

Karttunen analyzes an implicative sentence as a presupposition–proposition pair: it asserts the proposition v(S) and presupposes that v(S) is a condition for the complement, so that what it implies about the complement follows from the assertion or from its denial. The condition is read off the implication signature (NaturalLogic.ImplicationSignature): a verb implying a complement in a positive context presupposes v(S) sufficient for it, and one implying a complement in a negative context presupposes v(S) necessary for the complement's negation. Here the conditions are read through any relations of sufficiency and necessity that are sound for truth at a world (Implicative.Interpretation), Karttunen's own interpretation being the material conditional at the world (Implicative.Interpretation.material), and under every interpretation an implicative sentence implies what its signature says.

Main definitions

• Implicative.Interpretation: relations of sufficiency and necessity between facts, sound at worlds
• Implicative.sentence: the trivalent proposition of a verb with a given implication signature, undefined where its presupposition fails

Main results

• Implicative.holds_signed_of_implied_eq: an affirmed or denied claim implies the polarity of the complement that its signature records for that context
• Implicative.antitone_support: a signature that implies more presupposes more

References

• [Kar71a]

structure Implicative.Interpretation (F : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

An interpretation of sufficiency and necessity between facts F that is sound for truth at the worlds W. A fact sufficient for another at a world makes it true there when it is true, and a fact necessary for another is true there when the other is.

• Holds : F → W → Prop

  The fact holds at the world.

• neg : F → F

  The negation of a fact.

• holds_neg (a : F) (w : W) : self.Holds (self.neg a) w ↔ ¬self.Holds a w
• Sufficient : F → F → W → Prop

  The first fact is sufficient for the second at the world.

• Necessary : F → F → W → Prop

  The first fact is necessary for the second at the world.

• holds_of_sufficient {a b : F} {w : W} : self.Sufficient a b w → self.Holds a w → self.Holds b w
• holds_of_necessary {a b : F} {w : W} : self.Necessary a b w → self.Holds b w → self.Holds a w

def Implicative.Interpretation.material (W : Type u_1) : Interpretation (W → Prop) W

Karttunen's interpretation takes facts to be propositions and a condition to be the material conditional at the world.

Equations

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

def Implicative.Interpretation.signed {F : Type u_1} {W : Type u_2} (R : Interpretation F W) : Polarity → F → F

A fact or its negation, by polarity.

Equations

• R.signed Polarity.positive x✝ = x✝
• R.signed Polarity.negative x✝ = R.neg x✝

theorem Implicative.Interpretation.holds_signed_negative_mul {F : Type u_1} {W : Type u_2} {R : Interpretation F W} {q : Polarity} {a : F} {w : W} : R.Holds (R.signed (Polarity.negative * q) a) w ↔ ¬R.Holds (R.signed q a) w

noncomputable def Implicative.sentence {F : Type u_1} {W : Type u_2} (R : Interpretation F W) (s : NaturalLogic.ImplicationSignature) (v S : F) : W → SignType

The sentence of a verb with implication signature s, asserted proposition v and embedded fact S. It presupposes that v is sufficient for the complement s implies in a positive context and necessary for the negation of the complement it implies in a negative context, and it asserts v.

Equations

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

theorem Implicative.holds_signed_of_implied_eq {F : Type u_1} {W : Type u_2} {R : Interpretation F W} {s : NaturalLogic.ImplicationSignature} {v S : F} {w : W} {m q : Polarity} (hq : s.implied m = ↑q) (hs : (m • sentence R s v S) w = 1) : R.Holds (R.signed q S) w

A claim of matrix polarity m implies the polarity of the complement that its signature records for a context of that polarity.

theorem Implicative.antitone_support {F : Type u_1} {W : Type u_2} (R : Interpretation F W) (v S : F) : Antitone fun (s : NaturalLogic.ImplicationSignature) => Function.support (sentence R s v S)

A signature that implies more presupposes more, the presupposition of a sentence weakening as its signature descends.