Égré, Rossi and Sprenger (2026): Conditionals, Presupposition, and Logic: Avoid Void

Égré, Rossi and Sprenger answer the objection that a trivalent theory of conditionals cannot share its third value with a trivalent theory of presupposition, since an indicative does not presuppose its antecedent. The answer is a principle of felicitous assertion, Avoid Void: a sentence that is void at every world of the context cannot be asserted. On their conditional–modal semantics, with an update that collapses when the sentence is nowhere true, a conditional then presupposes that its antecedent is possible but not that it is true, and presuppositions project through negation, might and the antecedent of a conditional. Karttunen's filtering conditions for conjunction, the conditional and disjunction come out of sequential context update over the symmetric Cooper connectives, not of the truth tables. Written into consequence, Avoid Void blocks inferring if A, C from not A.

Main statements

• accepts_cond_iff: the Ramsey test (Proposition 3.3).
• presupposes_cond_dia, not_presupposes_cond_antecedent, not_presupposes_cond_neg: a conditional presupposes that its antecedent is possible and neither it nor its negation (Facts 4.3 and 4.4); Presupposes.neg, Presupposes.dia, Presupposes.cond_left give the projection of Proposition 5.1 and Fact 4.6.
• presupposes_forallInstances_dia: restricted quantifiers presuppose that their restrictor is possibly nonempty; at a single world this is Belnap's existential presupposition (forallInstances_singleton).
• update_cond_eq_empty_iff, update_cond_ofSet, update_disj_ofSet, update_conj_ofSet: Proposition 5.2.
• update_localUpdate_nonempty_iff: sequential update of an elementary conjunction, conditional or disjunction is felicitous exactly when the context admits it under Peters's filtering connectives and its content is possible in Karttunen's local context, so the pragmatic account recovers the filtering predictions (§5.3–5.5) while the Cooper conjunction itself does not filter (not_presupposes_conj_carrier).
• entails_neg_cond, not_entailsFlat_neg_cond, not_entailsSharp_neg_cond: False Antecedents is valid in C and blocked in C♭ and C#; entailsSharp_or_to_if, entailsSharp_reductio and the failures of footnote 15 (§6).
• strawsonEntails_iff_st: Strawson entailment is strict-tolerant validity.

Implementation notes

• Sentences, Kleene negation, Cooper conjunction and disjunction, and the modals are those of EgreRossiSprenger2026b. The update is Definition 3.2, which collapses when the sentence is nowhere true, not the one of EgreRossiSprenger2026b, which collapses when the update is self-defeating; footnote 6 contrasts the two (update_neg_conj_dia, update_contra_footnote6). The paper's values 1, # and 0 are 1, 0 and -1 in SignType.
• Worlds outside the context are left open (footnote 3); the conditional is void there.
• Definition 4.2 describes presupposition carriers whose value is a presupposition-free content in contexts accepting the presupposition and void elsewhere; carrier is that template, and ofTrigger the carrier of a trigger of Presupposition.Formula, which at a single world is the trigger's local value (ofTrigger_singleton).
• §2 adopts Cooper's tables for the conditional language and represents the conditional truth-functionally at worlds of the context. Under Definition 3.2 this holds for a classical antecedent (cond_ofSet_apply) but not for one that is void throughout the context, where (p → q) → r is void where Cooper's table gives r, and Left-Nesting, valid for Cooper valuations, fails (cond_cond_of_inter_eq_empty). The same collapse yields Fact 4.3, which fails under the update of EgreRossiSprenger2026b (not_presupposes_cond_dia_of_restrict).
• Fact 4.5 as printed, that ∀x(Ax → Bx) presupposes ∃xAx, fails for Definition 4.1 (not_presupposes_forallInstances_exists): its proof treats not accepting ∃xAx as accepting its negation. The derivable presupposition is ◇∃xAx, the counterpart of Fact 4.3.
• Fact 4.4 holds of contingent sentences, as Definition 4.1 presumes; it is proved for a context-free consequent from the witnesses its proof names.
• Definition 6.1 asks for a premise-compatible pair at which the conclusion is not void and glosses this as one at which it is true. The two agree for context-free sentences (entailsSharp_iff_of_contextFree) but not in general (entailsSharp_never_true); EntailsSharp is the printed definition. §6 prints the blocked False Antecedents inference as A ⊭ A → C; the premise is ¬A.

TODO

• The implicature account of (12)–(17) and the embedding of the compatibility presupposition under scalar alternatives.
• Projection from complex, not only elementary, arguments of the connectives.

References

• [ERS26a]
• [ERS26c]
• [ERS26b]
• [Coo68]
• [Bel70]
• [Kar73]
• [Kar74a]
• [Pet79]
• [Sta75]
• [vF99a]
• [CERvR12]
• [Gib81]

Update and the conditional

noncomputable def EgreRossiSprenger2026c.update {W : Type u_1} (s : Set W) (φ : EgreRossiSprenger2026b.Sentence W) : Set W

The update s[A] of Definition 3.2 keeps the worlds of s where A is not false, provided A is true somewhere in s, and otherwise collapses to ∅.

Equations

