Beaver and Krahmer's partial account of presupposition projection

This file formalizes Beaver and Krahmer's defense of trivalent presupposition projection: a lexical trigger contributes its complement through Blamey's transplication, and the strong, middle and weak Kleene connectives each make rigid, distinct projection predictions, none of which fits all of Soames's disjunctions. Flexibility is restored by the assertion operator — the floating-A theory derives cancellation as the preferred placement of meta-assertions — and a Stalnakerian update relation turns the partial semantics into a dynamic account of accommodation.

Main statements

• strong_conditional_presupposition, middle_conditional_filters, weak_conditional_cumulative: the three conditionals project a disjunctively weakened, a filtered, and a cumulative presupposition.
• no_disjunction_table_projects_and_cancels, no_kleene_fits_soames_disjunctions: no trivalent disjunction covers both projection and cancellation, and each of the three logics mispredicts some printed example.
• printed_predictions, printed_verdicts: the presuppositions the paper prints for each logic are the ones the semantics computes, and its verdicts are agreement with the intuitive presupposition.
• KingOfFrance.denial_presupposes_nothing, StoppedOrStarted.basic_undefined, regret_conditional_presupposes_nothing, floating_a_rows: the floating-A theory's preferred translations are unique and derive the cancellation readings.
• update_iff, hearer_update_filters_then_asserts, monologue: the paper's update relation is the substrate's Heimian partial update of a trivalent proposition, hearer accommodation is its image over candidate common grounds, and a monologue composes by sequencing.

Implementation notes

• Atomic formulas are bivalent, as the paper's valuations are, so a formula is undefined only through presupposition failure. The three logics index one connective constructor, so that the floating-A machinery counts surface occurrences; the paper's definitions of the middle and weak connectives in strong Kleene terms are theorems.
• Transplication is defined by the paper's own interdefinability formula over ∂, which is p ⊔ 0 on values. The assertion operator A is ofProp (a = 1) and meta-denial is its composite with negation.
• Incoherence counts non-presuppositional subformula occurrences. Reproducing the paper's printed degrees requires not substituting inside the argument of an assertion operator, which the text leaves open; the literal reading changes the degrees but no preference verdict. The preference order reads "optimal, then fewest assertions" lexicographically.
• The schematizations of the Soames disjunctions follow the paper's own schema for the stopped-or-started example; the judgments and printed predictions are the rows of Data/Examples/BeaverKrahmer2001.json.
• Not modelled: the partial type theory of §3 (partial assignments live in Logic/Assignment.lean), the Montagovian fragment of §4 and the appendix's optimal trees, and the plausibility grading sketched for the weighing-scale example.

TODO

• The quantifier rows of the paper's Fact 2: meta-assertion commutes with the strong Kleene quantifiers, but a strong Kleene universal as an infimum over SignType has no substrate home yet.

References

• D. Beaver, E. Krahmer, A Partial Account of Presupposition Projection (2001)
• S. Blamey, Partial Logic (1986)
• D. A. Bochvar, On a Three-valued Logical Calculus and Its Application to the Analysis of the Paradoxes of the Classical Extended Functional Calculus (1938)
• D. Beaver, The Kinematics of Presupposition (1992)
• S. C. Kleene, Introduction to Metamathematics (1952)
• S. Peters, A Truth-Conditional Formulation of Karttunen's Account of Presupposition (1979)
• E. Krahmer, Partiality and Dynamics (1994)
• D. T. Langendoen, H. B. Savin, The Projection Problem for Presuppositions (1971)
• S. Soames, A Projection Problem for Speaker Presuppositions (1979)
• G. Link, Prespie in Pragmatic Wonderland or: The Projection Problem for Presuppositions Revisited (1986)
• L. Karttunen, Presuppositions of Compound Sentences (1973)
• D. Lewis, Scorekeeping in a Language Game (1979)
• R. C. Stalnaker, Pragmatic Presuppositions (1974)
• I. Heim, On the Projection Problem for Presuppositions (1983)
• D. Beaver, Presupposition and Assertion in Dynamic Semantics (2001)
• R. Muskens, Meaning and Partiality (1995)

Transplication, assertion, denial

The binary presupposition operator is [Bla86]'s transplication. The unary ∂ it is interdefinable with is Beaver's ([Bea92]); it keeps truth and sends falsity to the gap, so ∂p is p ⊔ 0. The assertion operator A is Bochvar's ([Boc38]); it says that its argument is true, so Aa is ofProp (a = 1).

def BeaverKrahmer2001.transplicate (a p : SignType) : SignType

Transplication φ⟨π⟩ attaches the elementary presupposition π to φ, by the paper's interdefinability formula (∂π ∧ φ) ∨ ¬∂π over the strong Kleene connectives.

Equations

• BeaverKrahmer2001.transplicate a p = max (min (max p 0) a) (-max p 0)

theorem BeaverKrahmer2001.transplicate_eq_one_iff (a p : SignType) : transplicate a p = 1 ↔ p = 1 ∧ a = 1

theorem BeaverKrahmer2001.transplicate_eq_neg_one_iff (a p : SignType) : transplicate a p = -1 ↔ p = 1 ∧ a = -1

theorem BeaverKrahmer2001.transplicate_eq_zero_iff (a p : SignType) : transplicate a p = 0 ↔ p ≠ 1 ∨ a = 0

def BeaverKrahmer2001.metaDeny (a : SignType) : SignType

Meta-denial asserts falsity, D = A ∘ ¬.

Equations

• BeaverKrahmer2001.metaDeny a = SignType.ofProp (-a = 1)

def BeaverKrahmer2001.presupVal (a : SignType) : SignType

The maximal presupposition of a value is that it is defined, P = A ∨ D.

Equations

• BeaverKrahmer2001.presupVal a = max (SignType.ofProp (a = 1)) (BeaverKrahmer2001.metaDeny a)

theorem BeaverKrahmer2001.presupVal_eq_one_iff (a : SignType) : presupVal a = 1 ↔ a ≠ 0

theorem BeaverKrahmer2001.presupVal_ne_zero (a : SignType) : presupVal a ≠ 0

The maximal presupposition is a classical value.

The three Kleene logics

