Beaver (2001): Presupposition and Assertion in Dynamic Semantics

The book reviews the linguistic theories of presupposition (Part I) and then builds a dynamic one (Part II). This file formalizes the propositional core of Part II, the partial update logic PUL of Chapter 6, and its trivalent counterpart of Chapter 10. A sentence denotes an update of information states, sets of worlds, and the presupposition operator ∂φ passes a state through only if updating it with φ changes nothing. A state satisfies a sentence it is a fixed point of and admits a sentence it can be updated with. A sentence presupposes what every state admitting it satisfies, and entails what every output of an update with it satisfies. From Part I, the file states Strawsonian presupposition and its Strong Kleene projection (Fact 2.1).

Main statements

• Formula.Presupposes.and_right, Formula.Presupposes.implies_right: a presupposition of the second conjunct or of the consequent projects conditionalised on the first.
• Formula.satisfies_might_iff, Formula.satisfies_must_iff: might is a consistency test and must a satisfaction test.
• Formula.eval_eq_ofTrivalent: on the non-modal sentences an update is the Heimian update of the sentence's value under Peters' connectives, so the dynamic and trivalent entailments coincide (Formula.entails_iff_tval, Fact 10.3).
• entailed_rows, unentailed_rows: the entailments and non-entailments the book prints for its translations of the realise examples.

Implementation notes

• The book's updates are relations between states. Every PUL relation is a partial function, so a sentence denotes a CCP.Partial.
• Facts 7.1, 8.1–8.3 and 8.5–8.8, with the tests of D61, are stated for ABLE, the first-order system of Chapters 7 and 8. Their proofs use only the propositional clauses, which ABLE shares with PUL, and they are proved here for PUL.
• Presupposition and its projection through negation, conjunction and implies are the substrate's PartialUpdate.Presupposes and its lemmas; the study adds might, must and ∂.
• Formula.tval gives the modal sentences the junk value 0; every theorem about it assumes the sentence non-modal.

TODO

• The remark after Fact 2.1, that for bivalent ψ the presuppositions listed are maximal.
• Fact 10.4: the trivalent correspondence extends to Bochvar's assertion operator (D79).
• The hide-and-seek examples E178–E183, which motivate the order sensitivity of might.

References

• [Bea01]
• [Kle52]
• [Pet79]
• [Vel96]

Strawsonian presupposition under Strong Kleene (Fact 2.1)

def Beaver2001.StrawsonPresupposes {W : Type u_2} (φ π : W → SignType) : Prop

φ presupposes π in Strawson's sense (D1) when π is true wherever φ is classical.

Equations

• Beaver2001.StrawsonPresupposes φ π = ∀ (w : W), φ w ≠ 0 → π w = 1

The rows of Fact 2.1, with the Strong Kleene connectives ⊓, ⊔ and -, and φ → ψ read as ¬φ ∨ ψ.

theorem Beaver2001.StrawsonPresupposes.neg {W : Type u_2} {φ π : W → SignType} (h : StrawsonPresupposes φ π) : StrawsonPresupposes (fun (w : W) => -φ w) π

theorem Beaver2001.StrawsonPresupposes.and_left {W : Type u_2} {φ ψ π : W → SignType} (h : StrawsonPresupposes φ π) : StrawsonPresupposes (fun (w : W) => min (φ w) (ψ w)) fun (w : W) => max (-ψ w) (π w)

theorem Beaver2001.StrawsonPresupposes.and_right {W : Type u_2} {φ ψ π : W → SignType} (h : StrawsonPresupposes φ π) : StrawsonPresupposes (fun (w : W) => min (ψ w) (φ w)) fun (w : W) => max (-ψ w) (π w)

theorem Beaver2001.StrawsonPresupposes.imp_left {W : Type u_2} {φ ψ π : W → SignType} (h : StrawsonPresupposes φ π) : StrawsonPresupposes (fun (w : W) => max (-φ w) (ψ w)) fun (w : W) => max (ψ w) (π w)

φ → ψ presupposes (¬ψ) → π, which is ψ ∨ π.

