Presupposition in trivalent semantics

A sentence with a presupposition denotes a trivalent proposition W → SignType, true or false where its presupposition holds and 0 where it fails. A trigger presupposing A and asserting B is the indicator {w | A w}.indicator fun w ↦ ofProp (B w), its presupposition is its support Function.support p, and it holds at w when p w = 1. Theories of projection differ in their connectives: the classical connectives are Weak Kleene (SignType.meetWeak), Karttunen's filtering connectives are Peters' Middle Kleene (SignType.meetMiddle, SignType.joinMiddle), Bochvar's truth operator is fun w ↦ ofProp (p w = 1), and the rival Strong Kleene and Belnap connectives are ⊓, ⊔, SignType.meetBelnap and SignType.joinBelnap. Each projection rule is a characterization of its connective (SignType.meetMiddle_eq_zero_iff for Karttunen's filtering conjunction), and quantified presuppositions project by the trivalent quantifiers of Logic/Trivalent/Pointwise.lean. Two-dimensional accounts, which read an assertion where its presupposition fails, use TwoDim (Semantics/ConventionalImplicature.lean).

Main definitions

• Presupposition.strawsonEntails: von Fintel's entailment, with the conclusion's presupposition as a premise.
• Presupposition.presupOfReferent: the definite-description combinator.

Main results

• Presupposition.strawsonEntails_iff_disjoint: Strawson entailment is the disjointness of the premise's truth and the conclusion's falsity.
• Presupposition.strawsonEntails_not_trans: Strawson entailment is not transitive.

References

• [Hei83]
• [Kar73]
• [Pet79]
• [Boc38]
• [vF99a]

Strawson entailment

def Presupposition.strawsonEntails {W : Type u_1} (p q : W → SignType) : Prop

Strawson entailment ([vF99a]) requires q to be true wherever p is true and q is defined, the conclusion's presupposition being a premise added to the entailment rather than something the entailment delivers.

Equations

• Presupposition.strawsonEntails p q = ∀ (w : W), p w = 1 → q w ≠ 0 → q w = 1

theorem Presupposition.strawsonEntails_iff_disjoint {W : Type u_1} {p q : W → SignType} : strawsonEntails p q ↔ Disjoint (Trivalent.posExt p) (Trivalent.negExt q)

Strawson entailment is the disjointness of the premise's truth and the conclusion's falsity.

theorem Presupposition.strawsonEntails_not_trans : ¬∀ (p q r : Unit → SignType), strawsonEntails p q → strawsonEntails q r → strawsonEntails p r

Strawson entailment is not transitive, since an undefined middle term discharges both premises vacuously, the well-known failure of [vF99a]'s notion; so it supports no Preorder.

Definite descriptions

noncomputable def Presupposition.presupOfReferent {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Prop) : W → SignType

The definite-description combinator, for a partial selector referent returning the referent at each world (or none where none is determined) and a scope asserted of it, is the scope's value at the referent where one is selected and undefined elsewhere. Every definite denotation instantiates the selector, with the Russellian iota Reference.iota over a restrictor, over the restrictor conjoined with identity to an antecedent, or with Donnellan's attributive use.

Equations

• Presupposition.presupOfReferent referent scope w = (referent w).elim 0 fun (e : E) => SignType.ofProp (scope e w)

@[simp]

theorem Presupposition.presupOfReferent_eq_zero_iff {W : Type u_1} {E : Type u_2} {referent : W → Option E} {scope : E → W → Prop} {w : W} : presupOfReferent referent scope w = 0 ↔ referent w = none

theorem Presupposition.presupOfReferent_of_some {W : Type u_1} {E : Type u_2} {referent : W → Option E} {scope : E → W → Prop} {w : W} {e : E} (h : referent w = some e) : presupOfReferent referent scope w = SignType.ofProp (scope e w)

theorem Presupposition.presupOfReferent_of_none {W : Type u_1} {E : Type u_2} {referent : W → Option E} {scope : E → W → Prop} {w : W} (h : referent w = none) : presupOfReferent referent scope w = 0