Strong Kleene is the lattice structure of SignType; the middle (Peters) and weak (Bochvar-internal) connectives are SignType.meetMiddle and SignType.meetWeak with their joins ([Pet79]; the name middle Kleene is [Kra94]'s). The conditional of each logic is the derived form ¬a ∨ b.

inductive BeaverKrahmer2001.Kleene : Type

• strong : Kleene
• middle : Kleene
• weak : Kleene

@[instance_reducible]

instance BeaverKrahmer2001.instDecidableEqKleene : DecidableEq Kleene

Equations

• BeaverKrahmer2001.instDecidableEqKleene x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaverKrahmer2001.instFintypeKleene : Fintype Kleene

Equations

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

def BeaverKrahmer2001.instReprKleene.repr : Kleene → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaverKrahmer2001.instReprKleene : Repr Kleene

Equations

• BeaverKrahmer2001.instReprKleene = { reprPrec := BeaverKrahmer2001.instReprKleene.repr }

inductive BeaverKrahmer2001.Connective : Type

• conj : Connective
• disj : Connective
• imp : Connective

@[instance_reducible]

instance BeaverKrahmer2001.instDecidableEqConnective : DecidableEq Connective

Equations

• BeaverKrahmer2001.instDecidableEqConnective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaverKrahmer2001.instFintypeConnective : Fintype Connective

Equations

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

@[instance_reducible]

instance BeaverKrahmer2001.instReprConnective : Repr Connective

Equations

• BeaverKrahmer2001.instReprConnective = { reprPrec := BeaverKrahmer2001.instReprConnective.repr }

def BeaverKrahmer2001.instReprConnective.repr : Connective → ℕ → Std.Format

Equations

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

def BeaverKrahmer2001.Kleene.meet : Kleene → SignType → SignType → SignType

The conjunction of each logic.

Equations

• BeaverKrahmer2001.Kleene.strong.meet = fun (x1 x2 : SignType) => min x1 x2
• BeaverKrahmer2001.Kleene.middle.meet = SignType.meetMiddle
• BeaverKrahmer2001.Kleene.weak.meet = SignType.meetWeak

def BeaverKrahmer2001.Kleene.join : Kleene → SignType → SignType → SignType

The disjunction of each logic.

Equations

• BeaverKrahmer2001.Kleene.strong.join = fun (x1 x2 : SignType) => max x1 x2
• BeaverKrahmer2001.Kleene.middle.join = SignType.joinMiddle
• BeaverKrahmer2001.Kleene.weak.join = SignType.joinWeak

def BeaverKrahmer2001.Connective.eval : Connective → Kleene → SignType → SignType → SignType

The truth table of a connective in a logic, with the conditional the derived ¬a ∨ b; the tables match the paper's for all three logics.

Equations

• BeaverKrahmer2001.Connective.conj.eval x✝ = x✝.meet
• BeaverKrahmer2001.Connective.disj.eval x✝ = x✝.join
• BeaverKrahmer2001.Connective.imp.eval x✝ = fun (a b : SignType) => x✝.join (-a) b

def BeaverKrahmer2001.Kleene.connectives (k : Kleene) : Trivalent.Connectives

The connectives of each logic as the substrate's truth tables, with the conditional ¬a ∨ b; these are the strong, Middle and Weak Kleene connectives (Kleene.connectives_strong, …).

Equations

• k.connectives = { conj := k.meet, disj := k.join, cond := fun (a b : SignType) => k.join (-a) b }

theorem BeaverKrahmer2001.Kleene.connectives_strong : strong.connectives = Trivalent.Connectives.strongKleene

theorem BeaverKrahmer2001.Kleene.connectives_middle : middle.connectives = Trivalent.Connectives.middleKleene

theorem BeaverKrahmer2001.Kleene.connectives_weak : weak.connectives = Trivalent.Connectives.weakKleene

theorem BeaverKrahmer2001.meetMiddle_eq (a b : SignType) : a.meetMiddle b = max (min a b) (min a (-a))

The middle conjunction in strong Kleene terms.

theorem BeaverKrahmer2001.joinMiddle_eq (a b : SignType) : a.joinMiddle b = min (max a b) (max a (-a))

The middle disjunction in strong Kleene terms.

theorem BeaverKrahmer2001.impMiddle_eq (a b : SignType) : Connective.imp.eval Kleene.middle a b = min (max (-a) b) (max a (-a))

The middle conditional in strong Kleene terms.

theorem BeaverKrahmer2001.meetWeak_eq (a b : SignType) : a.meetWeak b = max (max (min a b) (min a (-a))) (min b (-b))

The weak conjunction in strong Kleene terms.

theorem BeaverKrahmer2001.joinWeak_eq (a b : SignType) : a.joinWeak b = min (min (max a b) (max a (-a))) (max b (-b))

The weak disjunction in strong Kleene terms.

theorem BeaverKrahmer2001.impWeak_eq (a b : SignType) : Connective.imp.eval Kleene.weak a b = min (min (max (-a) b) (max a (-a))) (max b (-b))

The weak conditional in strong Kleene terms.

Projection at the value level

theorem BeaverKrahmer2001.presupVal_neg (a : SignType) : presupVal (-a) = presupVal a

Negation projects presuppositions unchanged, P¬φ = Pφ.

theorem BeaverKrahmer2001.presupVal_transplicate (a p : SignType) : presupVal (transplicate a p) = min (SignType.ofProp (p = 1)) (presupVal a)

A transplication presupposes its subscript and whatever its body presupposes, P(φ⟨π⟩) = Aπ ∧ Pφ.

theorem BeaverKrahmer2001.presupVal_imp_strong (a b : SignType) : presupVal (Connective.imp.eval Kleene.strong a b) = min (max (presupVal a) (SignType.ofProp (b = 1))) (max (metaDeny a) (presupVal b))

theorem BeaverKrahmer2001.presupVal_imp_middle (a b : SignType) : presupVal (Connective.imp.eval Kleene.middle a b) = min (presupVal a) (max (metaDeny a) (presupVal b))

theorem BeaverKrahmer2001.presupVal_imp_weak (a b : SignType) : presupVal (Connective.imp.eval Kleene.weak a b) = min (presupVal a) (presupVal b)

theorem BeaverKrahmer2001.presupVal_join_strong (a b : SignType) : presupVal (max a b) = min (max (presupVal a) (SignType.ofProp (b = 1))) (max (presupVal b) (SignType.ofProp (a = 1)))

The strong disjunction projects conditionalized presuppositions.

theorem BeaverKrahmer2001.presupVal_join_middle (a b : SignType) : presupVal (a.joinMiddle b) = min (presupVal a) (max (SignType.ofProp (a = 1)) (presupVal b))

The middle disjunction projects the left disjunct's presupposition.

theorem BeaverKrahmer2001.presupVal_join_weak (a b : SignType) : presupVal (a.joinWeak b) = min (presupVal a) (presupVal b)

The weak disjunction projects every presupposition.

def BeaverKrahmer2001.cancelNeg : SignType → SignType

Bochvar's cancelling (external) negation.

Equations

• BeaverKrahmer2001.cancelNeg SignType.pos = -1
• BeaverKrahmer2001.cancelNeg SignType.neg = 1
• BeaverKrahmer2001.cancelNeg SignType.zero = 1

theorem BeaverKrahmer2001.cancelNeg_eq_neg_metaAssert (a : SignType) : cancelNeg a = -SignType.ofProp (a = 1)

Cancelling negation is ordinary negation over an assertion, ∼φ = ¬Aφ.

theorem BeaverKrahmer2001.no_disjunction_table_projects_and_cancels : ¬∃ (f : SignType → SignType → SignType), (∀ (π γ δ : Bool), f (transplicate (SignType.ofProp (γ = true)) (SignType.ofProp (π = true))) (SignType.ofProp (δ = true)) ≠ 0 ↔ π = true) ∧ ∀ (π γ : Bool), f (transplicate (SignType.ofProp (γ = true)) (SignType.ofProp (π = true))) (-SignType.ofProp (π = true)) ≠ 0

No single trivalent disjunction both projects the left disjunct's presupposition and cancels it against a denying right disjunct, on the paper's own schema for the Soames disjunctions.

Formulas

One language hosts all three logics: a connective node carries its Kleene index, so the floating-A machinery below counts occurrences of the surface form rather than of a strong Kleene expansion. Valuations are bivalent, so only presupposition failure makes a formula undefined.

inductive BeaverKrahmer2001.Formula (Atom : Type u_1) : Type u_1

• atom {Atom : Type u_1} : Atom → Formula Atom
• neg {Atom : Type u_1} : Formula Atom → Formula Atom
• conn {Atom : Type u_1} : Connective → Kleene → Formula Atom → Formula Atom → Formula Atom
• transpl {Atom : Type u_1} : Formula Atom → Formula Atom → Formula Atom
• assert {Atom : Type u_1} : Formula Atom → Formula Atom

def BeaverKrahmer2001.instDecidableEqFormula.decEq {Atom✝ : Type u_1} [DecidableEq Atom✝] (x✝ x✝¹ : Formula Atom✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.atom a) (BeaverKrahmer2001.Formula.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.atom a) a_1.neg = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.atom a) (BeaverKrahmer2001.Formula.conn a_1 a_2 a_3 a_4) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.atom a) (a_1.transpl a_2) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.atom a) a_1.assert = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.neg (BeaverKrahmer2001.Formula.atom a_1) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.neg b.neg = if h : a = b then h ▸ have inst := BeaverKrahmer2001.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.neg (BeaverKrahmer2001.Formula.conn a_1 a_2 a_3 a_4) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.neg (a_1.transpl a_2) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.neg a_1.assert = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.conn a a_1 a_2 a_3) (BeaverKrahmer2001.Formula.atom a_4) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.conn a a_1 a_2 a_3) a_4.neg = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.conn a a_1 a_2 a_3) (a_4.transpl a_5) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (BeaverKrahmer2001.Formula.conn a a_1 a_2 a_3) a_4.assert = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (a.transpl a_1) (BeaverKrahmer2001.Formula.atom a_2) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (a.transpl a_1) a_2.neg = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (a.transpl a_1) (BeaverKrahmer2001.Formula.conn a_2 a_3 a_4 a_5) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq (a.transpl a_1) a_2.assert = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.assert (BeaverKrahmer2001.Formula.atom a_1) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.assert a_1.neg = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.assert (BeaverKrahmer2001.Formula.conn a_1 a_2 a_3 a_4) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.assert (a_1.transpl a_2) = isFalse ⋯
• BeaverKrahmer2001.instDecidableEqFormula.decEq a.assert b.assert = if h : a = b then h ▸ have inst := BeaverKrahmer2001.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaverKrahmer2001.instDecidableEqFormula {Atom✝ : Type u_1} [DecidableEq Atom✝] : DecidableEq (Formula Atom✝)