theorem Beaver2001.StrawsonPresupposes.imp_right {W : Type u_2} {φ ψ π : W → SignType} (h : StrawsonPresupposes φ π) : StrawsonPresupposes (fun (w : W) => max (-ψ w) (φ w)) fun (w : W) => max (-ψ w) (π w)

theorem Beaver2001.StrawsonPresupposes.or_left {W : Type u_2} {φ ψ π : W → SignType} (h : StrawsonPresupposes φ π) : StrawsonPresupposes (fun (w : W) => max (φ w) (ψ w)) fun (w : W) => max (ψ w) (π w)

φ ∨ ψ presupposes (¬ψ) → π, which is ψ ∨ π.

theorem Beaver2001.StrawsonPresupposes.or_right {W : Type u_2} {φ ψ π : W → SignType} (h : StrawsonPresupposes φ π) : StrawsonPresupposes (fun (w : W) => max (ψ w) (φ w)) fun (w : W) => max (ψ w) (π w)

Partial update logic (Ch. 6)

inductive Beaver2001.Formula (P : Type u_3) : Type u_3

The sentences of PUL over the atomic formulae P (D22, D34).

• atom {P : Type u_3} (p : P) : Formula P
• not {P : Type u_3} (φ : Formula P) : Formula P
• and {P : Type u_3} (φ ψ : Formula P) : Formula P
• might {P : Type u_3} (φ : Formula P) : Formula P
• must {P : Type u_3} (φ : Formula P) : Formula P
• presup {P : Type u_3} (φ : Formula P) : Formula P

