Karttunen (1973): Presuppositions of Compound Sentences

This file formalizes Karttunen's paper, which asks how the presuppositions of a compound sentence are determined by those of its parts. The cumulative hypothesis of Langendoen and Savin adds them up; Karttunen keeps it for the holes, factives, aspectuals and implicatives, which let every presupposition of their complement through, and sets against them the plugs, verbs of saying, which let none through, and the filters, the connectives, which let a presupposition of their second clause through unless the first clause filters it: if A then B (13) and A and B (17) presuppose what A presupposes and each presupposition of B that A does not entail, and A or B (24) each presupposition of B that ¬A does not entail.

A sentence is a computation of the Writer monad whose value is its assertion and whose log lists its presuppositions, each filtered on its own (Presupposing), the side-effect carrier of Giorgolo and Asudeh. The monad's own composition concatenates the logs, and is the cumulative hypothesis (conj_false); a hole maps the value and keeps the log, internal negation among them; a plug keeps the value and drops the log; and a filter drops from the second clause's log what the first clause filters. The connectives take the filtering relation as a parameter: entailment in the original conditions, entailment from assumed facts in the revisions of §9 (Filters).

§8 derives the rule for conjunction and the rule for disjunction from the rule for conditionals by Harman's principles, that internal negation keeps presuppositions and that the classical equivalences of A ⊃ B with ¬A ∨ B and of A & B with ¬(¬A ∨ ¬B) keep them (harman_conj, harman_disj), and the rules satisfy the principles. The rules are not commutative ((16), (22)), so the principle that equivalent sentences share presuppositions can hold only of such chosen equivalences. §9's Geraldine example (25) presupposes (27) absolutely but not given (28), and does again in the contrary context the paper sketches; the Nixon examples (30) call for the same relativization with every connective. §10 finds no truth-functional three-valued conjunction that behaves like a filter: Bochvar's internal conjunction is a hole, his external one a plug, and Łukasiewicz's filters by the falsity of the other conjunct, so that (35b) comes out presupposition-free and (35a) does not. §11 finds that a hole believe survives (37) only through the equivalence (38), and fails on (42), whence the tentative verdict that attitude verbs are plugs.

Implementation notes

• A sentence's presuppositions are a list, the finite list of basic presuppositions of (5) in Karttunen's 1974 paper; only membership matters.
• The entailment a filter uses is from the truth of the first clause, which requires its presuppositions as well as its assertion (Presupposing.truth), so a presupposition that both clauses share is filtered as the second clause's and kept as the first's, as fn. 10 says. A filter thus reads the first clause's log, which no composition in Giorgolo and Asudeh's monad can.
• The per-presupposition rule is tested on Jack has children, and Jack's children regret that baldness is hereditary, built from the presuppositions of (1a) and (1b): it filters the first presupposition of the second conjunct and keeps the second, where a single conjoined presupposition would keep both.
• Murphy's restrictions on the assumed facts of §9 are read set-theoretically: some set of the facts, possibly empty, entails the presupposition together with the premise, is consistent with the premise, and does not entail the presupposition alone. On this reading the empty set filters only a presupposition the premise entails, of a consistent premise, that is not a tautology (filters_empty_iff), so the revised condition keeps the tautological presupposition of fn. 13 (univ_mem_log_disj_filters), which the footnote counts as filtered under the revised condition as well as the original.
• The assumed facts are a set of propositions, not a deductively closed common ground: over the propositions a closed context accepts, Murphy's first restriction blocks nothing, since a context that entails ¬A accepts A ⊃ C too (filters_sets_of_compl_mem).
• Van Fraassen's conjunction (34c), which the paper finds to behave as Łukasiewicz's on (35), is left out.

References

• [Kar73]
• [Kar74a]
• [GA12]
• [Boc38]
• [Hin62]

Sentences

@[reducible, inline]

abbrev Karttunen1973.Presupposing (W α : Type u) : Type u

The Writer monad of presuppositions, in which a computation yields a value and logs the propositions over W it presupposes. A sentence, as the projection rules see it, is a computation whose value is its assertion.

Equations

• Karttunen1973.Presupposing W = Writer (List (Set W))

def Karttunen1973.Presupposing.truth {W : Type u} (A : Presupposing W (Set W)) : Set W