• EgreRossiSprenger2026c.update s φ = if ∃ w ∈ s, φ s w = 1 then EgreRossiSprenger2026b.Sentence.restrict s φ else ∅

noncomputable def EgreRossiSprenger2026c.cond {W : Type u_1} (φ ψ : EgreRossiSprenger2026b.Sentence W) : EgreRossiSprenger2026b.Sentence W

The conditional asserts its consequent at the context updated with its antecedent, and is void where the world drops out of the update (§2).

Equations

• EgreRossiSprenger2026c.cond φ ψ s w = if w ∈ EgreRossiSprenger2026c.update s φ then ψ (EgreRossiSprenger2026c.update s φ) w else 0

theorem EgreRossiSprenger2026c.update_of_exists {W : Type u_1} {s : Set W} {φ : EgreRossiSprenger2026b.Sentence W} (h : ∃ w ∈ s, φ s w = 1) : update s φ = EgreRossiSprenger2026b.Sentence.restrict s φ

theorem EgreRossiSprenger2026c.update_of_not_exists {W : Type u_1} {s : Set W} {φ : EgreRossiSprenger2026b.Sentence W} (h : ¬∃ w ∈ s, φ s w = 1) : update s φ = ∅

theorem EgreRossiSprenger2026c.mem_update {W : Type u_1} {s : Set W} {φ : EgreRossiSprenger2026b.Sentence W} {w : W} : w ∈ update s φ ↔ (w ∈ s ∧ 0 ≤ φ s w) ∧ ∃ w' ∈ s, φ s w' = 1

theorem EgreRossiSprenger2026c.update_subset {W : Type u_1} (s : Set W) (φ : EgreRossiSprenger2026b.Sentence W) : update s φ ⊆ s

@[simp]

theorem EgreRossiSprenger2026c.update_empty {W : Type u_1} (φ : EgreRossiSprenger2026b.Sentence W) : update ∅ φ = ∅

theorem EgreRossiSprenger2026c.update_nonempty_iff {W : Type u_1} {s : Set W} {φ : EgreRossiSprenger2026b.Sentence W} : (update s φ).Nonempty ↔ ∃ w ∈ s, φ s w = 1

An update survives exactly when the sentence is true somewhere in the context.

theorem EgreRossiSprenger2026c.update_congr {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} (h : φ s = ψ s) : update s φ = update s ψ

The update reads the sentence only at the context itself.

theorem EgreRossiSprenger2026c.update_zero {W : Type u_1} (s : Set W) : update s 0 = ∅

@[simp]

theorem EgreRossiSprenger2026c.update_ofSet {W : Type u_1} (s p : Set W) : update s (EgreRossiSprenger2026b.Sentence.ofSet p) = s ∩ p

On a classical sentence the update is intersection, collapsed or not.

theorem EgreRossiSprenger2026c.cond_apply_of_mem {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} {w : W} (h : w ∈ update s φ) : cond φ ψ s w = ψ (update s φ) w

theorem EgreRossiSprenger2026c.cond_apply_of_notMem {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} {w : W} (h : w ∉ update s φ) : cond φ ψ s w = 0

theorem EgreRossiSprenger2026c.cond_apply_of_not_exists {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} (h : ¬∃ w ∈ s, φ s w = 1) (w : W) : cond φ ψ s w = 0

A conditional whose antecedent is nowhere true in the context is void throughout it.

theorem EgreRossiSprenger2026c.neg_cond {W : Type u_1} (φ ψ : EgreRossiSprenger2026b.Sentence W) : -cond φ ψ = cond φ (-ψ)

Negation commutes with the conditional (Negation Commutation, §2).

theorem EgreRossiSprenger2026c.cond_ofSet_apply {W : Type u_1} {s : Set W} {ψ : EgreRossiSprenger2026b.Sentence W} {w : W} {p : Set W} (hψ : ψ.ContextFree) (hw : w ∈ s) : cond (EgreRossiSprenger2026b.Sentence.ofSet p) ψ s w = SignType.condAssert Trivalent.Designation.lp (EgreRossiSprenger2026b.Sentence.ofSet p s w) (ψ s w)

With a classical antecedent and a context-free consequent, the conditional is Cooper's at every world of the context, as §2 represents it.

theorem EgreRossiSprenger2026c.cond_cond_of_inter_eq_empty {W : Type u_1} {s : Set W} {χ : EgreRossiSprenger2026b.Sentence W} {w : W} {p q : Set W} (h : s ∩ p = ∅) (hw : w ∈ s) : cond (cond (EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q)) χ s w = 0 ∧ SignType.condAssert Trivalent.Designation.lp (cond (EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q) s w) (χ s w) = χ s w ∧ cond ((-EgreRossiSprenger2026b.Sentence.ofSet p).disj (EgreRossiSprenger2026b.Sentence.ofSet q)) χ s w = χ s w

Where p is false throughout the context, (p → q) → r is void throughout it, while [Coo68]'s table and (p ⊃ q) → r both give it the value of r, so the conditional is not Cooper's on the conditional language, and Left-Nesting, valid for Cooper valuations ([ERS26b]), fails.

Acceptance and Avoid Void