def Beaver2001.instDecidableEqFormula.decEq {P✝ : Type u_3} [DecidableEq P✝] (x✝ x✝¹ : Formula P✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Beaver2001.instDecidableEqFormula.decEq (Beaver2001.Formula.atom a) (Beaver2001.Formula.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (Beaver2001.Formula.atom p) φ.not = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (Beaver2001.Formula.atom p) (φ.and ψ) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (Beaver2001.Formula.atom p) φ.might = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (Beaver2001.Formula.atom p) φ.must = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (Beaver2001.Formula.atom p) φ.presup = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.not (Beaver2001.Formula.atom p) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq a.not b.not = if h : a = b then h ▸ have inst := Beaver2001.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.not (φ_1.and ψ) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.not φ_1.might = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.not φ_1.must = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.not φ_1.presup = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (φ.and ψ) (Beaver2001.Formula.atom p) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (φ.and ψ) φ_1.not = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (φ.and ψ) φ_1.might = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (φ.and ψ) φ_1.must = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq (φ.and ψ) φ_1.presup = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.might (Beaver2001.Formula.atom p) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.might φ_1.not = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.might (φ_1.and ψ) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq a.might b.might = if h : a = b then h ▸ have inst := Beaver2001.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.might φ_1.must = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.might φ_1.presup = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.must (Beaver2001.Formula.atom p) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.must φ_1.not = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.must (φ_1.and ψ) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.must φ_1.might = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq a.must b.must = if h : a = b then h ▸ have inst := Beaver2001.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.must φ_1.presup = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.presup (Beaver2001.Formula.atom p) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.presup φ_1.not = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.presup (φ_1.and ψ) = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.presup φ_1.might = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq φ.presup φ_1.must = isFalse ⋯
• Beaver2001.instDecidableEqFormula.decEq a.presup b.presup = if h : a = b then h ▸ have inst := Beaver2001.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Beaver2001.instDecidableEqFormula {P✝ : Type u_3} [DecidableEq P✝] : DecidableEq (Formula P✝)

Equations

• Beaver2001.instDecidableEqFormula = Beaver2001.instDecidableEqFormula.decEq

def Beaver2001.Formula.implies {P : Type u_1} (φ ψ : Formula P) : Formula P

φ implies ψ is not (φ and not ψ) (D25).

Equations

• φ.implies ψ = (φ.and ψ.not).not

noncomputable def Beaver2001.Formula.eval {P : Type u_1} {W : Type u_2} (F : P → Set W) : Formula P → DynamicSemantics.CCP.Partial W

The update a sentence denotes in the model interpreting each atom p as F p (D25, D35), a partial function on information states that is defined for ∂φ only at the fixed points of φ.

Equations

• Beaver2001.Formula.eval F (Beaver2001.Formula.atom p) = fun (σ : Set W) => Part.some {w : W | w ∈ σ ∧ w ∈ F p}
• Beaver2001.Formula.eval F φ.not = (Beaver2001.Formula.eval F φ).neg
• Beaver2001.Formula.eval F (φ.and ψ) = DynamicSemantics.PartialUpdate.seq (Beaver2001.Formula.eval F φ) (Beaver2001.Formula.eval F ψ)
• Beaver2001.Formula.eval F φ.might = fun (σ : Set W) => Part.map (fun (υ : Set W) => if υ.Nonempty then σ else ∅) (Beaver2001.Formula.eval F φ σ)
• Beaver2001.Formula.eval F φ.must = fun (σ : Set W) => Part.map (fun (υ : Set W) => if υ = σ then σ else ∅) (Beaver2001.Formula.eval F φ σ)
• Beaver2001.Formula.eval F φ.presup = fun (σ : Set W) => { Dom := σ ∈ Beaver2001.Formula.eval F φ σ, get := fun (x : σ ∈ Beaver2001.Formula.eval F φ σ) => σ }

def Beaver2001.Formula.Satisfies {P : Type u_1} {W : Type u_2} (F : P → Set W) (σ : Set W) (φ : Formula P) : Prop

σ satisfies φ (D29) when σ[φ]σ.

Equations

• Beaver2001.Formula.Satisfies F σ φ = DynamicSemantics.PartialUpdate.supports σ (Beaver2001.Formula.eval F φ)

def Beaver2001.Formula.Presupposes {P : Type u_1} {W : Type u_2} (F : P → Set W) (φ ψ : Formula P) : Prop

φ presupposes ψ (D31) when every state admitting φ (D30) satisfies ψ.

Equations

• Beaver2001.Formula.Presupposes F φ ψ = DynamicSemantics.PartialUpdate.Presupposes (Beaver2001.Formula.eval F φ) (Beaver2001.Formula.eval F ψ)

def Beaver2001.Formula.Entails {P : Type u_1} {W : Type u_2} (F : P → Set W) (φ ψ : Formula P) : Prop

φ entails ψ (D26, with one premise) when every update with φ yields a state satisfying ψ (entails_iff_forall), which is dynamic entailment between the two updates.

Equations

• Beaver2001.Formula.Entails F φ ψ = DynamicSemantics.Entails [fun (x : Part (Set W)) => x >>= Beaver2001.Formula.eval F φ] fun (x : Part (Set W)) => x >>= Beaver2001.Formula.eval F ψ

def Beaver2001.Formula.ConsistentWith {P : Type u_1} {W : Type u_2} (F : P → Set W) (σ : Set W) (φ : Formula P) : Prop

σ is consistent with φ (Fact 8.5) when updating it does not reach the absurd state.

Equations

• Beaver2001.Formula.ConsistentWith F σ φ = ∃ τ ∈ Beaver2001.Formula.eval F φ σ, τ.Nonempty

def Beaver2001.Formula.IsTest {P : Type u_1} {W : Type u_2} (F : P → Set W) (φ : Formula P) : Prop

A test (D61) has only the input and the absurd state as outputs.

Equations

• Beaver2001.Formula.IsTest F φ = ∀ (σ τ : Set W), τ ∈ Beaver2001.Formula.eval F φ σ → τ = σ ∨ τ = ∅

theorem Beaver2001.Formula.mem_eval_atom {P : Type u_1} {W : Type u_2} {F : P → Set W} {σ τ : Set W} {p : P} : τ ∈ eval F (atom p) σ ↔ τ = {w : W | w ∈ σ ∧ w ∈ F p}

theorem Beaver2001.Formula.mem_eval_not {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ τ : Set W} : τ ∈ eval F φ.not σ ↔ ∃ υ ∈ eval F φ σ, σ \ υ = τ

theorem Beaver2001.Formula.mem_eval_and {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} {σ τ : Set W} : τ ∈ eval F (φ.and ψ) σ ↔ ∃ υ ∈ eval F φ σ, τ ∈ eval F ψ υ

theorem Beaver2001.Formula.mem_eval_might {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ τ : Set W} : τ ∈ eval F φ.might σ ↔ ∃ υ ∈ eval F φ σ, (if υ.Nonempty then σ else ∅) = τ

theorem Beaver2001.Formula.mem_eval_must {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ τ : Set W} : τ ∈ eval F φ.must σ ↔ ∃ υ ∈ eval F φ σ, (if υ = σ then σ else ∅) = τ

theorem Beaver2001.Formula.mem_eval_presup {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ τ : Set W} : τ ∈ eval F φ.presup σ ↔ σ ∈ eval F φ σ ∧ τ = σ

theorem Beaver2001.Formula.eval_eliminative {P : Type u_1} {W : Type u_2} {F : P → Set W} (φ : Formula P) {σ τ : Set W} : τ ∈ eval F φ σ → τ ⊆ σ

Every update is eliminative, never adding a world to its input (Fact 7.1).

theorem Beaver2001.Formula.empty_mem_eval_empty {P : Type u_1} {W : Type u_2} {F : P → Set W} (φ : Formula P) : ∅ ∈ eval F φ ∅

The absurd state admits every sentence and is its own update.

theorem Beaver2001.Formula.admits_of_mem {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ τ : Set W} (h : τ ∈ eval F φ σ) : DynamicSemantics.PartialUpdate.Admits (eval F φ) σ

theorem Beaver2001.Formula.presupposes_iff_forall {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} : Presupposes F φ ψ ↔ ∀ (σ : Set W), DynamicSemantics.PartialUpdate.Admits (eval F φ) σ → Satisfies F σ ψ

theorem Beaver2001.Formula.entails_iff_forall {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} : Entails F φ ψ ↔ ∀ (σ τ : Set W), τ ∈ eval F φ σ → Satisfies F τ ψ

theorem Beaver2001.Formula.eval_implies {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} : eval F (φ.implies ψ) = (eval F φ).cond (eval F ψ)

implies denotes Heim's conditional.

theorem Beaver2001.Formula.eval_must {P : Type u_1} {W : Type u_2} {F : P → Set W} (φ : Formula P) : eval F φ.must = eval F φ.not.might.not

must is the dual of might (Fact 6.1).

Projection (Facts 8.1–8.3, 8.8)

theorem Beaver2001.Formula.Presupposes.not {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (h : Presupposes F φ ψ) : Presupposes F φ.not ψ

theorem Beaver2001.Formula.Presupposes.and_left {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ χ : Formula P} (h : Presupposes F φ ψ) : Presupposes F (φ.and χ) ψ

theorem Beaver2001.Formula.Presupposes.implies_left {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ χ : Formula P} (h : Presupposes F φ ψ) : Presupposes F (φ.implies χ) ψ

theorem Beaver2001.Formula.Presupposes.might {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (h : Presupposes F φ ψ) : Presupposes F φ.might ψ

theorem Beaver2001.Formula.Presupposes.must {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (h : Presupposes F φ ψ) : Presupposes F φ.must ψ

theorem Beaver2001.Formula.Presupposes.trans {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ χ : Formula P} (h₁ : Presupposes F φ ψ) (h₂ : Presupposes F ψ χ) : Presupposes F φ χ

Presupposition composes (Fact 8.2).

theorem Beaver2001.Formula.presup_and_presupposes {P : Type u_1} {W : Type u_2} {F : P → Set W} (ψ χ : Formula P) : Presupposes F (ψ.presup.and χ) ψ

∂ψ and χ presupposes ψ.

theorem Beaver2001.Formula.Presupposes.and_right {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ χ : Formula P} (h : Presupposes F φ ψ) : Presupposes F (χ.and φ) (χ.implies ψ)

A presupposition of the second conjunct projects conditionalised on the first (Fact 8.3).

theorem Beaver2001.Formula.Presupposes.implies_right {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ χ : Formula P} (h : Presupposes F φ ψ) : Presupposes F (χ.implies φ) (χ.implies ψ)

A presupposition of the consequent projects conditionalised on the antecedent (Fact 8.3).

Epistemic modality (Facts 8.5–8.7)

theorem Beaver2001.Formula.might_isTest {P : Type u_1} {W : Type u_2} {F : P → Set W} (φ : Formula P) : IsTest F φ.might

theorem Beaver2001.Formula.must_isTest {P : Type u_1} {W : Type u_2} {F : P → Set W} (φ : Formula P) : IsTest F φ.must

theorem Beaver2001.Formula.IsTest.empty_mem_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ : Set W} (ht : IsTest F φ) (hσ : σ.Nonempty) (h : DynamicSemantics.PartialUpdate.Admits (eval F φ) σ) : ∅ ∈ eval F φ σ ↔ ¬Satisfies F σ φ

A test admitted by a non-absurd state crashes it exactly when the state does not satisfy the test.

theorem Beaver2001.Formula.satisfies_might_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ : Set W} (hσ : σ.Nonempty) : Satisfies F σ φ.might ↔ ConsistentWith F σ φ

might is a consistency test (Fact 8.5), passing a non-absurd state iff the state is consistent with φ.

theorem Beaver2001.Formula.empty_mem_eval_might_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ : Set W} (hσ : σ.Nonempty) (h : DynamicSemantics.PartialUpdate.Admits (eval F φ) σ) : ∅ ∈ eval F φ.might σ ↔ ¬ConsistentWith F σ φ

Otherwise might crashes the state (Fact 8.5).

theorem Beaver2001.Formula.satisfies_iff_not_consistentWith_not {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ : Set W} (h : DynamicSemantics.PartialUpdate.Admits (eval F φ) σ) : Satisfies F σ φ ↔ ¬ConsistentWith F σ φ.not

A state admitting φ satisfies it iff it is inconsistent with not φ (Lemma 8.6).

theorem Beaver2001.Formula.satisfies_must_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ : Set W} (hσ : σ.Nonempty) : Satisfies F σ φ.must ↔ Satisfies F σ φ

must is a satisfaction test (Fact 8.7), passing a non-absurd state iff the state satisfies φ.

theorem Beaver2001.Formula.empty_mem_eval_must_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ : Set W} (hσ : σ.Nonempty) (h : DynamicSemantics.PartialUpdate.Admits (eval F φ) σ) : ∅ ∈ eval F φ.must σ ↔ ¬Satisfies F σ φ