The worlds where the sentence is true, those where its presuppositions and its assertion hold.

Equations

• A.truth = Writer.val A ∩ {w : W | ∀ C ∈ Writer.log A, w ∈ C}

theorem Karttunen1973.Presupposing.compl_map_compl {W : Type u} (A : Presupposing W (Set W)) : (fun (x : Set W) => xᶜ) <$> (fun (x : Set W) => xᶜ) <$> A = A

Internal negation is an involution.

theorem Karttunen1973.Presupposing.truth_subset_of_mem {W : Type u} (A : Presupposing W (Set W)) {C : Set W} (h : C ∈ Writer.log A) : A.truth ⊆ C

A sentence entails each of its presuppositions (fn. 10).

def Karttunen1973.Presupposing.ofTrivalent {W : Type u} (p : W → SignType) : Presupposing W (Set W)

The sentence of a trivalent proposition asserts its positive extension and presupposes its support.

Equations

• Karttunen1973.Presupposing.ofTrivalent p = Writer.mk (Trivalent.posExt p) [Function.support p]

The filters (§5–§7)

noncomputable def Karttunen1973.cond {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) : Presupposing W (Set W)

Under rule (13), if A then B presupposes what A presupposes and each presupposition of B that A does not filter, by the relation φ from the truth of A.

Equations

• Karttunen1973.cond φ A B = Writer.mk ((Writer.val A)ᶜ ∪ Writer.val B) (Writer.log A ++ List.filter (fun (C : Set W) => decide ¬φ A.truth C) (Writer.log B))

noncomputable def Karttunen1973.conj {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) : Presupposing W (Set W)

Under rule (17), A and B presupposes what A presupposes and each presupposition of B that A does not filter.

Equations

• Karttunen1973.conj φ A B = Writer.mk (Writer.val A ∩ Writer.val B) (Writer.log A ++ List.filter (fun (C : Set W) => decide ¬φ A.truth C) (Writer.log B))

noncomputable def Karttunen1973.disj {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) : Presupposing W (Set W)

Under rule (24), A or B presupposes what A presupposes and each presupposition of B that the negation of A does not filter.

Equations

• Karttunen1973.disj φ A B = Writer.mk (Writer.val A ∪ Writer.val B) (Writer.log A ++ List.filter (fun (C : Set W) => decide ¬φ ((fun (x : Set W) => xᶜ) <$> A).truth C) (Writer.log B))

@[simp]

theorem Karttunen1973.mem_log_cond {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) {C : Set W} : C ∈ Writer.log (cond φ A B) ↔ C ∈ Writer.log A ∨ C ∈ Writer.log B ∧ ¬φ A.truth C

@[simp]

theorem Karttunen1973.mem_log_conj {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) {C : Set W} : C ∈ Writer.log (conj φ A B) ↔ C ∈ Writer.log A ∨ C ∈ Writer.log B ∧ ¬φ A.truth C

@[simp]

theorem Karttunen1973.mem_log_disj {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) {C : Set W} : C ∈ Writer.log (disj φ A B) ↔ C ∈ Writer.log A ∨ C ∈ Writer.log B ∧ ¬φ ((fun (x : Set W) => xᶜ) <$> A).truth C

theorem Karttunen1973.conj_false {W : Type u} (A B : Presupposing W (Set W)) : conj (fun (x x_1 : Set W) => False) A B = (fun (x1 x2 : Set W) => x1 ∩ x2) <$> A <*> B

The cumulative hypothesis of Langendoen and Savin (§1) is the rule for conjunction with nothing filtered, and the Writer monad's own conjunction, which concatenates the presuppositions.

theorem Karttunen1973.truth_conj {W : Type u} (A B : Presupposing W (Set W)) : (conj (fun (x1 x2 : Set W) => x1 ⊆ x2) A B).truth = A.truth ∩ B.truth

Under the original condition, a filtered presupposition holds wherever the first conjunct is true, so the conjunction is true exactly where both conjuncts are.

Harman's derivation (§8)

theorem Karttunen1973.log_cond {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) : Writer.log (cond φ A B) = Writer.log (disj φ ((fun (x : Set W) => xᶜ) <$> A) B)

