Égré, Rossi and Sprenger (2026): Trivalent Conditionals, Kratzer Style

Égré, Rossi and Sprenger extend the trivalent semantics of indicative conditionals to epistemic might and must. A sentence takes a trivalent value at a context and a world; the modals quantify over the context with the trivalent quantifiers that skip void instances; and the conditional stays a binary connective while hard-wiring Kratzer's restriction into its truth conditions: it asserts its consequent at the context updated with its antecedent, and is void where the world drops out or the update collapses. Acceptance is non-falsity throughout the context, equivalently probability 1 under every credence mirroring it, and the Restrictor View's predictions (the covert must, the test behaviour of modals, epistemic and if-might contradictions) come out at the level of acceptance and inference, not truth conditions.

Main statements

• Sentence.cond_ofCooper, ofFormula_cond: on nonmodal sentences the conditional is Cooper's, so the semantics extends the Cooper valuations of [ERS26b].
• Sentence.ContextFree.update_eq_restrict (Fact 1); Sentence.update_box_of_accepts, Sentence.update_dia_of and their converses (Fact 2), which on a conditional-free prejacent is [Vel96]'s test (update_dia_ofSet).
• Sentence.cond_box_eq_neg_one (Fact 3), Sentence.neg_cond (Proposition 2), Sentence.ContextFree.update_update (Proposition 3), Sentence.ContextFree.cond_cond (Corollary 1), and import_export_fails for a modal antecedent, (18) against (19).
• not_accepts_contra', update_contra' (Fact 5): through Agrees, the semantics is [Yal07]'s domain semantics on conditional-free sentences, and Fact 5 is Yalcin2007.not_accepted_contra'.
• Mirrors.prob_eq_one_iff, accepts_iff_forall_mirrors (Definition 7); prob_box_eq_zero_or_one (Fact 4); accepts_cond_box_iff, prob_cond_box_le, prob_cond_box_eq_prob_box_cond (Theorem 1); cEntails_iff_entails (Theorem 2).
• schema_K (Fact 6), entails_box (Fact 7), entails_cond_box (Corollary 2), accepts_cond_dia_iff (Fact 8), entails_dia_conj, entails_cond_dia (Fact 9), eq_empty_of_accepts_neg_dia, eq_empty_of_if_might, not_entails_of_dia (Proposition 5), modus_ponens (Fact 10), modus_tollens and its failures (Fact 11), the structural rules and failures of Proposition 4, and entails_insert_iff (Theorem 3) with the Conditional Proof counterexample.
• cond_ofSet, prob_cond_ofSet (Adams's Thesis, through [ERS26b]'s conditional events), prob_cond_contra (footnote 11), prob_contra'_coin (footnote 12), die_bare_vs_must ((20) and (21)).

Implementation notes

• A sentence denotes its valuation, a function Set W → W → SignType, so the semantics is compositional by construction (Proposition 1), and a schema proved for all such functions holds of the formulas of every model. Definition 3's degenerate clause ⟦A⟧^{s,w} := ⟦A⟧^{{w},w} for w ∉ s is stated for every A; the modal and conditional clauses evaluate at Sentence.ctx to build it in. Nonmodal sentences are then context-independent at every world, as the proof of Fact 1 asserts (Sentence.ContextFree), and conditional-free ones are Sentence.ofSet.
• The value 1/2 is 0 in SignType, so ⟦A⟧ ≥ 1/2 is 0 ≤ ⟦A⟧.
• Definition 6 requires only that the credence give the context probability 1, but footnote 8 and the proofs of Theorems 1 and 2 use a credence positive exactly on the context. Mirrors is that regular reading; under the literal one the probability half of Theorem 1 fails (not_prob_cond_box_eq_of_literal).
• Footnote 18 prints its premise as q ∧ ¬◇p, which its own model does not accept (not_accepts_fn18_printed); the main text's ◇¬p is meant.
• Consequence is stated for a fixed world space, quantifying over its contexts, which is what the proofs of Theorems 2 and 3 use; countermodels are concrete world spaces.

TODO

• The pragmatic acceptance condition for disjunctions in §4.3, under which disjunctions of epistemic contradictions are unacceptable.
• The motivating clause (4), which makes (15) false, and the §4.4 discussion of how speakers negate conditionals.

References

• [ERS26c]
• [ERS26b]
• [Coo68]
• [Kra86]
• [Yal07]
• [Yal12]
• [Vel96]

@[reducible, inline]

abbrev EgreRossiSprenger2026b.Sentence (W : Type u_2) : Type u_2

A sentence of the conditional–modal language denotes a trivalent value at each context–world pair.

Equations

• EgreRossiSprenger2026b.Sentence W = (Set W → W → SignType)

noncomputable def EgreRossiSprenger2026b.Sentence.ctx {W : Type u_1} (s : Set W) (w : W) : Set W

The context a sentence is evaluated in, s itself when the world belongs to it and the singleton {w} otherwise, which is Definition 3's degenerate stipulation read globally.

Equations

• EgreRossiSprenger2026b.Sentence.ctx s w = if w ∈ s then s else {w}

theorem EgreRossiSprenger2026b.Sentence.ctx_of_mem {W : Type u_1} {s : Set W} {w : W} (h : w ∈ s) : ctx s w = s

theorem EgreRossiSprenger2026b.Sentence.ctx_of_notMem {W : Type u_1} {s : Set W} {w : W} (h : w ∉ s) : ctx s w = {w}

@[simp]

theorem EgreRossiSprenger2026b.Sentence.ctx_singleton {W : Type u_1} (w : W) : ctx {w} w = {w}

theorem EgreRossiSprenger2026b.Sentence.mem_ctx {W : Type u_1} (s : Set W) (w : W) : w ∈ ctx s w

def EgreRossiSprenger2026b.Sentence.Normalized {W : Type u_1} (φ : Sentence W) : Prop

A sentence respects the degenerate stipulation when, outside the context, it is evaluated at its own singleton. The operators below produce only normalized sentences.

Equations

• φ.Normalized = ∀ (s : Set W), ∀ w ∉ s, φ s w = φ {w} w

def EgreRossiSprenger2026b.Sentence.ContextFree {W : Type u_1} (φ : Sentence W) : Prop

A nonmodal sentence places no condition on the context.