Otherwise must crashes the state (Fact 8.7).

The trivalent counterpart (Ch. 10)

inductive Beaver2001.Formula.NonModal {P : Type u_1} : Formula P → Prop

The non-modal sentences, the language PL+∂.

• atom {P : Type u_1} (p : P) : (Formula.atom p).NonModal
• not {P : Type u_1} {φ : Formula P} : φ.NonModal → φ.not.NonModal
• and {P : Type u_1} {φ ψ : Formula P} : φ.NonModal → ψ.NonModal → (φ.and ψ).NonModal
• presup {P : Type u_1} {φ : Formula P} : φ.NonModal → φ.presup.NonModal

theorem Beaver2001.Formula.NonModal.implies {P : Type u_1} {φ ψ : Formula P} (hφ : φ.NonModal) (hψ : ψ.NonModal) : (φ.implies ψ).NonModal

noncomputable def Beaver2001.Formula.tval {P : Type u_1} {W : Type u_2} (F : P → Set W) : Formula P → W → SignType

The value of a sentence of PL+∂ at a world under Peters' trivalent semantics (D70, D71), with bivalent atoms, the Peters connectives, and ∂φ true where φ is true and undefined elsewhere.

Equations

• Beaver2001.Formula.tval F (Beaver2001.Formula.atom p) x✝ = SignType.ofProp (x✝ ∈ F p)
• Beaver2001.Formula.tval F φ.not x✝ = -Beaver2001.Formula.tval F φ x✝
• Beaver2001.Formula.tval F (φ.and ψ) x✝ = (Beaver2001.Formula.tval F φ x✝).meetMiddle (Beaver2001.Formula.tval F ψ x✝)
• Beaver2001.Formula.tval F φ.presup x✝ = max (Beaver2001.Formula.tval F φ x✝) 0
• Beaver2001.Formula.tval F φ.might x✝ = 0
• Beaver2001.Formula.tval F φ.must x✝ = 0