Equations

• BeaverKrahmer2001.instDecidableEqFormula = BeaverKrahmer2001.instDecidableEqFormula.decEq

@[instance_reducible]

instance BeaverKrahmer2001.instReprFormula {Atom✝ : Type u_1} [Repr Atom✝] : Repr (Formula Atom✝)

Equations

• BeaverKrahmer2001.instReprFormula = { reprPrec := BeaverKrahmer2001.instReprFormula.repr }

def BeaverKrahmer2001.instReprFormula.repr {Atom✝ : Type u_1} [Repr Atom✝] : Formula Atom✝ → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev BeaverKrahmer2001.Valuation (Atom : Type u_1) : Type u_1

A bivalent valuation of the atoms.

Equations

• BeaverKrahmer2001.Valuation Atom = (Atom → Bool)

def BeaverKrahmer2001.Formula.eval {Atom : Type u_1} (V : Valuation Atom) : Formula Atom → SignType

Evaluation into three-valued truth.

Equations

• BeaverKrahmer2001.Formula.eval V (BeaverKrahmer2001.Formula.atom a) = SignType.ofProp (V a = true)
• BeaverKrahmer2001.Formula.eval V φ.neg = -BeaverKrahmer2001.Formula.eval V φ
• BeaverKrahmer2001.Formula.eval V (BeaverKrahmer2001.Formula.conn c k φ ψ) = c.eval k (BeaverKrahmer2001.Formula.eval V φ) (BeaverKrahmer2001.Formula.eval V ψ)
• BeaverKrahmer2001.Formula.eval V (φ.transpl π) = BeaverKrahmer2001.transplicate (BeaverKrahmer2001.Formula.eval V φ) (BeaverKrahmer2001.Formula.eval V π)
• BeaverKrahmer2001.Formula.eval V φ.assert = SignType.ofProp (BeaverKrahmer2001.Formula.eval V φ = 1)