The rules satisfy Harman's principle for the equivalence of A ⊃ B with ¬A ∨ B.

theorem Karttunen1973.log_conj {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) : Writer.log (conj φ A B) = Writer.log ((fun (x : Set W) => xᶜ) <$> disj φ ((fun (x : Set W) => xᶜ) <$> A) ((fun (x : Set W) => xᶜ) <$> B))

The rules satisfy Harman's principle for the equivalence of A & B with ¬(¬A ∨ ¬B).

theorem Karttunen1973.log_disj {W : Type u} (φ : Set W → Set W → Prop) (A B : Presupposing W (Set W)) : Writer.log (disj φ A B) = Writer.log (cond φ ((fun (x : Set W) => xᶜ) <$> A) B)

The rules satisfy Harman's principle for the equivalence of A ∨ B with ¬A ⊃ B.

theorem Karttunen1973.harman_conj {W : Type u} {S : Type u_1} {neg : S → S} {cond conj disj : S → S → S} {π : S → Set (Set W)} {f : S → Set W → Prop} (hneg : ∀ (A : S), π (neg A) = π A) (hcond : ∀ (A B : S), π (cond A B) = π (disj (neg A) B)) (hconj : ∀ (A B : S), π (conj A B) = π (neg (disj (neg A) (neg B)))) (h13 : ∀ (A B : S), π (cond A B) = π A ∪ {C : Set W | C ∈ π B ∧ ¬f A C}) (A B : S) : π (conj A B) = π A ∪ {C : Set W | C ∈ π B ∧ ¬f A C}

In Harman's derivation of (17) from (13) (§8), if internal negation keeps presuppositions, and A ⊃ B shares them with ¬A ∨ B and A & B with ¬(¬A ∨ ¬B), then a conditional that filters a presupposition of B when A filters it makes the conjunction filter it the same way.

theorem Karttunen1973.harman_disj {W : Type u} {S : Type u_1} {neg : S → S} {cond disj : S → S → S} {π : S → Set (Set W)} {f : S → Set W → Prop} (hneg : ∀ (A : S), π (neg A) = π A) (hdisj : ∀ (A B : S), π (disj A B) = π (cond (neg A) B)) (h13 : ∀ (A B : S), π (cond A B) = π A ∪ {C : Set W | C ∈ π B ∧ ¬f A C}) (A B : S) : π (disj A B) = π A ∪ {C : Set W | C ∈ π B ∧ ¬f (neg A) C}

The same reasoning (§8) derives the rule for disjunction (24). With A ∨ B sharing its presuppositions with ¬A ⊃ B, the disjunction filters a presupposition of B when ¬A filters it.

Jack's children (§5–§7)

def Karttunen1973.hasChildren : Presupposing (Bool × Bool) (Set (Bool × Bool))

Jack has children, over whether he does and whether baldness is hereditary.

Equations

• Karttunen1973.hasChildren = Writer.mk {w : Bool × Bool | w.1 = true} []

def Karttunen1973.allBald : Presupposing (Bool × Bool) (Set (Bool × Bool))

All of Jack's children are bald, which presupposes that Jack has children; the assertion is idealized.

Equations

• Karttunen1973.allBald = Writer.mk Set.univ [{w : Bool × Bool | w.1 = true}]

def Karttunen1973.regretHereditary : Presupposing (Bool × Bool) (Set (Bool × Bool))

Jack's children regret that baldness is hereditary, which presupposes that Jack has children, as (1a) does, and that baldness is hereditary, as (1b) does.

Equations

• Karttunen1973.regretHereditary = Writer.mk Set.univ [{w : Bool × Bool | w.1 = true}, {w : Bool × Bool | w.2 = true}]

theorem Karttunen1973.log_conj_16 : Writer.log (conj (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) hasChildren allBald) = [] ∧ Writer.log (conj (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) allBald hasChildren) = [{w : Bool × Bool | w.1 = true}]

(16a) presupposes nothing and (16b) that Jack has children, so conjunction is not commutative on presuppositions.

theorem Karttunen1973.log_disj_22 : Writer.log (disj (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) ((fun (x : Set (Bool × Bool)) => xᶜ) <$> hasChildren) allBald) = [] ∧ Writer.log (disj (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) allBald ((fun (x : Set (Bool × Bool)) => xᶜ) <$> hasChildren)) = [{w : Bool × Bool | w.1 = true}]