Equations

• φ.ContextFree = ∀ (s s' : Set W) (w : W), φ s w = φ s' w

theorem EgreRossiSprenger2026b.Sentence.ContextFree.normalized {W : Type u_1} {φ : Sentence W} (h : φ.ContextFree) : φ.Normalized

noncomputable def EgreRossiSprenger2026b.Sentence.ofSet {W : Type u_1} (p : Set W) : Sentence W

The L-sentence expressing the classical proposition p.

Equations

• EgreRossiSprenger2026b.Sentence.ofSet p x✝ w = SignType.ofProp (w ∈ p)

@[simp]

theorem EgreRossiSprenger2026b.Sentence.ofSet_apply {W : Type u_1} (p s : Set W) (w : W) : ofSet p s w = SignType.ofProp (w ∈ p)

theorem EgreRossiSprenger2026b.Sentence.contextFree_ofSet {W : Type u_1} (p : Set W) : (ofSet p).ContextFree

@[simp]

theorem EgreRossiSprenger2026b.Sentence.neg_apply {W : Type u_1} (φ : Sentence W) (s : Set W) (w : W) : (-φ) s w = -φ s w

Cooper negation is Kleene's, pointwise.

theorem EgreRossiSprenger2026b.Sentence.neg_ofSet {W : Type u_1} (p : Set W) : -ofSet p = ofSet pᶜ

def EgreRossiSprenger2026b.Sentence.conj {W : Type u_1} (φ ψ : Sentence W) : Sentence W

Cooper conjunction, pointwise.

Equations

• φ.conj ψ s w = (φ s w).meetBelnap (ψ s w)

def EgreRossiSprenger2026b.Sentence.disj {W : Type u_1} (φ ψ : Sentence W) : Sentence W

Cooper disjunction, pointwise.

Equations

• φ.disj ψ s w = (φ s w).joinBelnap (ψ s w)

@[simp]

theorem EgreRossiSprenger2026b.Sentence.conj_apply {W : Type u_1} (φ ψ : Sentence W) (s : Set W) (w : W) : φ.conj ψ s w = (φ s w).meetBelnap (ψ s w)

@[simp]

theorem EgreRossiSprenger2026b.Sentence.disj_apply {W : Type u_1} (φ ψ : Sentence W) (s : Set W) (w : W) : φ.disj ψ s w = (φ s w).joinBelnap (ψ s w)

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

theorem EgreRossiSprenger2026b.Sentence.ContextFree.conj {W : Type u_1} {φ ψ : Sentence W} (hφ : φ.ContextFree) (hψ : ψ.ContextFree) : (φ.conj ψ).ContextFree

theorem EgreRossiSprenger2026b.Sentence.ContextFree.disj {W : Type u_1} {φ ψ : Sentence W} (hφ : φ.ContextFree) (hψ : ψ.ContextFree) : (φ.disj ψ).ContextFree

Restriction and update (Definition 2)

def EgreRossiSprenger2026b.Sentence.restrict {W : Type u_1} (s : Set W) (φ : Sentence W) : Set W

The restriction s/A keeps the worlds of s where A is not false.

Equations

• EgreRossiSprenger2026b.Sentence.restrict s φ = {w : W | w ∈ s ∧ 0 ≤ φ s w}

@[simp]

theorem EgreRossiSprenger2026b.Sentence.mem_restrict {W : Type u_1} {s : Set W} {φ : Sentence W} {w : W} : w ∈ restrict s φ ↔ w ∈ s ∧ 0 ≤ φ s w

theorem EgreRossiSprenger2026b.Sentence.restrict_subset {W : Type u_1} (s : Set W) (φ : Sentence W) : restrict s φ ⊆ s

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

The update s[A] is the restriction if the restriction still accepts A, and the collapsed context ∅ if the update would be self-defeating.

Equations

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

theorem EgreRossiSprenger2026b.Sentence.update_eq_restrict {W : Type u_1} {s : Set W} {φ : Sentence W} (h : ∀ w ∈ restrict s φ, 0 ≤ φ (restrict s φ) w) : update s φ = restrict s φ

theorem EgreRossiSprenger2026b.Sentence.update_eq_empty {W : Type u_1} {s : Set W} {φ : Sentence W} (h : ¬∀ w ∈ restrict s φ, 0 ≤ φ (restrict s φ) w) : update s φ = ∅

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

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

theorem EgreRossiSprenger2026b.Sentence.mem_update_iff {W : Type u_1} {s : Set W} {φ : Sentence W} {w : W} : w ∈ update s φ ↔ w ∈ restrict s φ ∧ ∀ w' ∈ restrict s φ, 0 ≤ φ (restrict s φ) w'

A world survives the update exactly when it survives the restriction and the restriction accepts the sentence.

theorem EgreRossiSprenger2026b.Sentence.ContextFree.update_eq_restrict {W : Type u_1} {φ : Sentence W} (h : φ.ContextFree) (s : Set W) : update s φ = restrict s φ

Restriction and update agree on nonmodal sentences, whose evaluation does not move with the context (Fact 1).

@[simp]

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

The modals (Definition 3)

□ and ◇ generalize Cooper conjunction and disjunction over the worlds of the context: false when some instance is false, void when every instance is void, true otherwise — Haug's trivalent quantifiers over the context, in the form [Bel70] gave restricted quantification.

noncomputable def EgreRossiSprenger2026b.Sentence.box {W : Type u_1} (φ : Sentence W) : Sentence W

Epistemic must is Haug's universal quantifier over the context.

Equations

• φ.box s w = Trivalent.forallHaug ((EgreRossiSprenger2026b.Sentence.ctx s w).indicator fun (w' : W) => φ (EgreRossiSprenger2026b.Sentence.ctx s w) w')

noncomputable def EgreRossiSprenger2026b.Sentence.dia {W : Type u_1} (φ : Sentence W) : Sentence W

Epistemic might is Haug's existential quantifier over the context.

Equations

• φ.dia s w = Trivalent.existsHaug ((EgreRossiSprenger2026b.Sentence.ctx s w).indicator fun (w' : W) => φ (EgreRossiSprenger2026b.Sentence.ctx s w) w')

theorem EgreRossiSprenger2026b.Sentence.box_normalized {W : Type u_1} (φ : Sentence W) : φ.box.Normalized

theorem EgreRossiSprenger2026b.Sentence.dia_normalized {W : Type u_1} (φ : Sentence W) : φ.dia.Normalized

theorem EgreRossiSprenger2026b.Sentence.box_apply_of_mem {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} (h : w ∈ s) : φ.box s w = Trivalent.forallHaug (s.indicator fun (w' : W) => φ s w')

theorem EgreRossiSprenger2026b.Sentence.dia_apply_of_mem {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} (h : w ∈ s) : φ.dia s w = Trivalent.existsHaug (s.indicator fun (w' : W) => φ s w')

theorem EgreRossiSprenger2026b.Sentence.box_eq_neg_one_iff {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} (h : w ∈ s) : φ.box s w = -1 ↔ ∃ w' ∈ s, φ s w' = -1

□A is false at a context exactly when A is false somewhere in it.

theorem EgreRossiSprenger2026b.Sentence.box_eq_zero_iff {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} (h : w ∈ s) : φ.box s w = 0 ↔ ∀ w' ∈ s, φ s w' = 0

□A is void at a context exactly when A is void throughout it.

theorem EgreRossiSprenger2026b.Sentence.dia_eq_one_iff {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} (h : w ∈ s) : φ.dia s w = 1 ↔ ∃ w' ∈ s, φ s w' = 1

◇A is true at a context exactly when A is true somewhere in it.

theorem EgreRossiSprenger2026b.Sentence.dia_eq_zero_iff {W : Type u_1} {φ : Sentence W} {s : Set W} {w : W} (h : w ∈ s) : φ.dia s w = 0 ↔ ∀ w' ∈ s, φ s w' = 0

◇A is void at a context exactly when A is void throughout it.

theorem EgreRossiSprenger2026b.Sentence.box_apply_congr {W : Type u_1} {φ : Sentence W} {s : Set W} {w w' : W} (h : w ∈ s) (h' : w' ∈ s) : φ.box s w = φ.box s w'

The modals are uniform across their context.

theorem EgreRossiSprenger2026b.Sentence.dia_apply_congr {W : Type u_1} {φ : Sentence W} {s : Set W} {w w' : W} (h : w ∈ s) (h' : w' ∈ s) : φ.dia s w = φ.dia s w'

theorem EgreRossiSprenger2026b.Sentence.dia_eq_neg_box_neg {W : Type u_1} (φ : Sentence W) : φ.dia = -(-φ).box

◇ is the dual of □, as the definition ◇A := ¬□¬A demands.

theorem EgreRossiSprenger2026b.Sentence.box_eq_neg_dia_neg {W : Type u_1} (φ : Sentence W) : φ.box = -(-φ).dia

□ is the dual of ◇.

The conditional (Definition 3)

A → B asserts B at the context updated with A, and is void where the world of evaluation drops out of the update or the update collapses.

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

The trivalent, Kratzer-style conditional.

Equations

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

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

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

theorem EgreRossiSprenger2026b.Sentence.cond_normalized {W : Type u_1} (φ ψ : Sentence W) : (φ.cond ψ).Normalized

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

Negation commutes with the conditional at every context–world pair (Proposition 2).

theorem EgreRossiSprenger2026b.Sentence.cond_box_eq_neg_one {W : Type u_1} {φ ψ : Sentence W} {s : Set W} {w : W} (h : φ.cond ψ s w = -1) : φ.cond ψ.box s w = -1

Where A → B is false, so is A → □B (Fact 3), so the bare conditional has the less demanding non-falsity condition.

Acceptance and the test behaviour of modals

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

A context accepts a sentence when the sentence is not false at any of its worlds, evaluated at the context itself (Definition 7).

Equations

• EgreRossiSprenger2026b.Sentence.Accepts s φ = ∀ w ∈ s, 0 ≤ φ s w

@[simp]

theorem EgreRossiSprenger2026b.Sentence.accepts_empty {W : Type u_1} (φ : Sentence W) : Accepts ∅ φ

theorem EgreRossiSprenger2026b.Sentence.accepts_update {W : Type u_1} (s : Set W) (φ : Sentence W) : Accepts (update s φ) φ

An update accepts the sentence it updates on, the property that sets updates apart from restrictions.

theorem EgreRossiSprenger2026b.Sentence.update_eq_self_of_accepts {W : Type u_1} {φ : Sentence W} {s : Set W} (h : Accepts s φ) : update s φ = s

A context that accepts a sentence survives the update on it whole.

theorem EgreRossiSprenger2026b.Sentence.update_eq_empty_of_uniform {W : Type u_1} {φ : Sentence W} {s : Set W} (hu : ∀ w ∈ s, ∀ w' ∈ s, φ s w = φ s w') (h : ¬Accepts s φ) : update s φ = ∅

A context collapses under the update on a sentence that is uniform across it and that it does not accept.

theorem EgreRossiSprenger2026b.Sentence.update_eq_empty_of_forall_not_accepts {W : Type u_1} {φ : Sentence W} (h : ∀ (t : Set W), t.Nonempty → ¬Accepts t φ) (s : Set W) : update s φ = ∅

No nonempty context accepting a sentence, every update on it collapses.

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

A context accepts □A exactly when it accepts A, which gives Łukasiewicz's Principle and Strong must (Fact 7).

theorem EgreRossiSprenger2026b.Sentence.accepts_dia_iff {W : Type u_1} {φ : Sentence W} {s : Set W} : Accepts s φ.dia ↔ (∃ w ∈ s, φ s w = 1) ∨ ∀ w ∈ s, φ s w = 0

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

theorem EgreRossiSprenger2026b.Sentence.update_box_of_accepts {W : Type u_1} {φ : Sentence W} {s : Set W} (h : Accepts s φ) : update s φ.box = s

The update on □A keeps the context if it accepts A (Fact 2 for must)...

theorem EgreRossiSprenger2026b.Sentence.update_box_of_not_accepts {W : Type u_1} {φ : Sentence W} {s : Set W} (h : ¬Accepts s φ) : update s φ.box = ∅

... and collapses it otherwise.

theorem EgreRossiSprenger2026b.Sentence.update_dia_of {W : Type u_1} {φ : Sentence W} {s : Set W} (h : (∃ w ∈ s, φ s w = 1) ∨ ∀ w ∈ s, φ s w = 0) : update s φ.dia = s

The update on ◇A keeps the context if A is true somewhere in it or void throughout it (Fact 2 for might)...

theorem EgreRossiSprenger2026b.Sentence.update_dia_of_not {W : Type u_1} {φ : Sentence W} {s : Set W} (h : ¬((∃ w ∈ s, φ s w = 1) ∨ ∀ w ∈ s, φ s w = 0)) : update s φ.dia = ∅

... and collapses it otherwise.

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

A context accepts A → B exactly when its update on A accepts B.

Nonmodal sentences and Cooper's conditional

def EgreRossiSprenger2026b.Sentence.ofCooper {W : Type u_1} (p : W → SignType) : Sentence W

The nonmodal sentence with Cooper value p at each world, whatever the context.

Equations

• EgreRossiSprenger2026b.Sentence.ofCooper p x✝ = p

@[simp]

theorem EgreRossiSprenger2026b.Sentence.ofCooper_apply {W : Type u_1} (p : W → SignType) (s : Set W) (w : W) : ofCooper p s w = p w

theorem EgreRossiSprenger2026b.Sentence.contextFree_ofCooper {W : Type u_1} (p : W → SignType) : (ofCooper p).ContextFree

theorem EgreRossiSprenger2026b.Sentence.ContextFree.eq_ofCooper {W : Type u_1} {φ : Sentence W} (h : φ.ContextFree) : φ = ofCooper fun (w : W) => φ ∅ w

A nonmodal sentence is the sentence of its Cooper values.

theorem EgreRossiSprenger2026b.Sentence.cond_ofCooper {W : Type u_1} (p q : W → SignType) : (ofCooper p).cond (ofCooper q) = ofCooper fun (w : W) => SignType.condAssert Trivalent.Designation.lp (p w) (q w)

On nonmodal sentences the conditional is Cooper's connective at every world, inside the context or outside it, the reduction (i) of §3.5.

theorem EgreRossiSprenger2026b.Sentence.ContextFree.cond {W : Type u_1} {φ ψ : Sentence W} (hφ : φ.ContextFree) (hψ : ψ.ContextFree) : (φ.cond ψ).ContextFree

theorem EgreRossiSprenger2026b.Sentence.ContextFree.update_update {W : Type u_1} {φ ψ : Sentence W} (hφ : φ.ContextFree) (hψ : ψ.ContextFree) (s : Set W) : update (update s φ) ψ = update s (φ.conj ψ)

Updating on nonmodal sentences in turn is updating on their conjunction (Update Commutativity, Proposition 3).

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

theorem EgreRossiSprenger2026b.Sentence.ContextFree.cond_cond {W : Type u_1} {φ ψ : Sentence W} (hφ : φ.ContextFree) (hψ : ψ.ContextFree) (χ : Sentence W) : φ.cond (ψ.cond χ) = (φ.conj ψ).cond χ

Corollary 1, Import-Export for nonmodal antecedents, whatever the consequent.

Consequence (Definition 9)

TT-consequence preserves acceptance across every context of the world space; with the meanings fixed, a schema valid for all meanings holds in particular for those the paper's formulas take in any model.

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

TT-consequence: every context accepting the premises accepts the conclusion.

Equations

• EgreRossiSprenger2026b.Entails Γ ψ = ∀ (s : Set W), (∀ φ ∈ Γ, EgreRossiSprenger2026b.Sentence.Accepts s φ) → EgreRossiSprenger2026b.Sentence.Accepts s ψ

theorem EgreRossiSprenger2026b.Sentence.Accepts.of_cond {W : Type u_1} {φ ψ : Sentence W} {s : Set W} (h₁ : Accepts s (φ.cond ψ)) (h₂ : Accepts s φ) : Accepts s ψ

A context accepting A → B and A accepts B.

theorem EgreRossiSprenger2026b.modus_ponens {W : Type u_1} (φ ψ : Sentence W) : Entails {φ.cond ψ, φ} ψ

Fact 10, Modus Ponens, for arbitrary sentences.

theorem EgreRossiSprenger2026b.accepts_cond_box_iff {W : Type u_1} {φ ψ : Sentence W} {s : Set W} : Sentence.Accepts s (φ.cond ψ.box) ↔ Sentence.Accepts s (φ.cond ψ)

A context accepts A → B exactly when it accepts A → □B (Theorem 1, acceptance half)...

theorem EgreRossiSprenger2026b.accepts_box_cond_iff {W : Type u_1} {φ ψ : Sentence W} {s : Set W} : Sentence.Accepts s (φ.cond ψ).box ↔ Sentence.Accepts s (φ.cond ψ)

... and exactly when it accepts □(A → B).

theorem EgreRossiSprenger2026b.entails_cond_box {W : Type u_1} (φ ψ : Sentence W) : Entails {φ.cond ψ} (φ.cond ψ.box) ∧ Entails {φ.cond ψ.box} (φ.cond ψ)

A → B and A → □B entail each other, the covert epistemic must (Corollary 2).

theorem EgreRossiSprenger2026b.entails_box {W : Type u_1} (φ : Sentence W) : Entails {φ} φ.box ∧ Entails {φ.box} φ

A and □A entail each other, Łukasiewicz's Principle and Strong must (Fact 7).

theorem EgreRossiSprenger2026b.schema_K {W : Type u_1} (φ ψ : Sentence W) (s : Set W) : Sentence.Accepts s ((φ.cond ψ).box.cond (φ.box.cond ψ.box))

Every context accepts □(A → B) → (□A → □B) (Schema K, Fact 6).

theorem EgreRossiSprenger2026b.accepts_cond_dia_iff {W : Type u_1} {φ ψ : Sentence W} {s : Set W} : Sentence.Accepts s (φ.cond ψ.dia) ↔ Sentence.Accepts s (φ.cond ψ).dia

Might commutes with the conditional at the level of acceptance (Fact 8).

theorem EgreRossiSprenger2026b.accepts_cond_box_iff_box_cond {W : Type u_1} {φ ψ : Sentence W} {s : Set W} : Sentence.Accepts s (φ.cond ψ.box) ↔ Sentence.Accepts s (φ.cond ψ).box

Fact 8, the must half, is Theorem 1.

Structural properties (Proposition 4)

theorem EgreRossiSprenger2026b.entails_refl {W : Type u_1} (φ : Sentence W) : Entails {φ} φ

theorem EgreRossiSprenger2026b.Entails.mono {W : Type u_1} {ψ : Sentence W} {Γ Δ : Set (Sentence W)} (h : Entails Γ ψ) (hΓΔ : Γ ⊆ Δ) : Entails Δ ψ

theorem EgreRossiSprenger2026b.Entails.trans {W : Type u_1} {ψ : Sentence W} {Γ Δ Θ : Set (Sentence W)} (hΘ : ∀ φ ∈ Θ, Entails Γ φ) (h : Entails (Θ ∪ Δ) ψ) : Entails (Γ ∪ Δ) ψ

theorem EgreRossiSprenger2026b.entails_insert_iff {W : Type u_1} {φ ψ : Sentence W} {Γ : Set (Sentence W)} (hΓ : ∀ χ ∈ Γ, χ.ContextFree) : Entails (insert φ Γ) ψ ↔ Entails Γ (φ.cond ψ)

For nonmodal premises the Deduction Theorem holds (Theorem 3), because their acceptance survives the update on the hypothesis.

Domain semantics on the conditional-free fragment

On sentences without conditionals, the valuations of Definition 3 are [Yal07]'s domain semantics, equation (1): a trivalent sentence agrees with a domain-semantic one when it is two-valued at every world of every context and true exactly where the other is. The Boolean connectives and the modals preserve agreement, so the paper's verdicts on epistemic contradictions are Yalcin's theorems (Fact 5).

def EgreRossiSprenger2026b.Agrees {W : Type u_1} (φ : Sentence W) (ψ : Yalcin2007.Sentence W) : Prop

φ agrees with the domain-semantic sentence ψ at every world of every context.

Equations

• EgreRossiSprenger2026b.Agrees φ ψ = ∀ (s : Set W), ∀ w ∈ s, φ s w = SignType.ofProp (ψ s w)

theorem EgreRossiSprenger2026b.agrees_ofSet {W : Type u_1} (p : Set W) : Agrees (Sentence.ofSet p) (Yalcin2007.Sentence.ofProp p)

theorem EgreRossiSprenger2026b.Agrees.neg {W : Type u_1} {φ : Sentence W} {ψ : Yalcin2007.Sentence W} (h : Agrees φ ψ) : Agrees (-φ) ψᶜ

theorem EgreRossiSprenger2026b.Agrees.conj {W : Type u_1} {φ φ' : Sentence W} {ψ ψ' : Yalcin2007.Sentence W} (h : Agrees φ ψ) (h' : Agrees φ' ψ') : Agrees (φ.conj φ') (ψ ⊓ ψ')

theorem EgreRossiSprenger2026b.Agrees.dia {W : Type u_1} {φ : Sentence W} {ψ : Yalcin2007.Sentence W} (h : Agrees φ ψ) : Agrees φ.dia ψ.might

theorem EgreRossiSprenger2026b.Agrees.box {W : Type u_1} {φ : Sentence W} {ψ : Yalcin2007.Sentence W} (h : Agrees φ ψ) : Agrees φ.box ψ.must

theorem EgreRossiSprenger2026b.Agrees.accepts_iff {W : Type u_1} {φ : Sentence W} {ψ : Yalcin2007.Sentence W} (h : Agrees φ ψ) {s : Set W} : Sentence.Accepts s φ ↔ ψ.AcceptedIn s

Agreeing sentences are accepted in the same contexts.

theorem EgreRossiSprenger2026b.not_accepts_contra' {W : Type u_1} {s : Set W} (hs : s.Nonempty) (q : Set W) : ¬Sentence.Accepts s ((Sentence.ofSet q).conj (-Sentence.ofSet q).dia)

No nonempty context accepts the epistemic contradiction q ∧ ◇¬q (Fact 5), which on the conditional-free fragment is Yalcin2007.not_accepted_contra'...

theorem EgreRossiSprenger2026b.update_contra' {W : Type u_1} (s q : Set W) : Sentence.update s ((Sentence.ofSet q).conj (-Sentence.ofSet q).dia) = ∅

... and every update on it collapses.

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

The epistemic contradiction ¬p ∧ ◇p is [Yal07]'s contra...

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

... and so is its mirror image ◇p ∧ ¬p, the antecedent of (19).

theorem EgreRossiSprenger2026b.import_export_fails : (Sentence.ofSet {true}).dia.cond ((-Sentence.ofSet {true}).cond (Sentence.ofSet Set.univ)) Set.univ false = 1 ∧ ((Sentence.ofSet {true}).dia.conj (-Sentence.ofSet {true})).cond (Sentence.ofSet Set.univ) Set.univ false = 0

Import-Export fails for a modal antecedent, (18) against (19): where p is possible the update on ◇p is idle, so ◇p → (¬p → q) is ¬p → q and true at a ¬p-world where q holds, while the update on ◇p ∧ ¬p collapses and (◇p ∧ ¬p) → q is void.

Inference with conditionals and modals (§5)

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

theorem EgreRossiSprenger2026b.accepts_cond_ofSet_iff {W : Type u_1} {s p : Set W} {φ : Sentence W} : Sentence.Accepts s ((Sentence.ofSet p).cond φ) ↔ Sentence.Accepts (s ∩ p) φ

theorem EgreRossiSprenger2026b.conj_ofSet {W : Type u_1} (p q : Set W) : (Sentence.ofSet p).conj (Sentence.ofSet q) = Sentence.ofSet (p ∩ q)

theorem EgreRossiSprenger2026b.disj_ofSet {W : Type u_1} (p q : Set W) : (Sentence.ofSet p).disj (Sentence.ofSet q) = Sentence.ofSet (p ∪ q)

theorem EgreRossiSprenger2026b.accepts_dia_ofSet_iff {W : Type u_1} {s p : Set W} : Sentence.Accepts s (Sentence.ofSet p).dia ↔ s.Nonempty → (s ∩ p).Nonempty

theorem EgreRossiSprenger2026b.cond_ofSet_empty {W : Type u_1} (φ : Sentence W) : (Sentence.ofSet ∅).cond φ = 0

A conditional with an impossible antecedent is void everywhere.

theorem EgreRossiSprenger2026b.accepts_zero {W : Type u_1} (s : Set W) : Sentence.Accepts s 0

theorem EgreRossiSprenger2026b.update_dia_ofSet {W : Type u_1} (s p : Set W) : Sentence.update s (Sentence.ofSet p).dia = (DynamicSemantics.CCP.up p).might s

Fact 2 on a conditional-free prejacent is [Vel96]'s might: the update on ◇p tests whether p is open in the context.

theorem EgreRossiSprenger2026b.entails_dia_conj {W : Type u_1} (a b : Set W) : Entails {(Sentence.ofSet a).dia, (Sentence.ofSet a).cond (Sentence.ofSet b).dia} ((Sentence.ofSet a).conj (Sentence.ofSet b)).dia

For conditional-free A and B, ◇A, A → ◇B ⊨ ◇(A ∧ B) (Fact 9)...

theorem EgreRossiSprenger2026b.entails_cond_dia {W : Type u_1} (a b : Set W) : Entails {((Sentence.ofSet a).conj (Sentence.ofSet b)).dia} ((Sentence.ofSet a).cond (Sentence.ofSet b).dia)

... and ◇(A ∧ B) ⊨ A → ◇B.

theorem EgreRossiSprenger2026b.not_entails_dia_conj : ¬Entails {(Sentence.ofSet ∅).cond (Sentence.ofSet Set.univ).dia} ((Sentence.ofSet ∅).conj (Sentence.ofSet Set.univ)).dia

Without the premise ◇A the first entailment fails. If my team wins out, they might win it all (27) does not entail it might turn out that my team wins out and wins it all (26), since a context excluding A accepts the conditional vacuously.

def EgreRossiSprenger2026b.NeverVoid {W : Type u_1} (φ : Sentence W) : Prop

A sentence never void at a world of its context, as every conditional-free sentence is.

Equations

• EgreRossiSprenger2026b.NeverVoid φ = ∀ (s : Set W), ∀ w ∈ s, φ s w ≠ 0

theorem EgreRossiSprenger2026b.neverVoid_ofSet {W : Type u_1} (p : Set W) : NeverVoid (Sentence.ofSet p)

theorem EgreRossiSprenger2026b.eq_empty_of_accepts_neg_dia {W : Type u_1} {s : Set W} {φ : Sentence W} (hφ : NeverVoid φ) (h₁ : Sentence.Accepts s (-φ)) (h₂ : Sentence.Accepts s φ.dia) : s = ∅

Proposition 5, the is-might contradiction: no nonempty context accepts both ¬B and ◇B for a never-void B, that is, ¬B, ◇B ⊨ ⊥.

theorem EgreRossiSprenger2026b.eq_empty_of_if_might {W : Type u_1} {s : Set W} {φ ψ : Sentence W} (hφ : φ.ContextFree) (hψ : NeverVoid ψ) (h₀ : Sentence.Accepts s φ.dia) (h₁ : Sentence.Accepts s (φ.cond (-ψ))) (h₂ : Sentence.Accepts s (φ.cond ψ.dia)) : s = ∅

Proposition 5, the if-might contradiction: for nonmodal A and never-void B, ◇A, A → ¬B, A → ◇B ⊨ ⊥.

theorem EgreRossiSprenger2026b.not_entails_of_dia : ¬Entails {(Sentence.ofSet {true}).dia} (Sentence.ofSet {true})

Proposition 5, non-veridical might: ◇C ⊭ C.

theorem EgreRossiSprenger2026b.not_entails_neg_box : ¬Entails {-(Sentence.ofSet {true}).box} (-Sentence.ofSet {true})

Replacement of Logical Equivalents fails for must (§5), since □A ⊨ A but ¬□A ⊭ ¬A.

theorem EgreRossiSprenger2026b.modus_tollens {W : Type u_1} (a b : Set W) : Entails {(Sentence.ofSet a).cond (Sentence.ofSet b), -Sentence.ofSet b} (-Sentence.ofSet a)

Modus Tollens holds for conditional-free sentences (Fact 11)...

theorem EgreRossiSprenger2026b.not_modus_tollens_void : ¬Entails {(Sentence.ofSet Set.univ).cond ((Sentence.ofSet ∅).cond (Sentence.ofSet ∅)), -(Sentence.ofSet ∅).cond (Sentence.ofSet ∅)} (-Sentence.ofSet Set.univ)

... but fails once the consequent may be void, at a true antecedent with a void consequent.

theorem EgreRossiSprenger2026b.not_modus_tollens_box : ¬Entails {(-Sentence.ofSet {true}).cond (Sentence.ofSet {false}).box, -(Sentence.ofSet {false}).box} (Sentence.ofSet {true})

... and fails for a modal consequent, [Yal12]'s marble (28): with a green and a black marble possible, if the marble is not green, it must be black and it is not the case that it must be black are accepted, the marble is green is not.

theorem EgreRossiSprenger2026b.not_contraposition_box : ¬Entails {(-Sentence.ofSet {true}).cond (Sentence.ofSet {false}).box} ((-(Sentence.ofSet {false}).box).cond (Sentence.ofSet {true}))

The marble also refutes contraposition, since ¬A → □B ⊭ ¬□B → A.

theorem EgreRossiSprenger2026b.entails_disj_ofSet {W : Type u_1} (p q : Set W) : Entails {Sentence.ofSet p} ((Sentence.ofSet p).disj (Sentence.ofSet q))

Uniform Substitution fails (Proposition 4). Although p ⊨ p ∨ q for conditional-free p...

theorem EgreRossiSprenger2026b.not_entails_disj_cond : ¬Entails {(Sentence.ofSet ∅).cond (Sentence.ofSet ∅)} (((Sentence.ofSet ∅).cond (Sentence.ofSet ∅)).disj (Sentence.ofSet ∅))

... but not when a void conditional is substituted for p.

theorem EgreRossiSprenger2026b.entails_cond_iff_disj {W : Type u_1} (p q : Set W) : Entails {(Sentence.ofSet p).cond (Sentence.ofSet q)} ((-Sentence.ofSet p).disj (Sentence.ofSet q)) ∧ Entails {(-Sentence.ofSet p).disj (Sentence.ofSet q)} ((Sentence.ofSet p).cond (Sentence.ofSet q))

Replacement of Logical Equivalents fails (Proposition 4). For conditional-free p and q, p → q and ¬p ∨ q are equivalent...

theorem EgreRossiSprenger2026b.not_entails_neg_cond_neg_disj : ¬Entails {-(Sentence.ofSet ∅).cond (Sentence.ofSet ∅)} (-(-Sentence.ofSet ∅).disj (Sentence.ofSet ∅))

... but their negations are not.

theorem EgreRossiSprenger2026b.entails_of_dia_neg {W : Type u_1} (p q : Set W) : Entails {Sentence.ofSet p, Sentence.ofSet q, (-Sentence.ofSet p).dia} (-Sentence.ofSet q)

Conditional Proof fails with modal premises (§5). q, ◇¬p, p ⊨ ¬q, since no nonempty context accepts both p and ◇¬p...

theorem EgreRossiSprenger2026b.not_entails_cond_of_dia_neg : ¬Entails {Sentence.ofSet Set.univ, (-Sentence.ofSet {true}).dia} ((Sentence.ofSet {true}).cond (-Sentence.ofSet Set.univ))

... yet q, ◇¬p ⊭ p → ¬q, in footnote 18's model of a pq-world and a ¬pq-world.

theorem EgreRossiSprenger2026b.not_accepts_fn18_printed : ¬Sentence.Accepts Set.univ ((Sentence.ofSet Set.univ).conj (-(Sentence.ofSet {true}).dia))

Footnote 18 prints the premise as q ∧ ¬◇p, which its own model does not accept; the main text's ◇¬p is meant.

Probability and acceptance (§4)

A credence over the worlds gives each sentence, at a context, the trivalent probability of [ERS26b] (Definition 5). Mirroring coordinates the credence with the context. Definition 6 asks only that the credence give the context probability 1, but the paper uses it as regularity on the context, a credence positive at exactly the context's worlds (footnote 8 and the proof of Theorem 2), and under the literal reading the probability half of Theorem 1 fails (not_prob_cond_box_eq_of_literal). Mirrors is the regular reading.

def EgreRossiSprenger2026b.Mirrors {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (s : Set W) : Prop

A credence mirrors a context when its positive-weight worlds are exactly the context's.

Equations

• EgreRossiSprenger2026b.Mirrors μ s = ∀ (w : W), μ {w} ≠ 0 ↔ w ∈ s

theorem EgreRossiSprenger2026b.Mirrors.measure_eq_zero_iff {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} [Countable W] (h : Mirrors μ s) {t : Set W} : μ t = 0 ↔ ∀ w ∈ t, w ∉ s

Under mirroring, a set is null exactly when it misses the context.

theorem EgreRossiSprenger2026b.Mirrors.prob_eq_one_iff' {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) {f : W → SignType} : Trivalent.prob μ f = 1 ↔ ∀ w ∈ s, f w ≠ -1

theorem EgreRossiSprenger2026b.Mirrors.prob_eq_zero_iff' {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) {f : W → SignType} : Trivalent.prob μ f = 0 ↔ (∀ w ∈ s, f w ≠ 1) ∧ ∃ w ∈ s, f w = -1

theorem EgreRossiSprenger2026b.Mirrors.prob_eq_one_iff {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} {φ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) : Trivalent.prob μ (φ s) = 1 ↔ Sentence.Accepts s φ

Under mirroring, probability 1 is acceptance (§4.1).

theorem EgreRossiSprenger2026b.Mirrors.prob_eq_zero_or_one {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) {f : W → SignType} (hu : ∀ w ∈ s, ∀ w' ∈ s, f w = f w') : Trivalent.prob μ f = 0 ∨ Trivalent.prob μ f = 1

A sentence uniform across the context has probability 0 or 1 under a credence mirroring it.

theorem EgreRossiSprenger2026b.prob_box_eq_zero_or_one {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} {φ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) : Trivalent.prob μ (φ.box s) = 0 ∨ Trivalent.prob μ (φ.box s) = 1

Under a mirroring credence, must sentences have probability 0 or 1 (Fact 4)...

theorem EgreRossiSprenger2026b.prob_dia_eq_zero_or_one {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} {φ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) : Trivalent.prob μ (φ.dia s) = 0 ∨ Trivalent.prob μ (φ.dia s) = 1

... and so do might sentences.

theorem EgreRossiSprenger2026b.prob_cond_box_eq_zero {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} {φ ψ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) (hn : ¬Sentence.Accepts s (φ.cond ψ)) : Trivalent.prob μ (φ.cond ψ.box s) = 0

theorem EgreRossiSprenger2026b.prob_box_cond_eq_zero {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} {φ ψ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) (hn : ¬Sentence.Accepts s (φ.cond ψ)) : Trivalent.prob μ ((φ.cond ψ).box s) = 0

theorem EgreRossiSprenger2026b.prob_cond_box_le {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} {φ ψ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) : Trivalent.prob μ (φ.cond ψ.box s) ≤ Trivalent.prob μ (φ.cond ψ s)

Under a mirroring credence A → □B is never more probable than A → B (Theorem 1, probability half)...

theorem EgreRossiSprenger2026b.prob_cond_box_eq_prob_box_cond {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {s : Set W} {φ ψ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : Mirrors μ s) : Trivalent.prob μ (φ.cond ψ.box s) = Trivalent.prob μ ((φ.cond ψ).box s)

... and exactly as probable as □(A → B).

theorem EgreRossiSprenger2026b.not_prob_cond_box_eq_of_literal : ∃ (μ : MeasureTheory.Measure Bool), MeasureTheory.IsProbabilityMeasure μ ∧ μ Set.univ = 1 ∧ Trivalent.prob μ ((Sentence.ofSet {true}).cond (-Sentence.ofSet {true}).box Set.univ) ≠ Trivalent.prob μ (((Sentence.ofSet {true}).cond (-Sentence.ofSet {true})).box Set.univ)

Under Definition 6 read literally, a credence giving the context probability 1 without positive weight at each of its worlds, the probability half of Theorem 1 fails: concentrated on a ¬p-world, the credence makes p → □¬p certain by All Void and □(p → ¬p) impossible.

theorem EgreRossiSprenger2026b.mirrors_uniformOn {W : Type u_1} [MeasurableSpace W] [Countable W] [DiscreteMeasurableSpace W] [Finite W] (s : Set W) : Mirrors (ProbabilityTheory.uniformOn s) s

The uniform credence on a finite context mirrors it.

theorem EgreRossiSprenger2026b.exists_mirrors {W : Type u_1} [MeasurableSpace W] {s : Set W} [Countable W] [DiscreteMeasurableSpace W] [Finite W] (hs : s.Nonempty) : ∃ (μ : MeasureTheory.Measure W), MeasureTheory.IsProbabilityMeasure μ ∧ Mirrors μ s

A finite nonempty context has a mirroring credence, the uniform one.

theorem EgreRossiSprenger2026b.accepts_iff_forall_mirrors {W : Type u_1} [MeasurableSpace W] {s : Set W} {φ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [Finite W] : Sentence.Accepts s φ ↔ ∀ (μ : MeasureTheory.Measure W), MeasureTheory.IsProbabilityMeasure μ → Mirrors μ s → Trivalent.prob μ (φ s) = 1

Acceptance is probability 1 under every credence mirroring the context (Definition 7).

def EgreRossiSprenger2026b.CEntails {W : Type u_1} [MeasurableSpace W] (Γ : Set (Sentence W)) (ψ : Sentence W) : Prop

An inference preserves certainty (Definition 8) when every credence mirroring a context that makes the premises certain makes the conclusion certain.

Equations

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

theorem EgreRossiSprenger2026b.cEntails_iff_entails {W : Type u_1} [MeasurableSpace W] {ψ : Sentence W} [Countable W] [DiscreteMeasurableSpace W] [Finite W] {Γ : Set (Sentence W)} : CEntails Γ ψ ↔ Entails Γ ψ

Certainty preservation is acceptance preservation (Theorem 2).

Predictions

theorem EgreRossiSprenger2026b.cond_ofSet {W : Type u_1} (a b : Set W) : (Sentence.ofSet a).cond (Sentence.ofSet b) = Sentence.ofCooper (EgreRossiSprenger2026a.ofAdams { ante := a, cons := b })

The conditional between conditional-free sentences denotes, in every context, the conditional event of [ERS26b]'s reading of an Adams formula.

theorem EgreRossiSprenger2026b.prob_cond_contra {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (q : Set W) (φ : Sentence W) (s : Set W) : Trivalent.prob μ (((-Sentence.ofSet q).conj (Sentence.ofSet q).dia).cond φ s) = 1

A conditional whose antecedent is an epistemic contradiction is void throughout, so its probability is 1 by All Void, under every credence and at every context (footnote 11).

theorem EgreRossiSprenger2026b.prob_cond_ofSet {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] {μ : MeasureTheory.Measure W} {a : Set W} (b : Set W) (h : μ a ≠ 0) (s : Set W) : Trivalent.prob μ ((Sentence.ofSet a).cond (Sentence.ofSet b) s) = μ[b | a]

For conditional-free A and B, the probability of A → B is the conditional probability of B given A (Adams's Thesis, §4.1), at every context and under every credence, since the degenerate clause makes nonmodal sentences context-independent.

theorem EgreRossiSprenger2026b.prob_contra'_coin : Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) ((Sentence.ofSet {true}).conj (-Sentence.ofSet {true}).dia Set.univ) = 1 / 2

On a fair coin the epistemic contradiction the coin is facing heads and might not face heads has probability 1/2, true at the heads world and false at the tails world (footnote 12).

theorem EgreRossiSprenger2026b.die_bare_vs_must : Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) ((Sentence.ofSet Set.univ).cond (Sentence.ofSet {w : Fin 6 | w ≠ 0}) Set.univ) = 5 / 6 ∧ Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) ((Sentence.ofSet Set.univ).cond (Sentence.ofSet {w : Fin 6 | w ≠ 0}).box Set.univ) = 0

If the die has been tossed, the outcome is greater than 1 (20) has probability 5/6 and if the die has been tossed, the outcome must be greater than 1 (21) probability 0, though a context accepts the one exactly when it accepts the other.

The nonmodal fragment is the Mind paper's language

The Cooper valuations of Definition 1 are those of [ERS26b], and the conditional–modal semantics extends them: a formula of that paper's language denotes the nonmodal sentence of its Cooper values, and the connectives commute with the embedding.

def EgreRossiSprenger2026b.ofFormula {W : Type u_1} {ι : Type u_2} (t : W → ι → Bool) (A : Trivalent.Formula ι) : Sentence W

The nonmodal sentence a formula of the conditional language expresses, at worlds whose atoms t values.

Equations

• EgreRossiSprenger2026b.ofFormula t A = EgreRossiSprenger2026b.Sentence.ofCooper (EgreRossiSprenger2026a.value t A)

theorem EgreRossiSprenger2026b.contextFree_ofFormula {W : Type u_1} {ι : Type u_2} (t : W → ι → Bool) (A : Trivalent.Formula ι) : (ofFormula t A).ContextFree

@[simp]

theorem EgreRossiSprenger2026b.ofFormula_neg {W : Type u_1} {ι : Type u_2} (t : W → ι → Bool) (A : Trivalent.Formula ι) : ofFormula t A.neg = -ofFormula t A

@[simp]

theorem EgreRossiSprenger2026b.ofFormula_conj {W : Type u_1} {ι : Type u_2} (t : W → ι → Bool) (A B : Trivalent.Formula ι) : ofFormula t (A.conj B) = (ofFormula t A).conj (ofFormula t B)

@[simp]

theorem EgreRossiSprenger2026b.ofFormula_disj {W : Type u_1} {ι : Type u_2} (t : W → ι → Bool) (A B : Trivalent.Formula ι) : ofFormula t (A.disj B) = (ofFormula t A).disj (ofFormula t B)

@[simp]

theorem EgreRossiSprenger2026b.ofFormula_cond {W : Type u_1} {ι : Type u_2} (t : W → ι → Bool) (A B : Trivalent.Formula ι) : ofFormula t (A.cond B) = (ofFormula t A).cond (ofFormula t B)

The conditional–modal conditional restricts to Cooper's on the Mind paper's formulas.