@[simp]

theorem BeaverKrahmer2001.Formula.eval_atom {Atom : Type u_1} (V : Valuation Atom) (a : Atom) : eval V (atom a) = SignType.ofProp (V a = true)

@[simp]

theorem BeaverKrahmer2001.Formula.eval_neg {Atom : Type u_1} (V : Valuation Atom) (φ : Formula Atom) : eval V φ.neg = -eval V φ

@[simp]

theorem BeaverKrahmer2001.Formula.eval_conn {Atom : Type u_1} (V : Valuation Atom) (c : Connective) (k : Kleene) (φ ψ : Formula Atom) : eval V (conn c k φ ψ) = c.eval k (eval V φ) (eval V ψ)

@[simp]

theorem BeaverKrahmer2001.Formula.eval_transpl {Atom : Type u_1} (V : Valuation Atom) (φ π : Formula Atom) : eval V (φ.transpl π) = transplicate (eval V φ) (eval V π)

@[simp]

theorem BeaverKrahmer2001.Formula.eval_assert {Atom : Type u_1} (V : Valuation Atom) (φ : Formula Atom) : eval V φ.assert = SignType.ofProp (eval V φ = 1)

def BeaverKrahmer2001.Formula.ofFormula {Atom : Type u_1} (k : Kleene) : Trivalent.Formula Atom → Formula Atom

The substrate's formulas embed, with every connective read in one logic.

Equations

• One or more equations did not get rendered due to their size.
• BeaverKrahmer2001.Formula.ofFormula k (Trivalent.Formula.atom a) = BeaverKrahmer2001.Formula.atom a
• BeaverKrahmer2001.Formula.ofFormula k φ.neg = (BeaverKrahmer2001.Formula.ofFormula k φ).neg

theorem BeaverKrahmer2001.Formula.eval_ofFormula {Atom : Type u_1} (k : Kleene) (V : Valuation Atom) (φ : Trivalent.Formula Atom) : eval V (ofFormula k φ) = Trivalent.Formula.eval k.connectives (Trivalent.Model.ofBool V) φ

On a bivalent valuation, a formula whose connectives are all read in one logic evaluates as the substrate does under that logic's connectives.

def BeaverKrahmer2001.Formula.deny {Atom : Type u_1} (φ : Formula Atom) : Formula Atom

Meta-denial at formula level is Dφ = A¬φ.

Equations

• φ.deny = φ.neg.assert

def BeaverKrahmer2001.Formula.presup {Atom : Type u_1} (φ : Formula Atom) : Formula Atom

The maximal presupposition as a formula is Pφ = Aφ ∨ Dφ.

Equations

• φ.presup = BeaverKrahmer2001.Formula.conn BeaverKrahmer2001.Connective.disj BeaverKrahmer2001.Kleene.strong φ.assert φ.deny

theorem BeaverKrahmer2001.Formula.eval_presup {Atom : Type u_1} (V : Valuation Atom) (φ : Formula Atom) : eval V φ.presup = presupVal (eval V φ)

theorem BeaverKrahmer2001.Formula.presup_ne_zero {Atom : Type u_1} (V : Valuation Atom) (φ : Formula Atom) : eval V φ.presup ≠ 0

The maximal presupposition evaluates classically, so rewriting by the assertion algebra yields a transplication-free formula.

def BeaverKrahmer2001.Formula.Equiv {Atom : Type u_1} (φ ψ : Formula Atom) : Prop

Two formulas are equivalent when they evaluate alike at every valuation.

Equations

• φ.Equiv ψ = ∀ (V : BeaverKrahmer2001.Valuation Atom), BeaverKrahmer2001.Formula.eval V φ = BeaverKrahmer2001.Formula.eval V ψ

def BeaverKrahmer2001.Formula.Entails {Atom : Type u_1} (φ ψ : Formula Atom) : Prop

Entailment preserves truth.

Equations

• φ.Entails ψ = ∀ (V : BeaverKrahmer2001.Valuation Atom), BeaverKrahmer2001.Formula.eval V φ = 1 → BeaverKrahmer2001.Formula.eval V ψ = 1

def BeaverKrahmer2001.Formula.Presupposes {Atom : Type u_1} (φ π : Formula Atom) : Prop

φ presupposes π when φ is undefined wherever π is untrue.

Equations

• φ.Presupposes π = ∀ (V : BeaverKrahmer2001.Valuation Atom), BeaverKrahmer2001.Formula.eval V π ≠ 1 → BeaverKrahmer2001.Formula.eval V φ = 0

@[instance_reducible]

instance BeaverKrahmer2001.Formula.instDecidableEquiv {Atom : Type u_1} [Fintype Atom] [DecidableEq Atom] {φ ψ : Formula Atom} : Decidable (φ.Equiv ψ)

Equations

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

@[instance_reducible]

instance BeaverKrahmer2001.Formula.instDecidableEntails {Atom : Type u_1} [Fintype Atom] [DecidableEq Atom] {φ ψ : Formula Atom} : Decidable (φ.Entails ψ)

Equations

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

@[instance_reducible]

instance BeaverKrahmer2001.Formula.instDecidablePresupposes {Atom : Type u_1} [Fintype Atom] [DecidableEq Atom] {φ ψ : Formula Atom} : Decidable (φ.Presupposes ψ)

Equations

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

theorem BeaverKrahmer2001.Formula.disj_strong_eq {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.disj Kleene.strong φ ψ).Equiv (conn Connective.conj Kleene.strong φ.neg ψ.neg).neg

Disjunction is derived in the strong logic as φ ∨ ψ = ¬(¬φ ∧ ¬ψ).