def EgreRossiSprenger2026c.AvoidsVoid {W : Type u_1} (s : Set W) (φ : EgreRossiSprenger2026b.Sentence W) : Prop

A sentence avoids void in a context when it is not void at every world of it; by Avoid Void a sentence can be felicitously asserted only in a context where it avoids void.

Equations

• EgreRossiSprenger2026c.AvoidsVoid s φ = ∃ w ∈ s, φ s w ≠ 0

def EgreRossiSprenger2026c.Accepts {W : Type u_1} (s : Set W) (φ : EgreRossiSprenger2026b.Sentence W) : Prop

A context accepts a sentence when the sentence is false at none of its worlds and avoids void in it (Definition 3.1).

Equations

• EgreRossiSprenger2026c.Accepts s φ = (EgreRossiSprenger2026b.Sentence.Accepts s φ ∧ EgreRossiSprenger2026c.AvoidsVoid s φ)

theorem EgreRossiSprenger2026c.accepts_iff {W : Type u_1} {s : Set W} {φ : EgreRossiSprenger2026b.Sentence W} : Accepts s φ ↔ (∀ w ∈ s, 0 ≤ φ s w) ∧ ∃ w ∈ s, φ s w = 1

theorem EgreRossiSprenger2026c.not_accepts_empty {W : Type u_1} (φ : EgreRossiSprenger2026b.Sentence W) : ¬Accepts ∅ φ

The empty context accepts nothing.

theorem EgreRossiSprenger2026c.accepts_ofSet_iff' {W : Type u_1} {s p : Set W} : Accepts s (EgreRossiSprenger2026b.Sentence.ofSet p) ↔ s.Nonempty ∧ s ⊆ p

theorem EgreRossiSprenger2026c.avoidsVoid_box_iff {W : Type u_1} {s : Set W} {φ : EgreRossiSprenger2026b.Sentence W} : AvoidsVoid s φ.box ↔ AvoidsVoid s φ

theorem EgreRossiSprenger2026c.accepts_box_iff {W : Type u_1} {s : Set W} {φ : EgreRossiSprenger2026b.Sentence W} : Accepts s φ.box ↔ Accepts s φ

Accepting A is accepting □A (§3, after Definition 3.1).

theorem EgreRossiSprenger2026c.accepts_dia_iff {W : Type u_1} {s : Set W} {φ : EgreRossiSprenger2026b.Sentence W} : Accepts s φ.dia ↔ ∃ w ∈ s, φ s w = 1

A context accepts ◇A exactly when A is true somewhere in it.

theorem EgreRossiSprenger2026c.accepts_cond_iff {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} : Accepts s (cond φ ψ) ↔ Accepts (update s φ) ψ

A context accepts A → B iff its update with A accepts B (Proposition 3.3, the Ramsey test).

Presupposition

def EgreRossiSprenger2026c.Presupposes {W : Type u_1} (φ ψ : EgreRossiSprenger2026b.Sentence W) : Prop

A presupposes B when every context not accepting B makes A void at all its worlds, which by Avoid Void makes A unassertable there (Definition 4.1).

Equations

• EgreRossiSprenger2026c.Presupposes φ ψ = ∀ (s : Set W), ¬EgreRossiSprenger2026c.Accepts s ψ → ∀ w ∈ s, φ s w = 0

noncomputable def EgreRossiSprenger2026c.carrier {W : Type u_1} (ψ χ : EgreRossiSprenger2026b.Sentence W) : EgreRossiSprenger2026b.Sentence W

An elementary presupposition carrier with presupposition B and content C takes the value of C in a context accepting B, and is void throughout any other (Definition 4.2).

Equations

• EgreRossiSprenger2026c.carrier ψ χ s w = if EgreRossiSprenger2026c.Accepts s ψ then χ s w else 0

theorem EgreRossiSprenger2026c.Presupposes.not_avoidsVoid {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} (h : Presupposes φ ψ) (hs : ¬Accepts s ψ) : ¬AvoidsVoid s φ

theorem EgreRossiSprenger2026c.presupposes_carrier {W : Type u_1} (ψ χ : EgreRossiSprenger2026b.Sentence W) : Presupposes (carrier ψ χ) ψ

theorem EgreRossiSprenger2026c.neg_carrier {W : Type u_1} (ψ χ : EgreRossiSprenger2026b.Sentence W) : -carrier ψ χ = carrier ψ (-χ)

theorem EgreRossiSprenger2026c.update_carrier {W : Type u_1} (s : Set W) (ψ χ : EgreRossiSprenger2026b.Sentence W) : update s (carrier ψ χ) = if Accepts s ψ then update s χ else ∅

Updating with a carrier is updating with its content in a context that accepts its presupposition, and collapses in any other.

theorem EgreRossiSprenger2026c.Presupposes.neg {W : Type u_1} {φ ψ : EgreRossiSprenger2026b.Sentence W} (h : Presupposes φ ψ) : Presupposes (-φ) ψ

A presupposition projects through negation (Proposition 5.1).

theorem EgreRossiSprenger2026c.Presupposes.dia {W : Type u_1} {φ ψ : EgreRossiSprenger2026b.Sentence W} (h : Presupposes φ ψ) : Presupposes φ.dia ψ

