Karttunen (1973): presuppositions of compound sentences

[Kar73] asks how the presuppositions of a compound sentence are determined by those of its parts. Complement-taking predicates are plugs (verbs of saying: nothing projects), holes (factives, aspectuals, implicatives: everything projects), or filters; the connectives are filters with asymmetric conditions — if A then B (13) and A and B (17) presuppose what A presupposes and what B presupposes unless A entails it, while A or B (24) filters what the negation of A entails. §9 relativizes the entailment to a set X of background assumptions, (24b′), and Entails X A C is that relation; cond, conj, disj are the relativized rules, with X = Set.univ the absolute ones.

§8 derives the coincidence of (13) and (17) from three principles Harman supplied — internal negation preserves presuppositions, logically equivalent sentences share them, and the classical equivalences hold — which here is neg_cond_neg_presup, with cond_neg_presup the corresponding fact for disjunction. On the Geraldine example (25)–(28) the second disjunct's presupposition (27) is not filtered absolutely but is filtered given (28) (geraldine_presup_absolute, geraldine_presup_relative). §10 rejects truth-functional three-valued conjunction on (35): it filters by the falsity of the first conjunct where the entailment filter does not (kleene_35, conj_presup_35); the substrate's pointwise PartialProp.andFilter agrees with (17) where the first conjunct holds (conj_presup_iff_andFilter) and shares the truth-functional verdict where it fails (andFilter_35b). §11 treats propositional attitudes: the [Hin62] equivalence (38) lets the hole treatment of believe survive (37) by re-collecting the conjunction inside the attitude (hole_conj_presup, hole_conj_assertion_iff), but not (42), where believe and hope cannot be re-collected — hence the tentative verdict that the class are plugs (conj_plug_plug_presup).

The filters

def Karttunen1973.Entails {W : Type u_1} (X : Set W) (A C : W → Prop) : Prop

A entails C given the background assumptions X: X ∪ {A} ⊨ C.

Equations

• Karttunen1973.Entails X A C = ∀ w ∈ X, A w → C w

@[instance_reducible]

instance Karttunen1973.instDecidableEntailsOfFintypeOfMemSetOfDecidablePred {W : Type u_1} (X : Set W) [Fintype W] [DecidablePred fun (x : W) => x ∈ X] (A C : W → Prop) [DecidablePred A] [DecidablePred C] : Decidable (Entails X A C)

Equations

• Karttunen1973.instDecidableEntailsOfFintypeOfMemSetOfDecidablePred X A C = Karttunen1973.instDecidableEntailsOfFintypeOfMemSetOfDecidablePred._aux_1 X A C

def Karttunen1973.cond {W : Type u_1} (X : Set W) (p q : Semantics.Presupposition.PartialProp W) : Semantics.Presupposition.PartialProp W

(13), relativized by (24b′): if A then B presupposes what A presupposes, and what B presupposes unless A entails it given X.

Equations

• Karttunen1973.cond X p q = { presup := fun (w : W) => p.presup w ∧ (¬Karttunen1973.Entails X p.assertion q.presup → q.presup w), assertion := fun (w : W) => p.assertion w → q.assertion w }

def Karttunen1973.conj {W : Type u_1} (X : Set W) (p q : Semantics.Presupposition.PartialProp W) : Semantics.Presupposition.PartialProp W

(17), relativized: A and B presupposes what A presupposes, and what B presupposes unless A entails it given X.

Equations

• Karttunen1973.conj X p q = { presup := fun (w : W) => p.presup w ∧ (¬Karttunen1973.Entails X p.assertion q.presup → q.presup w), assertion := fun (w : W) => p.assertion w ∧ q.assertion w }

def Karttunen1973.disj {W : Type u_1} (X : Set W) (p q : Semantics.Presupposition.PartialProp W) : Semantics.Presupposition.PartialProp W

(24), relativized: A or B presupposes what A presupposes, and what B presupposes unless the negation of A entails it given X.

Equations

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

Harman's derivation (§8)

theorem Karttunen1973.neg_cond_neg_presup {W : Type u_1} (X : Set W) (p q : Semantics.Presupposition.PartialProp W) : (cond X p q.neg).neg.presup = (conj X p q).presup

The conjunction filter is the conditional filter through A ∧ B ≡ ¬(A → ¬B), with negation a hole.

theorem Karttunen1973.cond_neg_presup {W : Type u_1} (X : Set W) (p q : Semantics.Presupposition.PartialProp W) : (cond X p.neg q).presup = (disj X p q).presup