theorem BeaverKrahmer2001.Formula.imp_eq {Atom : Type u_1} (k : Kleene) (φ ψ : Formula Atom) : (conn Connective.imp k φ ψ).Equiv (conn Connective.disj k φ.neg ψ)

The conditional of every logic is ¬φ ∨ ψ in that logic.

theorem BeaverKrahmer2001.Formula.conj_middle_eq {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.conj Kleene.middle φ ψ).Equiv (conn Connective.disj Kleene.strong (conn Connective.conj Kleene.strong φ ψ) (conn Connective.conj Kleene.strong φ φ.neg))

The middle conjunction is a strong Kleene compound of its arguments.

theorem BeaverKrahmer2001.Formula.conj_weak_eq {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.conj Kleene.weak φ ψ).Equiv (conn Connective.disj Kleene.strong (conn Connective.disj Kleene.strong (conn Connective.conj Kleene.strong φ ψ) (conn Connective.conj Kleene.strong φ φ.neg)) (conn Connective.conj Kleene.strong ψ ψ.neg))

The weak conjunction is a strong Kleene compound of its arguments.

theorem BeaverKrahmer2001.Formula.presupposes_iff_entails {Atom : Type u_1} (φ π : Formula Atom) : φ.Presupposes π ↔ (conn Connective.disj Kleene.strong φ φ.neg).Entails π

Semantic presupposition is entailment by the disjunction of truth and falsity conditions, so φ presupposes π iff φ ∨ ¬φ ⊨ π.

theorem BeaverKrahmer2001.Formula.presupposes_presup {Atom : Type u_1} (φ : Formula Atom) : φ.Presupposes φ.presup

Pφ is a presupposition of φ.

theorem BeaverKrahmer2001.Formula.presup_strongest {Atom : Type u_1} {φ π : Formula Atom} (h : φ.Presupposes π) : φ.presup.Entails π

Pφ is the maximal presupposition, entailing every presupposition of φ.

The assertion algebra

The twelve equivalences of the paper's Fact 1 rewrite A and D through every constructor, so Pφ reduces to a transplication-free classical formula. Under eval, A is ofProp (a = 1) and the ∂ inside a transplication is p ⊔ 0, so each row is an identity between those expressions.

theorem BeaverKrahmer2001.Formula.assert_atom {Atom : Type u_1} (a : Atom) : (atom a).assert.Equiv (atom a)

theorem BeaverKrahmer2001.Formula.deny_atom {Atom : Type u_1} (a : Atom) : (atom a).deny.Equiv (atom a).neg

theorem BeaverKrahmer2001.Formula.assert_neg {Atom : Type u_1} (φ : Formula Atom) : φ.neg.assert.Equiv φ.deny

theorem BeaverKrahmer2001.Formula.deny_neg {Atom : Type u_1} (φ : Formula Atom) : φ.neg.deny.Equiv φ.assert

theorem BeaverKrahmer2001.Formula.assert_conj {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.conj Kleene.strong φ ψ).assert.Equiv (conn Connective.conj Kleene.strong φ.assert ψ.assert)

theorem BeaverKrahmer2001.Formula.deny_conj {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.conj Kleene.strong φ ψ).deny.Equiv (conn Connective.disj Kleene.strong φ.deny ψ.deny)

theorem BeaverKrahmer2001.Formula.assert_disj {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.disj Kleene.strong φ ψ).assert.Equiv (conn Connective.disj Kleene.strong φ.assert ψ.assert)

theorem BeaverKrahmer2001.Formula.deny_disj {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.disj Kleene.strong φ ψ).deny.Equiv (conn Connective.conj Kleene.strong φ.deny ψ.deny)

theorem BeaverKrahmer2001.Formula.assert_imp {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.imp Kleene.strong φ ψ).assert.Equiv (conn Connective.disj Kleene.strong φ.deny ψ.assert)

theorem BeaverKrahmer2001.Formula.deny_imp {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.imp Kleene.strong φ ψ).deny.Equiv (conn Connective.conj Kleene.strong φ.assert ψ.deny)

theorem BeaverKrahmer2001.Formula.assert_transpl {Atom : Type u_1} (φ π : Formula Atom) : (φ.transpl π).assert.Equiv (conn Connective.conj Kleene.strong π.assert φ.assert)

theorem BeaverKrahmer2001.Formula.deny_transpl {Atom : Type u_1} (φ π : Formula Atom) : (φ.transpl π).deny.Equiv (conn Connective.conj Kleene.strong π.assert φ.deny)

theorem BeaverKrahmer2001.Formula.eval_neg_assert {Atom : Type u_1} (V : Valuation Atom) (φ : Formula Atom) : eval V φ.assert.neg = cancelNeg (eval V φ)

Cancelling negation at formula level is negation over an assertion.

Projection at formula level

theorem BeaverKrahmer2001.Formula.presup_neg {Atom : Type u_1} (φ : Formula Atom) : φ.neg.presup.Equiv φ.presup

Negation projects presuppositions unchanged.

theorem BeaverKrahmer2001.Formula.presup_transpl {Atom : Type u_1} (φ π : Formula Atom) : (φ.transpl π).presup.Equiv (conn Connective.conj Kleene.strong π.assert φ.presup)

A transplication presupposes its subscript on top of its body's presupposition.

theorem BeaverKrahmer2001.Formula.strong_conditional_presupposition {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.imp Kleene.strong φ ψ).presup.Equiv (conn Connective.conj Kleene.strong (conn Connective.disj Kleene.strong φ.presup ψ.assert) (conn Connective.disj Kleene.strong φ.deny ψ.presup))

The strong conditional projects only a disjunctively weakened presupposition, the famous too-weak prediction for a presupposing antecedent.

theorem BeaverKrahmer2001.Formula.middle_conditional_filters {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.imp Kleene.middle φ ψ).presup.Equiv (conn Connective.conj Kleene.strong φ.presup (conn Connective.disj Kleene.strong φ.deny ψ.presup))

The middle conditional filters. The antecedent's presupposition projects intact, and the consequent's survives unless the antecedent is denied.