A presupposition projects through might (Proposition 5.1).

theorem EgreRossiSprenger2026c.Presupposes.cond_left {W : Type u_1} {φ ψ : EgreRossiSprenger2026b.Sentence W} (h : Presupposes φ ψ) (χ : EgreRossiSprenger2026b.Sentence W) : Presupposes (cond φ χ) ψ

A presupposition of the antecedent projects from a conditional (Proposition 5.1).

theorem EgreRossiSprenger2026c.not_avoidsVoid_of_presupposes {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} (h : Presupposes φ ψ) (hs : ¬Accepts s ψ) (χ : EgreRossiSprenger2026b.Sentence W) : ¬AvoidsVoid s (-φ) ∧ ¬AvoidsVoid s φ.dia ∧ ¬AvoidsVoid s (cond φ χ)

Where a presupposition of A fails, asserting ¬A, ◇A or A → C violates Avoid Void (Proposition 5.1).

theorem EgreRossiSprenger2026c.presupposes_cond_dia {W : Type u_1} (φ ψ : EgreRossiSprenger2026b.Sentence W) : Presupposes (cond φ ψ) φ.dia

A conditional presupposes that its antecedent is possible (Fact 4.3).

theorem EgreRossiSprenger2026c.presupposes_cond_dia_projects {W : Type u_1} (φ ψ χ : EgreRossiSprenger2026b.Sentence W) : Presupposes (-cond φ ψ) φ.dia ∧ Presupposes (cond φ ψ).dia φ.dia ∧ Presupposes (cond (cond φ ψ) χ) φ.dia

The compatibility presupposition projects through negation, might and the antecedent of a conditional (Fact 4.6).