(22a) presupposes nothing, and by (24a) (22b) presupposes that Jack has children, a sentence the paper leaves undecided (fn. 11).

theorem Karttunen1973.log_cond_11a_disj : Writer.log (cond (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) hasChildren allBald) = [] ∧ {w : Bool × Bool | w.1 = true} ∈ Writer.log (disj (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) hasChildren allBald)

The rule for conditionals does not carry over to disjunction (§8). (11a) presupposes nothing, but Either Jack has children or all of Jack's children are bald presupposes that he has children, since his having none does not entail it.

theorem Karttunen1973.mem_log_conj_regret : {w : Bool × Bool | w.2 = true} ∈ Writer.log (conj (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) hasChildren regretHereditary) ∧ {w : Bool × Bool | w.1 = true} ∉ Writer.log (conj (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) hasChildren regretHereditary)

In Jack has children, and Jack's children regret that baldness is hereditary, the second conjunct presupposes that Jack has children and that baldness is hereditary, and the rule (17) filters the first, which the first conjunct entails, and keeps the second.

Assumed facts (§9)

def Karttunen1973.Filters {W : Type u} (F : Set (Set W)) (P C : Set W) : Prop

Under (24b′) and (17b′), given the assumed facts F, the premise P filters C when some set of them, possibly empty, entails C together with P, though it does not entail the negation of P nor C alone (Murphy's restrictions).

Equations

• Karttunen1973.Filters F P C = ∃ X ⊆ F, ⋂₀ X ∩ P ⊆ C ∧ ¬⋂₀ X ⊆ Pᶜ ∧ ¬⋂₀ X ⊆ C

theorem Karttunen1973.filters_empty_iff {W : Type u} {P C : Set W} : Filters ∅ P C ↔ P ⊆ C ∧ P.Nonempty ∧ C ≠ Set.univ

With no assumed facts, a premise filters what it entails, if it is consistent and what it entails is not a tautology.

theorem Karttunen1973.not_filters_univ {W : Type u} (F : Set (Set W)) (P : Set W) : ¬Filters F P Set.univ

No set of assumed facts filters a tautology, which each of them entails alone.

theorem Karttunen1973.filters_sets_of_compl_mem {W : Type u} {G : Filter W} {P C : Set W} (hP : Pᶜ ∈ G) (hPC : (P ∩ C).Nonempty) (hC : ¬Pᶜ ⊆ C) : Filters G.sets P C

Over the propositions a deductively closed context accepts, Murphy's first restriction blocks nothing, since a context that entails ¬P accepts P ⊃ C as well, which is consistent with P where C is and entails C with it.

inductive Karttunen1973.Geraldine : Type

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

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

@[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}

noncomputable def Karttunen1973.geraldine (φ : Set Geraldine → Set Geraldine → Prop) : Presupposing Geraldine (Set Geraldine)

(25) Either Geraldine is not a Mormon or she has given up wearing her holy underwear, whose second disjunct presupposes (27); its assertion is idealized.

Equations

• Karttunen1973.geraldine φ = Karttunen1973.disj φ (Writer.mk Karttunen1973.mormonᶜ []) (Writer.mk Set.univ [Karttunen1973.worn])

theorem Karttunen1973.worn_mem_log_geraldine : worn ∈ Writer.log (geraldine fun (x1 x2 : Set Geraldine) => x1 ⊆ x2)

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

theorem Karttunen1973.worn_not_mem_log_geraldine_28 : worn ∉ Writer.log (geraldine (Filters {{Geraldine.mormonUnworn}ᶜ}))

Given (28) All Mormons have worn holy underwear, (25) does not presuppose (27), since (26) and (28) together entail it.

theorem Karttunen1973.worn_mem_log_geraldine_contrary : worn ∈ Writer.log (geraldine (Filters {{Geraldine.mormonWorn}ᶜ}))

In the contrary context the paper sketches, where Mormons must not wear holy underwear, (25) presupposes (27).

theorem Karttunen1973.worn_mem_log_geraldine_notMormon : worn ∈ Writer.log (geraldine (Filters {mormonᶜ}))

By Murphy's first restriction, an assumed fact that contradicts the negated first disjunct, Geraldine is not a Mormon, filters nothing, so (25) presupposes (27) relative to it.

def Karttunen1973.appoint : Presupposing (Bool × Bool) (Set (Bool × Bool))

Nixon will appoint J. Edgar Hoover to the Cabinet, over whether he will and whether Hoover is a homosexual (32).

Equations

• Karttunen1973.appoint = Writer.mk {w : Bool × Bool | w.1 = true} []

def Karttunen1973.regret : Presupposing (Bool × Bool) (Set (Bool × Bool))

He will regret having appointed a homosexual, which presupposes (31).

Equations

• Karttunen1973.regret = Writer.mk Set.univ [{w : Bool × Bool | w.1 = true ∧ w.2 = true}]

theorem Karttunen1973.mem_log_30 : {w : Bool × Bool | w.1 = true ∧ w.2 = true} ∈ Writer.log (cond (Filters ∅) appoint regret) ∧ {w : Bool × Bool | w.1 = true ∧ w.2 = true} ∈ Writer.log (conj (Filters ∅) appoint regret) ∧ {w : Bool × Bool | w.1 = true ∧ w.2 = true} ∈ Writer.log (disj (Filters ∅) ((fun (x : Set (Bool × Bool)) => xᶜ) <$> appoint) regret)

With no assumed facts, each of (30a–c) presupposes (31), which (33) alone does not entail.

theorem Karttunen1973.not_mem_log_30 : {w : Bool × Bool | w.1 = true ∧ w.2 = true} ∉ Writer.log (cond (Filters {{w : Bool × Bool | w.2 = true}}) appoint regret) ∧ {w : Bool × Bool | w.1 = true ∧ w.2 = true} ∉ Writer.log (conj (Filters {{w : Bool × Bool | w.2 = true}}) appoint regret) ∧ {w : Bool × Bool | w.1 = true ∧ w.2 = true} ∉ Writer.log (disj (Filters {{w : Bool × Bool | w.2 = true}}) ((fun (x : Set (Bool × Bool)) => xᶜ) <$> appoint) regret)

Given (32), none of the conditional, the conjunction and the disjunction of (30a–c) presupposes (31), since (32) and (33) together entail it.

def Karttunen1973.johnDumb : Presupposing Bool (Set Bool)

John is dumb, over whether he is.

Equations

• Karttunen1973.johnDumb = Writer.mk {true} []

def Karttunen1973.knowsTautology : Presupposing Bool (Set Bool)

He knows that if it rains, it rains, which presupposes a tautology (fn. 13).

Equations

• Karttunen1973.knowsTautology = Writer.mk Set.univ [Set.univ]

theorem Karttunen1973.univ_not_mem_log_disj : Set.univ ∉ Writer.log (disj (fun (x1 x2 : Set Bool) => x1 ⊆ x2) johnDumb knowsTautology)

The original condition (24b) filters the tautology presupposed by the second disjunct of Either John is dumb, or he knows that if it rains, it rains (fn. 13).

theorem Karttunen1973.univ_mem_log_disj_filters (F : Set (Set Bool)) : Set.univ ∈ Writer.log (disj (Filters F) johnDumb knowsTautology)

The revised condition (24b′) keeps fn. 13's tautology, since with Murphy's restrictions no set of assumed facts filters it.

Truth-functional conjunction (§10)

theorem Karttunen1973.meetWeak_ne_zero_iff {W : Type u} (p q : W → SignType) (w : W) : (p w).meetWeak (q w) ≠ 0 ↔ p w ≠ 0 ∧ q w ≠ 0

Bochvar's internal conjunction (34a) ([Boc38]), the substrate's SignType.meetWeak, is a hole, defined only where both conjuncts are.

theorem Karttunen1973.meetWeak_ofProp_ne_zero {W : Type u} (p q : W → SignType) (w : W) : (SignType.ofProp (p w = 1)).meetWeak (SignType.ofProp (q w = 1)) ≠ 0

Bochvar's external conjunction (34d), the conjunction of the conjuncts' truth, t(A) & t(B) (fn. 18), is a plug, defined everywhere.

theorem Karttunen1973.inf_ne_zero_of_eq_neg_one {W : Type u} (p q : W → SignType) (w : W) (hf : p w = -1) : (p ⊓ q) w ≠ 0

Łukasiewicz's conjunction (34b), Strong Kleene ⊓, is defined wherever a conjunct is false, whatever the other conjunct presupposes.

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 ⋯

@[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}

noncomputable def Karttunen1973.kingBald : France → SignType

The king of France is bald, which presupposes a king; the assertion is idealized.

Equations

• Karttunen1973.kingBald = Karttunen1973.hasKing.indicator 1

theorem Karttunen1973.inf_kingBald_35 : min (SignType.ofProp (France.parisNoKing ∈ capitalParis)) (kingBald France.parisNoKing) = 0 ∧ min (SignType.ofProp (France.parisNoKing ∉ capitalParis)) (kingBald France.parisNoKing) = -1

At the actual world of (35), with no king, Łukasiewicz's conjunction leaves (35a) Paris is the capital of France, and the king of France is bald undefined but makes (35b), with Marseilles, false.

theorem Karttunen1973.hasKing_mem_log_conj_35 : hasKing ∈ Writer.log (conj (fun (x1 x2 : Set France) => x1 ⊆ x2) (Presupposing.ofTrivalent fun (w : France) => SignType.ofProp (w ∈ capitalParis)) (Presupposing.ofTrivalent kingBald)) ∧ hasKing ∈ Writer.log (conj (fun (x1 x2 : Set France) => x1 ⊆ x2) (Presupposing.ofTrivalent fun (w : France) => SignType.ofProp (w ∉ capitalParis)) (Presupposing.ofTrivalent kingBald))

By (17) both sentences of (35) presuppose a king, since neither capital entails one.

theorem Karttunen1973.meetMiddle_35b : (SignType.ofProp (France.parisNoKing ∉ capitalParis)).meetMiddle (kingBald France.parisNoKing) = -1

The substrate's Middle Kleene SignType.meetMiddle is a truth table too, and shares Łukasiewicz's verdict on (35b), filtering the presupposition of the second conjunct where the first is false.

Propositional attitudes (§11)

A hole maps the complement's value and keeps its log, att <$> A; a plug keeps the value and drops the log, pure (att A.val).

theorem Karttunen1973.mem_log_conj_hole {W : Type u} (φ : Set W → Set W → Prop) (att₁ att₂ : Set W → Set W) (a c : Set W) : a ∈ Writer.log (conj φ (att₁ <$> Writer.mk a []) (att₂ <$> Writer.mk c [a])) ↔ ¬φ (att₁ a) a

With hole attitudes, the compound (37) Bill believes that Fred has been beating Zelda, and furthermore, Bill believes that Fred has stopped beating Zelda, or (42) with hope as the second attitude, presupposes that Fred has been beating Zelda unless believing it filters it, which under entailment takes a veridical belief.

theorem Karttunen1973.log_map_conj {W : Type u} (att : Set W → Set W) (a c : Set W) : Writer.log (att <$> conj (fun (x1 x2 : Set W) => x1 ⊆ x2) (Writer.mk a []) (Writer.mk c [a])) = []

In (39) Bill believes that Fred has been beating Zelda, and furthermore, that Fred has stopped beating her, the filter applies inside the complement, and nothing is presupposed whether the verb is a hole or a plug.

theorem Karttunen1973.val_map_box_conj {W : Type u} (φ : Set W → Set W → Prop) (R : SetRel W W) (A B : Presupposing W (Set W)) : Writer.val (R.core <$> conj φ A B) = Writer.val (conj φ (R.core <$> A) (R.core <$> B))

With belief as necessity over the believer's doxastic alternatives, (37) and (39) assert the same ([Hin62]), which is the equivalence (38), so a hole believe is saved on (37) only by the equivalence.

theorem Karttunen1973.log_conj_pure {W : Type u} (φ : Set W → Set W → Prop) (att₁ att₂ : Set W → Set W) (A B : Presupposing W (Set W)) : Writer.log (conj φ (pure (att₁ (Writer.val A))) (pure (att₂ (Writer.val B)))) = []

(42) as the conjunction of two distinct attitudes (43) admits no such equivalence; as plugs, the attitudes leave it presupposing nothing, the paper's tentative verdict for the class.