theorem BeaverKrahmer2001.Formula.weak_conditional_cumulative {Atom : Type u_1} (φ ψ : Formula Atom) : (conn Connective.imp Kleene.weak φ ψ).presup.Equiv (conn Connective.conj Kleene.strong φ.presup ψ.presup)

The weak conditional is cumulative, projecting every elementary presupposition, which is the analysis of [LS71].

The floating-A theory

A sentence's translation set keeps or meta-asserts each transplication; the preferred translations are the defined ones of least incoherence, and of those the ones with fewest assertions ([Lin86] supplies the ingredients). Incoherence counts the non-presuppositional subformula occurrences whose replacement by a tautology or a contradiction preserves the truth conditions; occurrences inside a subscript or inside an assertion are not substituted.

def BeaverKrahmer2001.Formula.translations {Atom : Type u_1} : Formula Atom → List (Formula Atom)

The translation set keeps or meta-asserts each transplication.

Equations

• One or more equations did not get rendered due to their size.
• (BeaverKrahmer2001.Formula.atom a).translations = [BeaverKrahmer2001.Formula.atom a]
• φ.neg.translations = List.map BeaverKrahmer2001.Formula.neg φ.translations
• φ.assert.translations = List.map BeaverKrahmer2001.Formula.assert φ.translations

def BeaverKrahmer2001.Formula.assertCount {Atom : Type u_1} : Formula Atom → ℕ

The number of assertion operators.

Equations

• (BeaverKrahmer2001.Formula.atom a).assertCount = 0
• φ.neg.assertCount = φ.assertCount
• (BeaverKrahmer2001.Formula.conn c k φ ψ).assertCount = φ.assertCount + ψ.assertCount
• (φ.transpl π).assertCount = φ.assertCount + π.assertCount
• φ.assert.assertCount = φ.assertCount + 1

def BeaverKrahmer2001.Formula.contexts {Atom : Type u_1} : Formula Atom → List (Formula Atom → Formula Atom)

contexts lists the one-hole contexts at the non-presuppositional occurrences, since subscripts and asserted material are not substitution sites.

Equations

• One or more equations did not get rendered due to their size.
• (BeaverKrahmer2001.Formula.atom a).contexts = [id]
• φ.neg.contexts = id :: List.map (fun (x : BeaverKrahmer2001.Formula Atom → BeaverKrahmer2001.Formula Atom) => BeaverKrahmer2001.Formula.neg ∘ x) φ.contexts
• φ.assert.contexts = [id]

def BeaverKrahmer2001.Formula.top {Atom : Type u_1} [Inhabited Atom] : Formula Atom

The language's own tautology.

Equations

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

def BeaverKrahmer2001.Formula.bot {Atom : Type u_1} [Inhabited Atom] : Formula Atom

The language's own contradiction.

Equations

• BeaverKrahmer2001.Formula.bot = BeaverKrahmer2001.Formula.top.neg

theorem BeaverKrahmer2001.Formula.eval_top {Atom : Type u_1} [Inhabited Atom] (V : Valuation Atom) : eval V top = 1

theorem BeaverKrahmer2001.Formula.eval_bot {Atom : Type u_1} [Inhabited Atom] (V : Valuation Atom) : eval V bot = -1

def BeaverKrahmer2001.Formula.TrueIff {Atom : Type u_1} (φ ψ : Formula Atom) : Prop

Two formulas are true together at every valuation.

Equations

• φ.TrueIff ψ = ∀ (V : BeaverKrahmer2001.Valuation Atom), BeaverKrahmer2001.Formula.eval V φ = 1 ↔ BeaverKrahmer2001.Formula.eval V ψ = 1

@[instance_reducible]

instance BeaverKrahmer2001.Formula.instDecidableTrueIff {Atom : Type u_1} [Fintype Atom] [DecidableEq Atom] {φ ψ : Formula Atom} : Decidable (φ.TrueIff ψ)

Equations

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

def BeaverKrahmer2001.Formula.nonInformativity {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] (φ : Formula Atom) : ℕ

The number of redundant substitution sites, those where replacement by the tautology preserves the truth conditions.

Equations

• φ.nonInformativity = List.countP (fun (k : BeaverKrahmer2001.Formula Atom → BeaverKrahmer2001.Formula Atom) => decide (φ.TrueIff (k BeaverKrahmer2001.Formula.top))) φ.contexts

def BeaverKrahmer2001.Formula.inconsistency {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] (φ : Formula Atom) : ℕ

The number of inconsistent substitution sites, those where replacement by the contradiction preserves the truth conditions.

Equations

• φ.inconsistency = List.countP (fun (k : BeaverKrahmer2001.Formula Atom → BeaverKrahmer2001.Formula Atom) => decide (φ.TrueIff (k BeaverKrahmer2001.Formula.bot))) φ.contexts

def BeaverKrahmer2001.Formula.incoherence {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] (φ : Formula Atom) : ℕ

Total incoherence is the sum of the two degrees.

Equations

• φ.incoherence = φ.nonInformativity + φ.inconsistency

def BeaverKrahmer2001.Formula.Defined {Atom : Type u_1} (φ : Formula Atom) : Prop

A formula is defined when it is somewhere classical.

Equations

• φ.Defined = ∃ (V : BeaverKrahmer2001.Valuation Atom), BeaverKrahmer2001.Formula.eval V φ ≠ 0

@[instance_reducible]

instance BeaverKrahmer2001.Formula.instDecidableDefined {Atom : Type u_1} [Fintype Atom] [DecidableEq Atom] {φ : Formula Atom} : Decidable φ.Defined

Equations

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

def BeaverKrahmer2001.Formula.Optimal {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] (S : List (Formula Atom)) (φ : Formula Atom) : Prop

A translation is optimal when it is defined and of least incoherence among the defined.

Equations

• BeaverKrahmer2001.Formula.Optimal S φ = (φ.Defined ∧ ∀ ψ ∈ S, ψ.Defined → φ.incoherence ≤ ψ.incoherence)

@[instance_reducible]

instance BeaverKrahmer2001.Formula.instDecidableOptimal {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] {S : List (Formula Atom)} {φ : Formula Atom} : Decidable (Optimal S φ)

Equations