theorem EgreRossiSprenger2026c.not_presupposes_cond_antecedent {W : Type u_1} {φ ψ : EgreRossiSprenger2026b.Sentence W} (hψ : ψ.ContextFree) {w₁ w₂ : W} (h₁ : φ {w₁, w₂} w₁ = 1) (h₁' : ψ {w₁, w₂} w₁ = 1) (h₂ : φ {w₁, w₂} w₂ = -1) : ¬Presupposes (cond φ ψ) φ

With a context-free consequent, a conditional does not presuppose its antecedent, as a context where antecedent and consequent are true at one world and the antecedent is false at the other shows (Fact 4.4, first claim).

theorem EgreRossiSprenger2026c.not_presupposes_cond_neg {W : Type u_1} {φ ψ : EgreRossiSprenger2026b.Sentence W} (hψ : ψ.ContextFree) {w₁ : W} (h₁ : φ {w₁} w₁ = 1) (h₁' : ψ {w₁} w₁ = 1) : ¬Presupposes (cond φ ψ) (-φ) ∧ ¬Presupposes (cond φ ψ) (-φ).dia

Nor does it presuppose the negation of its antecedent or the possibility of that negation (Fact 4.4, second and third claims).

theorem EgreRossiSprenger2026c.avoidsVoid_cond_ofSet_iff {W : Type u_1} {s p q : Set W} : AvoidsVoid s (cond (EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q)) ↔ (s ∩ p).Nonempty

With a classical antecedent and consequent, a conditional avoids void exactly when its antecedent is compatible with the context, [Sta75]'s condition on asserting an indicative.

theorem EgreRossiSprenger2026c.not_presupposes_conj_carrier : ¬Presupposes ((EgreRossiSprenger2026b.Sentence.ofSet Set.univ).conj (carrier (EgreRossiSprenger2026b.Sentence.ofSet ∅) (EgreRossiSprenger2026b.Sentence.ofSet Set.univ))) (EgreRossiSprenger2026b.Sentence.ofSet ∅)

The Cooper conjunction does not filter, since A ∧ B can be true where the presupposition of B fails (§5.1, example (25)).

Quantified sentences (Fact 4.5)

The quantifiers over a domain shared by the worlds of the context are Cooper's conjunction and disjunction generalized to the instances, forallHaug and existsHaug.

noncomputable def EgreRossiSprenger2026c.forallInstances {W : Type u_1} {D : Type u_2} (φ : D → EgreRossiSprenger2026b.Sentence W) : EgreRossiSprenger2026b.Sentence W

Universal quantification, the generalized Cooper conjunction of the instances.

Equations

• EgreRossiSprenger2026c.forallInstances φ s w = Trivalent.forallHaug fun (d : D) => φ d s w

noncomputable def EgreRossiSprenger2026c.existsInstances {W : Type u_1} {D : Type u_2} (φ : D → EgreRossiSprenger2026b.Sentence W) : EgreRossiSprenger2026b.Sentence W

Existential quantification, the generalized Cooper disjunction of the instances.

Equations

• EgreRossiSprenger2026c.existsInstances φ s w = Trivalent.existsHaug fun (d : D) => φ d s w

theorem EgreRossiSprenger2026c.presupposes_forallInstances_dia {W : Type u_1} {D : Type u_2} (A : D → Set W) (ψ : D → EgreRossiSprenger2026b.Sentence W) : Presupposes (forallInstances fun (d : D) => cond (EgreRossiSprenger2026b.Sentence.ofSet (A d)) (ψ d)) (EgreRossiSprenger2026b.Sentence.ofSet (⋃ (d : D), A d)).dia ∧ Presupposes (existsInstances fun (d : D) => cond (EgreRossiSprenger2026b.Sentence.ofSet (A d)) (ψ d)) (EgreRossiSprenger2026b.Sentence.ofSet (⋃ (d : D), A d)).dia

Restricted universal and existential sentences presuppose that their restrictor is possibly nonempty, the counterpart of Fact 4.3 for quantifier restriction.

theorem EgreRossiSprenger2026c.not_presupposes_forallInstances_exists : ¬Presupposes (forallInstances fun (x : Unit) => cond (EgreRossiSprenger2026b.Sentence.ofSet {true}) (EgreRossiSprenger2026b.Sentence.ofSet Set.univ)) (EgreRossiSprenger2026b.Sentence.ofSet (⋃ (x : Unit), {true})) ∧ ¬Presupposes (existsInstances fun (x : Unit) => cond (EgreRossiSprenger2026b.Sentence.ofSet {true}) (EgreRossiSprenger2026b.Sentence.ofSet Set.univ)) (EgreRossiSprenger2026b.Sentence.ofSet (⋃ (x : Unit), {true}))

A context can fail to accept ∃xAx at one world while an A that is a B makes ∀x(Ax → Bx) and ∃x(Ax → Bx) true at another, so Fact 4.5 fails as printed.

theorem EgreRossiSprenger2026c.forallInstances_singleton {W : Type u_1} {D : Type} (A B : D → Set W) (w : W) : forallInstances (fun (d : D) => cond (EgreRossiSprenger2026b.Sentence.ofSet (A d)) (EgreRossiSprenger2026b.Sentence.ofSet (B d))) {w} w = Belnap1970.restrictedForall (fun (d : D) => w ∈ A d) fun (d : D) => w ∈ B d

At a single world the restricted universal is [Bel70]'s restricted quantification, whose existential presupposition is bound to the world.

Updates on complex sentences (Proposition 5.2)

theorem EgreRossiSprenger2026c.update_cond_nonempty_iff {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} : (update s (cond φ ψ)).Nonempty ↔ (update (update s φ) ψ).Nonempty

An update on A → B survives exactly when the update on A and then on B does.

theorem EgreRossiSprenger2026c.update_cond_eq_empty_iff {W : Type u_1} {s : Set W} {φ ψ : EgreRossiSprenger2026b.Sentence W} : update s (cond φ ψ) = ∅ ↔ update s φ = ∅ ∨ update (update s φ) ψ = ∅

An update on A → B collapses exactly when the update on A or its update on B does (Proposition 5.2, first case).

theorem EgreRossiSprenger2026c.update_cond_ofSet {W : Type u_1} {s : Set W} {ψ : EgreRossiSprenger2026b.Sentence W} {p : Set W} (hψ : EgreRossiSprenger2026b.NeverVoid ψ) (h : (update s (cond (EgreRossiSprenger2026b.Sentence.ofSet p) ψ)).Nonempty) : update s (cond (EgreRossiSprenger2026b.Sentence.ofSet p) ψ) = s \ update (update s (EgreRossiSprenger2026b.Sentence.ofSet p)) (-ψ)

For a classical antecedent and a never void consequent, a surviving update on A → B removes from the context the worlds that the update on A and then on ¬B keeps (Proposition 5.2).

theorem EgreRossiSprenger2026c.update_disj_ofSet {W : Type u_1} {s p q : Set W} (h : (s ∩ (pᶜ ∩ q)).Nonempty) : update s ((EgreRossiSprenger2026b.Sentence.ofSet p).disj (EgreRossiSprenger2026b.Sentence.ofSet q)) = update s (cond (-EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q))

For classical disjuncts, with ¬A ∧ B possible, the update on A ∨ B is the update on ¬A → B (Proposition 5.2, (3)).

theorem EgreRossiSprenger2026c.update_conj_ofSet {W : Type u_1} {s : Set W} (p q : Set W) : update s ((EgreRossiSprenger2026b.Sentence.ofSet p).conj (EgreRossiSprenger2026b.Sentence.ofSet q)) = update s (EgreRossiSprenger2026b.Sentence.ofSet p) ∩ update s (EgreRossiSprenger2026b.Sentence.ofSet q) ∧ update s ((EgreRossiSprenger2026b.Sentence.ofSet p).conj (EgreRossiSprenger2026b.Sentence.ofSet q)) = update (update s (EgreRossiSprenger2026b.Sentence.ofSet p)) (EgreRossiSprenger2026b.Sentence.ofSet q)

For classical conjuncts the update on A ∧ B is the intersection of the updates and the update on A and then B (Proposition 5.2, (4)).

Projection by sequential update (§5.3–5.5)

An interpreter updates on the first argument of a connective and evaluates the second in the result, in s[A] for a conjunction or a conditional and in s[¬A] for a disjunction; the assertion is felicitous when neither step collapses. For elementary carriers this is exactly admittance under [Pet79]'s filtering connectives together with the possibility of the content in [Kar74a]'s local context, though the connectives are Cooper's symmetric ones.

noncomputable def EgreRossiSprenger2026c.ofTrigger {W : Type u_1} {Atom : Type u_2} (I : Atom → Set W) (p p' : Atom) : EgreRossiSprenger2026b.Sentence W

The elementary carrier of a trigger of the propositional fragment, presupposing I p and asserting I p'.

Equations

• EgreRossiSprenger2026c.ofTrigger I p p' = EgreRossiSprenger2026c.carrier (EgreRossiSprenger2026b.Sentence.ofSet (I p)) (EgreRossiSprenger2026b.Sentence.ofSet (I p'))

theorem EgreRossiSprenger2026c.ofTrigger_singleton {W : Type u_1} {Atom : Type u_2} (I : Atom → Set W) (p p' : Atom) (w : W) : ofTrigger I p p' {w} w = Presupposition.Formula.middleKleene I (Presupposition.Formula.trigger p p') w

At a single world the carrier is the trigger's local value, defined where the presupposition holds, so the global and the local treatments of presupposition part only in larger contexts.

noncomputable def EgreRossiSprenger2026c.localUpdate {W : Type u_1} (s : Set W) (φ : EgreRossiSprenger2026b.Sentence W) : Presupposition.Connective → Set W

The context in which sequential update evaluates the second argument of a connective.

Equations

• EgreRossiSprenger2026c.localUpdate s φ Presupposition.Connective.conj = EgreRossiSprenger2026c.update s φ
• EgreRossiSprenger2026c.localUpdate s φ Presupposition.Connective.cond = EgreRossiSprenger2026c.update s φ
• EgreRossiSprenger2026c.localUpdate s φ Presupposition.Connective.disj = EgreRossiSprenger2026c.update s (-φ)

theorem EgreRossiSprenger2026c.update_localUpdate_nonempty_iff {W : Type u_1} {Atom : Type u_2} {I : Atom → Set W} {s : Set W} (c : Presupposition.Connective) (a a' b b' : Atom) : (update (localUpdate s (ofTrigger I a a') c) (ofTrigger I b b')).Nonempty ↔ s ⊆ Function.support (Presupposition.Formula.middleKleene I (Presupposition.Formula.bin c (Presupposition.Formula.trigger a a') (Presupposition.Formula.trigger b b'))) ∧ (Presupposition.Connective.localContext s (Presupposition.Formula.truth I (Presupposition.Formula.trigger a a')) c ∩ Presupposition.Formula.truth I (Presupposition.Formula.trigger b b')).Nonempty

Sequential update of an elementary conjunction, conditional or disjunction is felicitous exactly when the context admits it under [Pet79]'s filtering connectives and the content of its second argument is possible in [Kar74a]'s local context (§5.3–5.5).

Epistemic contradictions (§5.3, footnote 6)

theorem EgreRossiSprenger2026c.update_update_neg_dia {W : Type u_1} (s p : Set W) : update (update s (-EgreRossiSprenger2026b.Sentence.ofSet p)) (EgreRossiSprenger2026b.Sentence.ofSet p).dia = ∅

Sequential update on ¬p ∧ ◇p collapses (§5.3).

theorem EgreRossiSprenger2026c.not_accepts_neg_conj_dia {W : Type u_1} (s p : Set W) : ¬Accepts s ((-EgreRossiSprenger2026b.Sentence.ofSet p).conj (EgreRossiSprenger2026b.Sentence.ofSet p).dia)

No context accepts ¬p ∧ ◇p (footnote 6).

theorem EgreRossiSprenger2026c.update_neg_conj_dia {W : Type u_1} {s p : Set W} (h : (s ∩ p).Nonempty) (h' : (s \ p).Nonempty) : update s ((-EgreRossiSprenger2026b.Sentence.ofSet p).conj (EgreRossiSprenger2026b.Sentence.ofSet p).dia) = s \ p

The update of Definition 3.2 on ¬p ∧ ◇p keeps the ¬p-worlds where p is open (footnote 6).

theorem EgreRossiSprenger2026c.update_contra_footnote6 : update Set.univ ((-EgreRossiSprenger2026b.Sentence.ofSet {true}).conj (EgreRossiSprenger2026b.Sentence.ofSet {true}).dia) = {false} ∧ (-EgreRossiSprenger2026b.Sentence.ofSet {true}).conj (EgreRossiSprenger2026b.Sentence.ofSet {true}).dia {false} false = -1 ∧ EgreRossiSprenger2026b.Sentence.update Set.univ ((-EgreRossiSprenger2026b.Sentence.ofSet {true}).conj (EgreRossiSprenger2026b.Sentence.ofSet {true}).dia) = ∅

Where p holds at one world and fails at the other, Definition 3.2 updates ¬p ∧ ◇p to the second world, at which the sentence is then false, while the update of [ERS26c] collapses (footnote 6).

The earlier update

Fact 4.3 rests on the collapse of Definition 3.2 at a sentence that is nowhere true. The update of [ERS26c] keeps the non-false worlds unless the update is self-defeating, and on it a conditional whose antecedent is void throughout the context takes its consequent's value.

theorem EgreRossiSprenger2026c.not_presupposes_cond_dia_of_restrict : ¬Presupposes (EgreRossiSprenger2026b.Sentence.cond 0 (EgreRossiSprenger2026b.Sentence.ofSet Set.univ)) (EgreRossiSprenger2026b.Sentence.dia 0)

Under the update of [ERS26c], A → B does not presuppose ◇A, since with A void everywhere no context accepts ◇A, yet A → ⊤ is true.

theorem EgreRossiSprenger2026c.cond_zero_left {W : Type u_1} (ψ : EgreRossiSprenger2026b.Sentence W) (s : Set W) (w : W) : cond 0 ψ s w = 0

Under Definition 3.2 the same conditional is void throughout every context.

Inference (§6)

C-validity is the consequence of [ERS26c], preservation of non-falsity at every context. Avoid Void enters consequence in two ways: C♭ preserves acceptance in the sense of Definition 3.1, and C# adds to C-validity that some premise-compatible context–world pair does not void the conclusion.

def EgreRossiSprenger2026c.EntailsFlat {W : Type u_1} (Γ : Set (EgreRossiSprenger2026b.Sentence W)) (ψ : EgreRossiSprenger2026b.Sentence W) : Prop

An inference is C♭-valid when every context accepting the premises accepts the conclusion.

Equations

• EgreRossiSprenger2026c.EntailsFlat Γ ψ = ∀ (s : Set W), (∀ φ ∈ Γ, EgreRossiSprenger2026c.Accepts s φ) → EgreRossiSprenger2026c.Accepts s ψ

def EgreRossiSprenger2026c.EntailsSharp {W : Type u_1} (Γ : Set (EgreRossiSprenger2026b.Sentence W)) (ψ : EgreRossiSprenger2026b.Sentence W) : Prop

An inference is C#-valid when it is C-valid and not every context–world pair at which the premises are not false voids the conclusion (Definition 6.1).

Equations

• EgreRossiSprenger2026c.EntailsSharp Γ ψ = (EgreRossiSprenger2026b.Entails Γ ψ ∧ ¬∀ (s : Set W), ∀ w ∈ s, (∀ φ ∈ Γ, 0 ≤ φ s w) → ψ s w = 0)

theorem EgreRossiSprenger2026c.entailsSharp_iff {W : Type u_1} {Γ : Set (EgreRossiSprenger2026b.Sentence W)} {ψ : EgreRossiSprenger2026b.Sentence W} : EntailsSharp Γ ψ ↔ EgreRossiSprenger2026b.Entails Γ ψ ∧ ∃ (s : Set W), ∃ w ∈ s, (∀ φ ∈ Γ, 0 ≤ φ s w) ∧ ψ s w ≠ 0

theorem EgreRossiSprenger2026c.entailsSharp_iff_of_contextFree {W : Type u_1} {Γ : Set (EgreRossiSprenger2026b.Sentence W)} {ψ : EgreRossiSprenger2026b.Sentence W} (hΓ : ∀ φ ∈ Γ, φ.ContextFree) (hψ : ψ.ContextFree) : EntailsSharp Γ ψ ↔ EgreRossiSprenger2026b.Entails Γ ψ ∧ ∃ (s : Set W), ∃ w ∈ s, (∀ φ ∈ Γ, 0 ≤ φ s w) ∧ ψ s w = 1

For context-free premises and conclusion, Definition 6.1's second clause is its gloss, that given C-validity some premise-compatible pair makes the conclusion true.

theorem EgreRossiSprenger2026c.entailsSharp_never_true : EntailsSharp {EgreRossiSprenger2026b.Sentence.ofSet {true}} (cond (-EgreRossiSprenger2026b.Sentence.ofSet {true}).dia (EgreRossiSprenger2026b.Sentence.ofSet ∅)) ∧ ∀ (s : Set Bool), ∀ w ∈ s, cond (-EgreRossiSprenger2026b.Sentence.ofSet {true}).dia (EgreRossiSprenger2026b.Sentence.ofSet ∅) s w ≠ 1

The gloss fails beyond context-free sentences, since p C#-entails ◇¬p → ⊥, which is true at no context–world pair.

theorem EgreRossiSprenger2026c.entails_neg_cond {W : Type u_1} (φ ψ : EgreRossiSprenger2026b.Sentence W) : EgreRossiSprenger2026b.Entails {-φ} (cond φ ψ)

False Antecedents, ¬A ⊨ A → C, is C-valid.

theorem EgreRossiSprenger2026c.not_entailsFlat_neg_cond {W : Type u_1} {p : Set W} {w : W} (hw : w ∉ p) (ψ : EgreRossiSprenger2026b.Sentence W) : ¬EntailsFlat {-EgreRossiSprenger2026b.Sentence.ofSet p} (cond (EgreRossiSprenger2026b.Sentence.ofSet p) ψ)

False Antecedents is not C♭-valid for a contingent classical antecedent.

theorem EgreRossiSprenger2026c.not_entailsSharp_neg_cond {W : Type u_1} (p : Set W) (ψ : EgreRossiSprenger2026b.Sentence W) : ¬EntailsSharp {-EgreRossiSprenger2026b.Sentence.ofSet p} (cond (EgreRossiSprenger2026b.Sentence.ofSet p) ψ)

False Antecedents is not C#-valid for a classical antecedent, since wherever ¬A is not false A → C is void.

theorem EgreRossiSprenger2026c.entailsFlat_neg_cond {W : Type u_1} (φ ψ : EgreRossiSprenger2026b.Sentence W) : EntailsFlat {-cond φ ψ} (cond φ (-ψ)) ∧ EntailsFlat {cond φ (-ψ)} (-cond φ ψ)

Negation Commutation stays C♭-valid.

theorem EgreRossiSprenger2026c.not_entailsFlat_or_to_if {W : Type u_1} {p q : Set W} {w : W} (hp : w ∈ p) : ¬EntailsFlat {(EgreRossiSprenger2026b.Sentence.ofSet p).disj (EgreRossiSprenger2026b.Sentence.ofSet q)} (cond (-EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q))

Or-to-If is not C♭-valid, since a context can accept p ∨ q by making p true and q false throughout, which voids ¬p → q.

theorem EgreRossiSprenger2026c.entailsSharp_or_to_if {W : Type u_1} {p q : Set W} {w : W} (hp : w ∉ p) (hq : w ∈ q) : EntailsSharp {(EgreRossiSprenger2026b.Sentence.ofSet p).disj (EgreRossiSprenger2026b.Sentence.ofSet q)} (cond (-EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q))

Or-to-If is C#-valid when ¬p ∧ q is possible.

theorem EgreRossiSprenger2026c.not_accepts_cond_cond_neg {W : Type u_1} (s p q : Set W) : ¬(Accepts s (cond (EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q)) ∧ Accepts s (cond (EgreRossiSprenger2026b.Sentence.ofSet p) (-EgreRossiSprenger2026b.Sentence.ofSet q)))

[Gib81]'s notes p → q and p → ¬q are accepted together by no context, so in C♭ they entail anything (§6, (33)–(34)).

theorem EgreRossiSprenger2026c.entailsSharp_reductio {W : Type u_1} {p q : Set W} {w : W} (hw : w ∉ p) : EntailsSharp {cond (EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q), cond (EgreRossiSprenger2026b.Sentence.ofSet p) (-EgreRossiSprenger2026b.Sentence.ofSet q)} (-EgreRossiSprenger2026b.Sentence.ofSet p)

Reductio from conflicting conditionals, p → q, p → ¬q ⊨ ¬p, is C#-valid when p can fail.

theorem EgreRossiSprenger2026c.entailsSharp_ofSet_self {W : Type u_1} {p : Set W} {w : W} (hw : w ∈ p) : EntailsSharp {EgreRossiSprenger2026b.Sentence.ofSet p} (EgreRossiSprenger2026b.Sentence.ofSet p) ∧ ¬EntailsSharp {EgreRossiSprenger2026b.Sentence.ofSet p, -EgreRossiSprenger2026b.Sentence.ofSet p} (EgreRossiSprenger2026b.Sentence.ofSet p)

C# is not monotone, since p entails p but p, ¬p does not (footnote 15).

theorem EgreRossiSprenger2026c.not_entailsSharp_contradiction {W : Type u_1} (p : Set W) : ¬EntailsSharp {(EgreRossiSprenger2026b.Sentence.ofSet p).conj (-EgreRossiSprenger2026b.Sentence.ofSet p)} ((EgreRossiSprenger2026b.Sentence.ofSet p).conj (-EgreRossiSprenger2026b.Sentence.ofSet p))

C# is not reflexive, since p ∧ ¬p does not entail itself (footnote 15).

theorem EgreRossiSprenger2026c.not_entailsSharp_trans {W : Type u_1} {p q : Set W} {w w' : W} (hw : w ∈ p) (hw' : w' ∉ p) (hq : w' ∈ q) : EntailsSharp {EgreRossiSprenger2026b.Sentence.ofSet p} ((EgreRossiSprenger2026b.Sentence.ofSet p).disj (EgreRossiSprenger2026b.Sentence.ofSet q)) ∧ EntailsSharp {(EgreRossiSprenger2026b.Sentence.ofSet p).disj (EgreRossiSprenger2026b.Sentence.ofSet q)} (cond (-EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q)) ∧ ¬EntailsSharp {EgreRossiSprenger2026b.Sentence.ofSet p} (cond (-EgreRossiSprenger2026b.Sentence.ofSet p) (EgreRossiSprenger2026b.Sentence.ofSet q))

C# is not transitive, since p ⊨ p ∨ q and p ∨ q ⊨ ¬p → q but not p ⊨ ¬p → q (footnote 15).

theorem EgreRossiSprenger2026c.strawsonEntails_iff_st {W : Type u_1} (p q : W → SignType) : Presupposition.strawsonEntails p q ↔ ∀ (w : W), Trivalent.Designation.k3.threshold ≤ p w → Trivalent.Designation.lp.threshold ≤ q w

[vF99a]'s Strawson entailment between trivalent propositions is the strict-tolerant validity of [CERvR12], under which the conclusion is tolerantly true wherever the premise is strictly true (§6).