def Beaver2001.Formula.TrueAt {P : Type u_1} {W : Type u_2} (F : P → Set W) (w : W) (φ : Formula P) : Prop

φ is true at w in the update semantics (D76) when {w}[φ]{w}.

Equations

• Beaver2001.Formula.TrueAt F w φ = ({w} ∈ Beaver2001.Formula.eval F φ {w})

def Beaver2001.Formula.FalseAt {P : Type u_1} {W : Type u_2} (F : P → Set W) (w : W) (φ : Formula P) : Prop

φ is false at w in the update semantics (D77) when {w}[φ]∅.

Equations

• Beaver2001.Formula.FalseAt F w φ = (∅ ∈ Beaver2001.Formula.eval F φ {w})

theorem Beaver2001.Formula.eval_eq_ofTrivalent {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} (hφ : φ.NonModal) : eval F φ = DynamicSemantics.CCP.Partial.ofTrivalent (tval F φ)

On PL+∂ an update is the Heimian update of the sentence's trivalent value, defined iff the sentence is classical at every world of the state and keeping the worlds where it is true. This combines Lemma 10.1 with the distributivity of non-modal updates used to prove Lemma 10.2.

theorem Beaver2001.Formula.admits_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ : Set W} (hφ : φ.NonModal) : DynamicSemantics.PartialUpdate.Admits (eval F φ) σ ↔ ∀ w ∈ σ, tval F φ w ≠ 0