• BeaverKrahmer2001.Formula.instDecidableOptimal = { decide := decide φ.Defined && decide (∀ ψ ∈ S, ψ.Defined → φ.incoherence ≤ ψ.incoherence), reflects_decide := ⋯ }

def BeaverKrahmer2001.Formula.rank {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] (S : List (Formula Atom)) (φ : Formula Atom) : Lex (Bool × ℕ)

The preference rank orders by optimality first and then by the number of assertions, lexicographically.

Equations

• BeaverKrahmer2001.Formula.rank S φ = toLex (decide ¬BeaverKrahmer2001.Formula.Optimal S φ, φ.assertCount)

def BeaverKrahmer2001.Formula.Prefers {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] (S : List (Formula Atom)) (γ δ : Formula Atom) : Prop

Prefers is the paper's γ ≺ δ.

Equations

• BeaverKrahmer2001.Formula.Prefers S γ δ = (BeaverKrahmer2001.Formula.rank S γ < BeaverKrahmer2001.Formula.rank S δ)

def BeaverKrahmer2001.Formula.Preferred {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] (S : List (Formula Atom)) (γ : Formula Atom) : Prop

A translation is preferred when nothing in the set is preferred over it.

Equations

• BeaverKrahmer2001.Formula.Preferred S γ = (γ ∈ S ∧ ∀ δ ∈ S, ¬BeaverKrahmer2001.Formula.Prefers S δ γ)

@[instance_reducible]

instance BeaverKrahmer2001.Formula.instDecidablePrefers {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] {S : List (Formula Atom)} {γ δ : Formula Atom} : Decidable (Prefers S γ δ)

Equations

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

@[instance_reducible]

instance BeaverKrahmer2001.Formula.instDecidablePreferred {Atom : Type u_1} [Inhabited Atom] [Fintype Atom] [DecidableEq Atom] {S : List (Formula Atom)} {γ : Formula Atom} : Decidable (Preferred S γ)

Equations

• BeaverKrahmer2001.Formula.instDecidablePreferred = { decide := decide (γ ∈ S) && decide (∀ δ ∈ S, ¬BeaverKrahmer2001.Formula.Prefers S δ γ), reflects_decide := ⋯ }

The paper's atoms and worked cancellations

One four-element atom type hosts every schematized example; the subscript atom is p throughout, the prejacent bodies are q and r.

inductive BeaverKrahmer2001.Atom : Type

• p : Atom
• q : Atom
• r : Atom
• s : Atom

@[instance_reducible]

instance BeaverKrahmer2001.instDecidableEqAtom : DecidableEq Atom

Equations

• BeaverKrahmer2001.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaverKrahmer2001.instFintypeAtom : Fintype Atom

Equations

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

def BeaverKrahmer2001.instReprAtom.repr : Atom → ℕ → Std.Format

Equations

• BeaverKrahmer2001.instReprAtom.repr BeaverKrahmer2001.Atom.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BeaverKrahmer2001.Atom.p")).group prec✝
• BeaverKrahmer2001.instReprAtom.repr BeaverKrahmer2001.Atom.q prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BeaverKrahmer2001.Atom.q")).group prec✝
• BeaverKrahmer2001.instReprAtom.repr BeaverKrahmer2001.Atom.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BeaverKrahmer2001.Atom.r")).group prec✝
• BeaverKrahmer2001.instReprAtom.repr BeaverKrahmer2001.Atom.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BeaverKrahmer2001.Atom.s")).group prec✝

@[instance_reducible]

instance BeaverKrahmer2001.instReprAtom : Repr Atom

Equations

• BeaverKrahmer2001.instReprAtom = { reprPrec := BeaverKrahmer2001.instReprAtom.repr }

@[instance_reducible]

instance BeaverKrahmer2001.instInhabitedAtom : Inhabited Atom

Equations

• BeaverKrahmer2001.instInhabitedAtom = { default := BeaverKrahmer2001.instInhabitedAtom.default }

The king of France is not bald, since there is no king of France denies a presupposing sentence and its presupposition together.

def BeaverKrahmer2001.KingOfFrance.basic : Formula Atom

The basic translation ¬(q⟨p⟩) ∧̈ ¬p, nowhere true and incoherent.

Equations

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

def BeaverKrahmer2001.KingOfFrance.preferred : Formula Atom

The preferred translation meta-asserts the presupposing conjunct.

Equations

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

theorem BeaverKrahmer2001.KingOfFrance.denial_presupposes_nothing (V : Valuation Atom) : Formula.eval V preferred.presup = 1

The preferred translation of the denial presupposes nothing, so cancellation is derived.

In Either Bill has just stopped smoking, or else he's just started smoking the two disjuncts carry inconsistent presuppositions.

def BeaverKrahmer2001.StoppedOrStarted.basic : Formula Atom

The basic translation q⟨p⟩ ∨̈ r⟨¬p⟩.

Equations

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

def BeaverKrahmer2001.StoppedOrStarted.preferred : Formula Atom

The preferred translation meta-asserts both disjuncts.

Equations

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

theorem BeaverKrahmer2001.StoppedOrStarted.basic_undefined : ¬basic.Defined

The basic translation presupposes a contradiction, so it is nowhere defined.

In If Mary is sad, then Bill regrets that Mary is sad the antecedent satisfies the consequent's presupposition.

def BeaverKrahmer2001.SadRegret.basic : Formula Atom

The basic translation p →̈ q⟨p⟩.

Equations

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

def BeaverKrahmer2001.SadRegret.preferred : Formula Atom

The preferred translation meta-asserts the consequent.

Equations

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

theorem BeaverKrahmer2001.SadRegret.regret_conditional_presupposes_nothing (V : Valuation Atom) : Formula.eval V preferred.presup = 1

Although the weak conditional is cumulative, the preferred translation presupposes nothing, so the conditional's apparent presupposition is filtered by preference.

theorem BeaverKrahmer2001.prefers_not_total : ∃ (S : List (Formula Atom)) (γ : Formula Atom) (δ : Formula Atom), γ ≠ δ ∧ γ ∈ S ∧ δ ∈ S ∧ ¬Formula.Prefers S γ δ ∧ ¬Formula.Prefers S δ γ

Preference is not a total order, since two optimal translations with equally many assertions tie.