The disjunction filter is the conditional filter through A ∨ B ≡ ¬A → B.

theorem Karttunen1973.conj_presup_iff_andFilter {W : Type u_1} (X : Set W) (p q : Semantics.Presupposition.PartialProp W) (w : W) (hX : w ∈ X) (h : p.assertion w) : (conj X p q).presup w ↔ (p.andFilter q).presup w

Where the first conjunct holds, (17) agrees with the substrate's pointwise filter PartialProp.andFilter.

Background assumptions (§9)

inductive Karttunen1973.Geraldine : Type

Whether Geraldine is a Mormon and whether she has worn holy underwear.

• mormonWorn : Geraldine
• mormonUnworn : Geraldine
• gentileWorn : Geraldine
• gentileUnworn : Geraldine

@[instance_reducible]

instance Karttunen1973.instDecidableEqGeraldine : DecidableEq Geraldine

Equations

• Karttunen1973.instDecidableEqGeraldine x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Karttunen1973.instFintypeGeraldine : Fintype Geraldine

Equations

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

@[reducible, inline]

abbrev Karttunen1973.mormon : Set Geraldine

(26) Geraldine is a Mormon.

Equations

• Karttunen1973.mormon = {Karttunen1973.Geraldine.mormonWorn, Karttunen1973.Geraldine.mormonUnworn}

@[reducible, inline]

abbrev Karttunen1973.worn : Set Geraldine

(27) Geraldine has worn holy underwear.

Equations

• Karttunen1973.worn = {Karttunen1973.Geraldine.mormonWorn, Karttunen1973.Geraldine.gentileWorn}

@[reducible, inline]

abbrev Karttunen1973.allMormonsWorn : Set Geraldine

(28) All Mormons have worn holy underwear, Fred's background assumption.

Equations

• Karttunen1973.allMormonsWorn = {Karttunen1973.Geraldine.mormonUnworn}ᶜ

def Karttunen1973.givenUp : Semantics.Presupposition.PartialProp Geraldine

She has given up wearing her holy underwear: presupposes (27); the assertion is idealized.

Equations

• Karttunen1973.givenUp = { presup := fun (x : Karttunen1973.Geraldine) => x ∈ Karttunen1973.worn, assertion := fun (x : Karttunen1973.Geraldine) => True }

def Karttunen1973.geraldine (X : Set Geraldine) : Semantics.Presupposition.PartialProp Geraldine

(25) Either Geraldine is not a Mormon or she has given up wearing her holy underwear, relative to the background X.

Equations

• Karttunen1973.geraldine X = Karttunen1973.disj X (Semantics.Presupposition.PartialProp.ofProp fun (x : Karttunen1973.Geraldine) => x ∉ Karttunen1973.mormon) Karttunen1973.givenUp

theorem Karttunen1973.geraldine_presup_absolute : ¬(geraldine Set.univ).presup Geraldine.mormonUnworn

Absolutely, (25) presupposes (27): (26) alone does not entail it.

theorem Karttunen1973.geraldine_presup_relative (w : Geraldine) : w ∈ allMormonsWorn → (geraldine allMormonsWorn).presup w

Given (28), (25) presupposes nothing: (26) and (28) together entail (27).

Truth-functional conjunction (§10)

inductive Karttunen1973.France : Type

Whether Paris is the capital of France and whether France has a king.

• parisKing : France
• parisNoKing : France
• marseilleKing : France
• marseilleNoKing : France

@[instance_reducible]

instance Karttunen1973.instDecidableEqFrance : DecidableEq France

Equations

• Karttunen1973.instDecidableEqFrance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Karttunen1973.instFintypeFrance : Fintype France

Equations

• Karttunen1973.instFintypeFrance = { elems := { val := ↑Karttunen1973.France.enumList, nodup := Karttunen1973.France.enumList_nodup }, complete := Karttunen1973.instFintypeFrance._proof_1 }

@[reducible, inline]

abbrev Karttunen1973.capitalParis : Set France

Paris is the capital of France.

Equations

• Karttunen1973.capitalParis = {Karttunen1973.France.parisKing, Karttunen1973.France.parisNoKing}

@[reducible, inline]

abbrev Karttunen1973.hasKing : Set France

France has a king.

Equations

• Karttunen1973.hasKing = {Karttunen1973.France.parisKing, Karttunen1973.France.marseilleKing}

def Karttunen1973.kingBald : Semantics.Presupposition.PartialProp France

The king of France is bald: presupposes a king; baldness is idealized.

Equations