theorem Beaver2001.Formula.trueAt_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {w : W} (hφ : φ.NonModal) : TrueAt F w φ ↔ tval F φ w = 1

Update truth is trivalent truth (Lemma 10.1).

theorem Beaver2001.Formula.falseAt_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {w : W} (hφ : φ.NonModal) : FalseAt F w φ ↔ tval F φ w = -1

Update falsity is trivalent falsity (Lemma 10.1).

theorem Beaver2001.Formula.satisfies_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ : Formula P} {σ : Set W} (hφ : φ.NonModal) : Satisfies F σ φ ↔ ∀ w ∈ σ, TrueAt F w φ

A state satisfies a non-modal sentence iff the sentence is true at each of its worlds, the distributivity used to prove Lemma 10.2.

theorem Beaver2001.Formula.entails_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (hφ : φ.NonModal) (hψ : ψ.NonModal) : Entails F φ ψ ↔ ∀ (w : W), TrueAt F w φ → TrueAt F w ψ

For non-modal sentences, entailment is entailment at every world (Lemma 10.2).

theorem Beaver2001.Formula.entails_iff_satisfies {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (hφ : φ.NonModal) (hψ : ψ.NonModal) : Entails F φ ψ ↔ ∀ (σ : Set W), Satisfies F σ φ → Satisfies F σ ψ

For non-modal sentences, entailment is preservation of fixed points (D73).

theorem Beaver2001.Formula.entails_iff_tval {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (hφ : φ.NonModal) (hψ : ψ.NonModal) : Entails F φ ψ ↔ ∀ (w : W), tval F φ w = 1 → tval F ψ w = 1

The update and trivalent entailments coincide on PL+∂ (Fact 10.3).

theorem Beaver2001.Formula.Presupposes.entails {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (h : Presupposes F φ ψ) (hψ : ψ.NonModal) : Entails F φ ψ

A sentence entails what it presupposes, when that is non-modal.

theorem Beaver2001.Formula.presupposes_iff_strawsonPresupposes {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (hφ : φ.NonModal) (hψ : ψ.NonModal) : Presupposes F φ ψ ↔ StrawsonPresupposes (tval F φ) (tval F ψ)

On PL+∂ the dynamic presupposition of D31 is the Strawsonian presupposition of D1 under Peters' semantics, which is Peters' result.

theorem Beaver2001.Formula.presupposes_iff {P : Type u_1} {W : Type u_2} {F : P → Set W} {φ ψ : Formula P} (hφ : φ.NonModal) (hψ : ψ.NonModal) : Presupposes F φ ψ ↔ Entails F φ ψ ∧ Entails F φ.not ψ

A non-modal sentence presupposes exactly what both it and its negation entail.

The book's examples

inductive Beaver2001.Atom : Type

The atomic formulae of the examples, with the book's names where it prints a translation.

• hiding : Atom

  Bertha is hiding, the book's bih.

• believesHiding : Atom

  Anna has come to believe that Bertha is hiding, cb_a_bih.

• findsHer : Atom

  Anna will find Bertha, awfb.

• regrets : Atom

  Bertha has negative vibes arising from her belief that Anna realises she is hiding, NVB_B_(∂_bih&cb_a_bih).

• inKitchen : Atom

  Bertha is in the kitchen, which E175 writes bc.

• inAttic : Atom

  Bertha is in the attic, ba.

• believesInAttic : Atom

  Anna has come to believe that Bertha is in the attic, cb_a_ba.

• lands : Atom

  Spaceman Spiff lands on Planet X.

• heavier : Atom

  Spiff's weight is greater than it would be on Earth.

• bothered : Atom

  Spiff is bothered by it.

• leaves : Atom

  Spiff won't stay long.

@[instance_reducible]

instance Beaver2001.instDecidableEqAtom : DecidableEq Atom

Equations

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

def Beaver2001.termModel (P : Type u_3) : P → Set (Set P)

The term model over the atomic formulae P (D23), whose worlds are sets of atoms, an atom holding at the worlds containing it.

Equations

• Beaver2001.termModel P p = {w : Set P | p ∈ w}

theorem Beaver2001.e154 {W : Type u_2} (F : Atom → Set W) : Formula.Presupposes F ((Formula.atom Atom.lands).implies ((Formula.atom Atom.heavier).presup.and (Formula.atom Atom.bothered))) ((Formula.atom Atom.lands).implies (Formula.atom Atom.heavier))

E154, if Spaceman Spiff lands on Planet X, he will be bothered by the fact that his weight is greater than it would be on Earth, presupposes that if he lands there his weight is greater.

theorem Beaver2001.e154_not_unconditional : ¬Formula.Presupposes (termModel Atom) ((Formula.atom Atom.lands).implies ((Formula.atom Atom.heavier).presup.and (Formula.atom Atom.bothered))) (Formula.atom Atom.heavier)

E154 does not presuppose that Spiff's weight is greater, since a world where he does not land makes the sentence true.

theorem Beaver2001.e156 {W : Type u_2} (F : Atom → Set W) : Formula.Presupposes F (((Formula.atom Atom.lands).and ((Formula.atom Atom.heavier).presup.and (Formula.atom Atom.bothered))).implies (Formula.atom Atom.leaves)) ((Formula.atom Atom.lands).implies (Formula.atom Atom.heavier))

E156, if Spaceman Spiff lands on Planet X and is bothered by the fact that his weight is greater than it would be on Earth, he won't stay long, carries the same conditional presupposition.

def Beaver2001.translations : List (String × Formula Atom)

The translations of §6.5, keyed by their printed form.

Equations

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

theorem Beaver2001.entailed_rows {W : Type u_2} (F : Atom → Set W) (row : Datum) : row ∈ Examples.all → ∀ φ ∈ row.parse? "translation" translations, ∀ ψ ∈ row.parse? "entails" translations, Formula.Entails F φ ψ

The entailments the book prints for its translations (E168c, E169c, E172c, E173c, E174c, E175d) hold in every model, each translation presupposing what it entails.

theorem Beaver2001.unentailed_rows (row : Datum) : row ∈ Examples.all → ∀ φ ∈ row.parse? "translation" translations, ∀ ψ ∈ row.parse? "doesNotEntail" translations, ¬Formula.Entails (termModel Atom) φ ψ

The non-entailments it prints (E175c, E176c, E177c) fail in the term model.

theorem Beaver2001.e177_admits {W : Type u_2} (F : Atom → Set W) (σ : Set W) (φ : Formula Atom) : φ ∈ Examples.e177.parse? "translation" translations → DynamicSemantics.PartialUpdate.Admits (Formula.eval F φ) σ

Every information state admits the translation of E177, so the sentence carries no presupposition.