Update and accommodation

The paper's update relation is the substrate's Heimian partial update of a trivalent proposition (CCP.Partial.ofTrivalent), its domain condition the presupposition operator and its output the meta-asserted content; the hearer-side update⋆ over candidate common grounds is its PFun.image, and a monologue composes by sequencing. Accommodation, after [Lew79c] and [Sta74], is the filtering this image performs.

theorem BeaverKrahmer2001.update_iff {W : Type u_1} (ξ : W → SignType) (σ τ : Set W) : (σ, τ) ∈ PFun.graph' (DynamicSemantics.CCP.Partial.ofTrivalent ξ) ↔ σ ⊆ {i : W | presupVal (ξ i) = 1} ∧ τ = σ ∩ {i : W | SignType.ofProp (ξ i = 1) = 1}

The paper's update ξ σ τ says, in its own vocabulary, that σ supports the presupposition P ∘ ξ throughout and that τ is σ intersected with the asserted content A ∘ ξ.

theorem BeaverKrahmer2001.hearer_update {W : Type u_1} (ξ : W → SignType) (cgs : Set (Set W)) (τ : Set W) : τ ∈ PFun.image (DynamicSemantics.CCP.Partial.ofTrivalent ξ) cgs ↔ ∃ σ ∈ cgs, (σ, τ) ∈ PFun.graph' (DynamicSemantics.CCP.Partial.ofTrivalent ξ)

update⋆ is the image, so a candidate output common ground is the update of some candidate input.

theorem BeaverKrahmer2001.hearer_update_filters_then_asserts {W : Type u_1} (ξ : W → SignType) (cgs : Set (Set W)) : PFun.image (DynamicSemantics.CCP.Partial.ofTrivalent ξ) cgs = (fun (σ : Set W) => σ ∩ Trivalent.posExt ξ) '' {σ : Set W | σ ∈ cgs ∧ DynamicSemantics.PartialUpdate.Admits (DynamicSemantics.CCP.Partial.ofTrivalent ξ) σ}

The two-stage procedure filters out the candidate common grounds incompatible with the presuppositions, then updates each remaining one with the assertion.

theorem BeaverKrahmer2001.monologue {W : Type u_1} (ξ₁ ξ₂ : W → SignType) : PFun.image (DynamicSemantics.CCP.Partial.ofTrivalent ξ₂) (PFun.image (DynamicSemantics.CCP.Partial.ofTrivalent ξ₁) Set.univ) = PFun.image (DynamicSemantics.PartialUpdate.seq (DynamicSemantics.CCP.Partial.ofTrivalent ξ₁) (DynamicSemantics.CCP.Partial.ofTrivalent ξ₂)) Set.univ

A hearer making no assumptions updates from the full powerset; two sentences compose by sequencing the updates.

The paper's judgments

The rows with a schema feature are the paper's schematized examples; intuitive names the presupposition the paper reports, the per-logic …Predicts features the ones it prints, and the …Verdict features its correctness judgments. The rows with basic and preferred features are the floating-A cancellations.

def BeaverKrahmer2001.schemas (k : Kleene) : List (String × Formula Atom)

The schema a row's schema feature names, at each logic.

Equations

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

def BeaverKrahmer2001.presups : List (String × Formula Atom)

The presupposition a row's intuitive or …Predicts feature names.

Equations

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

def BeaverKrahmer2001.verdictTable : List (String × Bool)

A verdict feature read as agreement with the intuitive presupposition.

Equations

• BeaverKrahmer2001.verdictTable = [("correct", true), ("incorrect", false)]

def BeaverKrahmer2001.translationsTable : List (String × Formula Atom)

The basic and preferred translations a row's floating-A features name.

Equations

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

def BeaverKrahmer2001.Kleene.predictsKey : Kleene → String

The prediction feature of each logic.

Equations

• BeaverKrahmer2001.Kleene.strong.predictsKey = "strongPredicts"
• BeaverKrahmer2001.Kleene.middle.predictsKey = "middlePredicts"
• BeaverKrahmer2001.Kleene.weak.predictsKey = "weakPredicts"

def BeaverKrahmer2001.Kleene.verdictKey : Kleene → String

The verdict feature of each logic.

Equations

• BeaverKrahmer2001.Kleene.strong.verdictKey = "strongVerdict"
• BeaverKrahmer2001.Kleene.middle.verdictKey = "middleVerdict"
• BeaverKrahmer2001.Kleene.weak.verdictKey = "weakVerdict"

theorem BeaverKrahmer2001.printed_predictions (k : Kleene) (row : Datum) : row ∈ Examples.all → ∀ φ ∈ row.parse? "schema" (schemas k), ∀ π ∈ row.parse? k.predictsKey presups, φ.presup.Equiv π

The presupposition the paper prints for each logic is the maximal presupposition the semantics computes.

theorem BeaverKrahmer2001.printed_verdicts (k : Kleene) (row : Datum) : row ∈ Examples.all → ∀ φ ∈ row.parse? "schema" (schemas k), ∀ ι ∈ row.parse? "intuitive" presups, ∀ v ∈ row.parse? k.verdictKey verdictTable, v = true ↔ φ.presup.Equiv ι

The paper's verdicts compare the predicted with the intuitive presupposition.

theorem BeaverKrahmer2001.no_kleene_fits_soames_disjunctions (k : Kleene) : ∃ row ∈ Examples.all, ∃ φ ∈ row.parse? "schema" (schemas k), ∃ ι ∈ row.parse? "intuitive" presups, ¬φ.presup.Equiv ι

No single logic fits the Soames disjunction data, since each of the three mispredicts the intuitive presupposition of some printed example ([Soa79]; [vdS89]'s conclusion, which the paper accepts before restoring flexibility with the floating A).

theorem BeaverKrahmer2001.floating_a_rows (row : Datum) : row ∈ Examples.all → ∀ φ ∈ row.parse? "basic" translationsTable, ∀ γ ∈ row.parse? "preferred" translationsTable, Formula.Preferred φ.translations γ ∧ ∀ δ ∈ φ.translations, Formula.Preferred φ.translations δ → δ = γ

The floating-A winners the paper names are the preferred translations, uniquely.