• Karttunen1973.kingBald = { presup := fun (x : Karttunen1973.France) => x ∈ Karttunen1973.hasKing, assertion := fun (x : Karttunen1973.France) => True }

theorem Karttunen1973.conj_presup_35 : ¬(conj Set.univ (Semantics.Presupposition.PartialProp.ofProp fun (x : France) => x ∈ capitalParis) kingBald).presup France.parisNoKing ∧ ¬(conj Set.univ (Semantics.Presupposition.PartialProp.ofProp fun (x : France) => x ∉ capitalParis) kingBald).presup France.parisNoKing

(35a) Paris is the capital of France, and the king of France is bald and (35b) with Marseilles both presuppose a king under (17): neither capital claim entails one.

theorem Karttunen1973.kleene_35 : min ((Semantics.Presupposition.PartialProp.ofProp fun (x : France) => x ∈ capitalParis).eval France.parisNoKing) (kingBald.eval France.parisNoKing) = Trivalent.indet ∧ min ((Semantics.Presupposition.PartialProp.ofProp fun (x : France) => x ∉ capitalParis).eval France.parisNoKing) (kingBald.eval France.parisNoKing) = Trivalent.false

Strong-Kleene conjunction makes (35b) false at the actual world and so bivalent — presupposition-free — while (35a) is undefined.

theorem Karttunen1973.andFilter_35b : ((Semantics.Presupposition.PartialProp.ofProp fun (x : France) => x ∉ capitalParis).andFilter kingBald).presup France.parisNoKing

The substrate's pointwise filter shares the truth-functional verdict on (35b): the second conjunct's presupposition is filtered where the first conjunct is false.

Propositional attitudes (§11)

def Karttunen1973.hole {W : Type u_1} (att : (W → Prop) → W → Prop) (φ : Semantics.Presupposition.PartialProp W) : Semantics.Presupposition.PartialProp W

A hole lets the complement's presuppositions through: att applies to its assertion.

Equations

• Karttunen1973.hole att φ = { presup := φ.presup, assertion := att φ.assertion }

def Karttunen1973.plug {W : Type u_1} (att : (W → Prop) → W → Prop) (φ : Semantics.Presupposition.PartialProp W) : Semantics.Presupposition.PartialProp W

A plug blocks them.

Equations

• Karttunen1973.plug att φ = { presup := fun (x : W) => True, assertion := att φ.assertion }

theorem Karttunen1973.conj_hole_hole_presup {W : Type u_1} (w : W) (att₁ att₂ : (W → Prop) → W → Prop) (A C : W → Prop) : (conj Set.univ (hole att₁ (Semantics.Presupposition.PartialProp.ofProp A)) (hole att₂ { presup := A, assertion := C })).presup w ↔ (¬∀ (v : W), att₁ A v → A v) → A w

(37) Bill believes that Fred has been beating Zelda, and furthermore, Bill believes that Fred has stopped beating Zelda under the hole treatment presupposes A unless the first conjunct — that Bill believes A — entails A. The same holds of (42), with hope as the second attitude.

theorem Karttunen1973.hole_conj_presup {W : Type u_1} (w : W) (att : (W → Prop) → W → Prop) (A C : W → Prop) : (hole att (conj Set.univ (Semantics.Presupposition.PartialProp.ofProp A) { presup := A, assertion := C })).presup w

(39), the re-collected Bill believes that Fred has been beating Zelda and that he has stopped: the filter applies inside the complement and nothing is presupposed, whatever the verb's status.

theorem Karttunen1973.hole_conj_assertion_iff {W : Type u_1} (w : W) (R : W → W → Prop) (A C : W → Prop) : (hole (ModalLogic.box R) (conj Set.univ (Semantics.Presupposition.PartialProp.ofProp A) { presup := A, assertion := C })).assertion w ↔ (conj Set.univ (hole (ModalLogic.box R) (Semantics.Presupposition.PartialProp.ofProp A)) (hole (ModalLogic.box R) { presup := A, assertion := C })).assertion w

(38): (37) and (39) assert the same thing ([Hin62]), so the hole treatment survives (37) only by letting the equivalence do the filtering.

theorem Karttunen1973.conj_plug_plug_presup {W : Type u_1} (w : W) (att₁ att₂ : (W → Prop) → W → Prop) (A C : W → Prop) : (conj Set.univ (plug att₁ (Semantics.Presupposition.PartialProp.ofProp A)) (plug att₂ { presup := A, assertion := C })).presup w

Two distinct attitudes (43) admit no re-collection; as plugs, (42) presupposes nothing outright — K's tentative verdict for the whole class.