Égré, Rossi and Sprenger (2026): Probability for Trivalent Conditionals

Égré, Rossi and Sprenger give a unified truth-conditional and probabilistic theory of indicative conditionals on Cooper's trivalent tables: the conditional asserts its consequent where its antecedent is non-false, conjunction and disjunction skip the void value, and the probability of a sentence is the weight of its truth against that of its truth and falsity together. The semantics validates a Reduction Theorem, every compound of conditionals is equivalent to a simple conditional, and the probability function validates Adams's Thesis and, through Import-Export, Stalnaker's Thesis in full generality, escaping the triviality results by giving up classical conjunction and the Product Rule.

Main statements

• equiv_neg_cond, equiv_cond_cond, equiv_conj_cond, equiv_disj_cond, equiv_cond_left: Proposition 1, the five equivalences, each at the generality the paper claims for it, with conjunction_needs_boolean and sk_fails_conjunction marking where the laws stop.
• cooperEval_flat: the Reduction Theorem, by the appendix's recursion flat.
• prob_value_neg, prob_value_disj: the second and third principles of trivalent probability; additivity_all_void shows the third fails without properness, which the paper does not flag.
• ofAdams, exists_ofAdams_eq, ofAdams_eq_ofAdams_iff, prob_ofAdams: an [Ada75] formula denotes the conditional event of its consequent on its antecedent, these exhaust the trivalent propositions (the semantic content of the Reduction Theorem), and its trivalent probability is Adams's conditional probability; hence adams_thesis, and pEntails_iff_prob restates p-entailment in trivalent probabilities.
• cEntails_iff_forall_prob: preserving probability 1 is preserving designated values, the trivalent characterization of the logic C.
• prob_cond_eq_one_of_cEntails, prob_cond_congr_left, prob_cond_disj: the axioms 3′, 4′ and 5′ of trivalent conditional probability; axiom2'_all_void and additivity_cond_all_void show 2′ and 5′ fail as printed in the all-void case.
• stalnaker_thesis: p_A(B → C) = p_{A ∧ B}(C) with no hypotheses at all, since Import-Export is a pointwise identity.
• prob_cond_material_eq: learning a simple conditional is learning the material conditional (Proposition 6).
• goldstein_santorio_die, santorio_wellwood_die, edgington_coin: the die and coin examples of [GS21], [SW23a] and [Edg91], computed in the fair models; prob_conj_gt is the failure of p(X ∧ Y) ≤ p(X).

Implementation notes

• The language is the shared Trivalent.Formula and a Cooper valuation is its evaluation by Trivalent.Connectives.cooper on a Boolean model, so the paper's ⊤ and ⊥ are the formulas p ∨ ¬p and p ∧ ¬p of an atom.
• Worlds carry a classical valuation of the atoms through a map t : W → ι → Bool, after the paper's identification of worlds with atom-classical valuations; a formula's value at a world is a SignType, and its probability is Trivalent.prob, which builds in the paper's All Void convention. With that convention axiom 3′ holds unconditionally. The second principle carries its own all-void exception, but the third principle and axioms 2′ and 5′ also need the relevant sentence to be non-void with positive credence, which the printed versions omit; additivity_all_void, axiom2'_all_void and additivity_cond_all_void are the counterexamples.
• The logic C is defined by its trivalent characterization, preservation of LP-designated values, which [ERS25] prove equivalent to preservation of probability 1; the equivalence is cEntails_iff_forall_prob, proved over the valuation space itself.
• The die and coin examples are stated against uniformOn Set.univ and computed by counting worlds through Trivalent.prob_uniformOn_univ.

TODO

• Theorem 2, the representation of the uncertain logic U in Adams's p-validity through the Reduction Theorem, and Propositions 3 and 4, its trivalent characterization and conservativity. With pEntails_iff_prob both sides are conditions on trivalent probability; what remains is Adams's equivalence of p-entailment with the uncertainty-sum criterion, open in Adams1975.
• Theorem 4, trivalent conditionalization as f-divergence minimization.
• McGee's adequacy conditions C2–C8 for the conditional probability p(A → B).

References

• [ERS26b]
• [ERS25]
• [Coo68]
• [dF36]
• [Ada65]
• [Ada75]
• [Lew76]
• [McG89]
• [GS21]
• [SW23a]
• [Edg91]

Cooper's laws at the value level

The laws of Proposition 1 are pointwise facts about SignType.condAssert at the LP standard and the Belnap connectives, each with the classicality hypotheses the paper gives it.

theorem EgreRossiSprenger2026a.condAssert_lp_meetBelnap_left {a b c : SignType} : SignType.condAssert Trivalent.Designation.lp (a.meetBelnap b) c = SignType.condAssert Trivalent.Designation.lp (min a b) c

Cooper's conditional at a Cooper conjunction is the conditional at the Strong Kleene conjunction: both are designated exactly when both conjuncts are.

theorem EgreRossiSprenger2026a.meetBelnap_condAssert_condAssert {a b c d : SignType} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hd : d ≠ 0) : (SignType.condAssert Trivalent.Designation.lp a b).meetBelnap (SignType.condAssert Trivalent.Designation.lp c d) = SignType.condAssert Trivalent.Designation.lp (a.joinBelnap c) (((-a).joinBelnap b).meetBelnap ((-c).joinBelnap d))

For classical values, a Cooper conjunction of conditionals asserts the conjoined material conditionals on the disjoined antecedents (Conjunction, Proposition 1).

theorem EgreRossiSprenger2026a.joinBelnap_condAssert_condAssert {a b c d : SignType} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hd : d ≠ 0) : (SignType.condAssert Trivalent.Designation.lp a b).joinBelnap (SignType.condAssert Trivalent.Designation.lp c d) = SignType.condAssert Trivalent.Designation.lp (a.joinBelnap c) ((a.meetBelnap b).joinBelnap (c.meetBelnap d))

Dually, a Cooper disjunction of conditionals asserts the disjoined conjunctions on the disjoined antecedents (Disjunction, Proposition 1).

theorem EgreRossiSprenger2026a.conjunction_needs_boolean : ¬∀ (a b c d : SignType), (SignType.condAssert Trivalent.Designation.lp a b).meetBelnap (SignType.condAssert Trivalent.Designation.lp c d) = SignType.condAssert Trivalent.Designation.lp (a.joinBelnap c) (((-a).joinBelnap b).meetBelnap ((-c).joinBelnap d))

Conjunction does not extend to trivalent conjuncts.

theorem EgreRossiSprenger2026a.sk_fails_conjunction : ¬∀ (a b c d : SignType), a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → min (SignType.condAssert Trivalent.Designation.lp a b) (SignType.condAssert Trivalent.Designation.lp c d) = SignType.condAssert Trivalent.Designation.lp (a.joinBelnap c) (((-a).joinBelnap b).meetBelnap ((-c).joinBelnap d))

With Strong Kleene conjunction in place of Cooper's, Conjunction fails already for classical values (footnote 6).

theorem EgreRossiSprenger2026a.condAssert_condAssert_material {a b c : SignType} (hb : b ≠ 0) : SignType.condAssert Trivalent.Designation.lp (SignType.condAssert Trivalent.Designation.lp a b) c = SignType.condAssert Trivalent.Designation.lp ((-a).joinBelnap b) c

Left-Nesting (Proposition 1): a conditional antecedent with classical consequent supposes exactly what the material conditional supposes.

theorem EgreRossiSprenger2026a.left_nesting_needs_boolean : ¬∀ (a b c : SignType), SignType.condAssert Trivalent.Designation.lp (SignType.condAssert Trivalent.Designation.lp a b) c = SignType.condAssert Trivalent.Designation.lp ((-a).joinBelnap b) c

Left-Nesting fails for a void consequent.

theorem EgreRossiSprenger2026a.condAssert_k3_left_eq_nested {a b c : SignType} (ha : a ≠ 0) (hb : b ≠ 0) : SignType.condAssert Trivalent.Designation.k3 (SignType.condAssert Trivalent.Designation.k3 a b) c = SignType.condAssert Trivalent.Designation.k3 a (SignType.condAssert Trivalent.Designation.k3 b c)

De Finetti's conditional identifies left with right nesting on classical values, so it cannot separate (A → B) → C from A → (B → C) (footnote 6).

theorem EgreRossiSprenger2026a.condAssert_k3_fails_left_nesting : ¬∀ (a b c : SignType), b ≠ 0 → SignType.condAssert Trivalent.Designation.k3 (SignType.condAssert Trivalent.Designation.k3 a b) c = SignType.condAssert Trivalent.Designation.k3 ((-a).joinBelnap b) c

... and it fails Cooper's Left-Nesting law.

theorem EgreRossiSprenger2026a.condAssert_condAssert_condAssert {a b c d : SignType} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hd : d ≠ 0) : SignType.condAssert Trivalent.Designation.lp (SignType.condAssert Trivalent.Designation.lp a b) (SignType.condAssert Trivalent.Designation.lp c d) = SignType.condAssert Trivalent.Designation.lp (((-a).joinBelnap b).meetBelnap c) d

For classical values (A → B) → (C → D) reduces to ((A ⊃ B) ∧ C) → D, the nested case of the Reduction Theorem.

theorem EgreRossiSprenger2026a.zero_le_sup_condAssert (d : Trivalent.Designation) (a b : SignType) : 0 ≤ max (SignType.condAssert d a b) (SignType.condAssert d b a)

Under Strong Kleene disjunction the linearity sentence (A → B) ∨ (B → A) is never false, at either designation standard, one reason the paper keeps Cooper's disjunction (footnote 3).

theorem EgreRossiSprenger2026a.meetBelnap_condAssert_of_false (b : SignType) : (SignType.condAssert Trivalent.Designation.lp (-1) b).meetBelnap 1 = 1

When c is true and a false, (a → b) ∧ c is just c, which is why McGee's Independence Principle fails on this semantics (footnote 11).

Cooper valuations

The language L→ is Trivalent.Formula, atoms closed under ¬, ∧, ∨ and →, and a Cooper valuation (Definition 1) evaluates it by Connectives.cooper on the Boolean model of a classical valuation of the atoms. The paper's ⊤ and ⊥ abbreviate a classical tautology and contradiction.

def EgreRossiSprenger2026a.cooperEval {ι : Type u_1} (v : ι → Bool) (φ : Trivalent.Formula ι) : SignType

The Cooper valuation induced by a classical valuation of the atoms (Definition 1), in which negation is Kleene's, conjunction and disjunction skip the void value, and the conditional asserts its consequent where its antecedent is non-false.

Equations

• EgreRossiSprenger2026a.cooperEval v φ = Trivalent.Formula.eval Trivalent.Connectives.cooper (Trivalent.Model.ofBool v) φ

def EgreRossiSprenger2026a.top {ι : Type u_1} (i : ι) : Trivalent.Formula ι

⊤, the classical tautology p ∨ ¬p.

Equations

• EgreRossiSprenger2026a.top i = (Trivalent.Formula.atom i).disj (Trivalent.Formula.atom i).neg

def EgreRossiSprenger2026a.bot {ι : Type u_1} (i : ι) : Trivalent.Formula ι

⊥, the classical contradiction p ∧ ¬p.

Equations

• EgreRossiSprenger2026a.bot i = (Trivalent.Formula.atom i).conj (Trivalent.Formula.atom i).neg

def EgreRossiSprenger2026a.material {ι : Type u_1} (φ ψ : Trivalent.Formula ι) : Trivalent.Formula ι

The material conditional ¬φ ∨ ψ, with Cooper's disjunction.

Equations

• EgreRossiSprenger2026a.material φ ψ = φ.neg.disj ψ

@[simp]

theorem EgreRossiSprenger2026a.cooperEval_atom {ι : Type u_1} {v : ι → Bool} (i : ι) : cooperEval v (Trivalent.Formula.atom i) = SignType.ofProp (v i = true)

@[simp]

theorem EgreRossiSprenger2026a.cooperEval_neg {ι : Type u_1} {v : ι → Bool} (φ : Trivalent.Formula ι) : cooperEval v φ.neg = -cooperEval v φ

@[simp]

theorem EgreRossiSprenger2026a.cooperEval_conj {ι : Type u_1} {v : ι → Bool} (φ ψ : Trivalent.Formula ι) : cooperEval v (φ.conj ψ) = (cooperEval v φ).meetBelnap (cooperEval v ψ)

@[simp]

theorem EgreRossiSprenger2026a.cooperEval_disj {ι : Type u_1} {v : ι → Bool} (φ ψ : Trivalent.Formula ι) : cooperEval v (φ.disj ψ) = (cooperEval v φ).joinBelnap (cooperEval v ψ)

@[simp]

theorem EgreRossiSprenger2026a.cooperEval_cond {ι : Type u_1} {v : ι → Bool} (φ ψ : Trivalent.Formula ι) : cooperEval v (φ.cond ψ) = SignType.condAssert Trivalent.Designation.lp (cooperEval v φ) (cooperEval v ψ)

@[simp]

theorem EgreRossiSprenger2026a.cooperEval_material {ι : Type u_1} {v : ι → Bool} (φ ψ : Trivalent.Formula ι) : cooperEval v (material φ ψ) = (-cooperEval v φ).joinBelnap (cooperEval v ψ)

@[simp]

theorem EgreRossiSprenger2026a.cooperEval_top {ι : Type u_1} {v : ι → Bool} (i : ι) : cooperEval v (top i) = 1

@[simp]

theorem EgreRossiSprenger2026a.cooperEval_bot {ι : Type u_1} {v : ι → Bool} (i : ι) : cooperEval v (bot i) = -1

def EgreRossiSprenger2026a.CooperEquiv {ι : Type u_1} (φ ψ : Trivalent.Formula ι) : Prop

Two formulas are semantically equivalent when every Cooper valuation gives them the same value (Definition 2).

Equations

• EgreRossiSprenger2026a.CooperEquiv φ ψ = ∀ (v : ι → Bool), EgreRossiSprenger2026a.cooperEval v φ = EgreRossiSprenger2026a.cooperEval v ψ

def EgreRossiSprenger2026a.NoCond {ι : Type u_1} : Trivalent.Formula ι → Prop

The conditional-free fragment L.

Equations

• EgreRossiSprenger2026a.NoCond (Trivalent.Formula.atom a) = True
• EgreRossiSprenger2026a.NoCond φ.neg = EgreRossiSprenger2026a.NoCond φ
• EgreRossiSprenger2026a.NoCond (φ.conj ψ) = (EgreRossiSprenger2026a.NoCond φ ∧ EgreRossiSprenger2026a.NoCond ψ)
• EgreRossiSprenger2026a.NoCond (φ.disj ψ) = (EgreRossiSprenger2026a.NoCond φ ∧ EgreRossiSprenger2026a.NoCond ψ)
• EgreRossiSprenger2026a.NoCond (a.cond a_1) = False

theorem EgreRossiSprenger2026a.NoCond.cooperEval_ne_zero {ι : Type u_1} {φ : Trivalent.Formula ι} (h : NoCond φ) (v : ι → Bool) : cooperEval v φ ≠ 0

Valuations are atom-classical and the conditional is the only source of the third value, so conditional-free formulas take classical values.

Proposition 1: the five equivalences

theorem EgreRossiSprenger2026a.equiv_neg_cond {ι : Type u_1} (φ ψ : Trivalent.Formula ι) : CooperEquiv (φ.cond ψ).neg (φ.cond ψ.neg)

Negating a conditional negates its consequent, for arbitrary formulas (Negation Commutation).

theorem EgreRossiSprenger2026a.equiv_cond_cond {ι : Type u_1} (φ ψ χ : Trivalent.Formula ι) : CooperEquiv (φ.cond (ψ.cond χ)) ((φ.conj ψ).cond χ)

Import-Export, for arbitrary formulas.

theorem EgreRossiSprenger2026a.equiv_conj_cond {ι : Type u_1} {φ ψ χ ξ : Trivalent.Formula ι} (hφ : NoCond φ) (hψ : NoCond ψ) (hχ : NoCond χ) (hξ : NoCond ξ) : CooperEquiv ((φ.cond ψ).conj (χ.cond ξ)) ((φ.disj χ).cond ((material φ ψ).conj (material χ ξ)))

Conjunction, for conditional-free components.

theorem EgreRossiSprenger2026a.equiv_disj_cond {ι : Type u_1} {φ ψ χ ξ : Trivalent.Formula ι} (hφ : NoCond φ) (hψ : NoCond ψ) (hχ : NoCond χ) (hξ : NoCond ξ) : CooperEquiv ((φ.cond ψ).disj (χ.cond ξ)) ((φ.disj χ).cond ((φ.conj ψ).disj (χ.conj ξ)))

Disjunction, for conditional-free components.

theorem EgreRossiSprenger2026a.equiv_cond_left {ι : Type u_1} {ψ : Trivalent.Formula ι} (hψ : NoCond ψ) (φ χ : Trivalent.Formula ι) : CooperEquiv ((φ.cond ψ).cond χ) ((material φ ψ).cond χ)

Left-Nesting, for a conditional-free inner consequent: in antecedent position an indicative and its material conditional express the same supposition.

The Reduction Theorem

def EgreRossiSprenger2026a.flat {ι : Type u_1} : Trivalent.Formula ι → Trivalent.Formula ι × Trivalent.Formula ι

The conditional-free antecedent and consequent of the simple conditional equivalent to a formula, by the appendix's recursion; an atom p is ⊤ → p.

Equations

• One or more equations did not get rendered due to their size.
• EgreRossiSprenger2026a.flat (Trivalent.Formula.atom a) = (EgreRossiSprenger2026a.top a, Trivalent.Formula.atom a)
• EgreRossiSprenger2026a.flat φ.neg = ((EgreRossiSprenger2026a.flat φ).1, (EgreRossiSprenger2026a.flat φ).2.neg)

theorem EgreRossiSprenger2026a.noCond_flat {ι : Type u_1} (φ : Trivalent.Formula ι) : NoCond (flat φ).1 ∧ NoCond (flat φ).2

theorem EgreRossiSprenger2026a.cooperEval_flat {ι : Type u_1} (φ : Trivalent.Formula ι) (v : ι → Bool) : cooperEval v φ = cooperEval v ((flat φ).1.cond (flat φ).2)

Every formula is semantically equivalent to the simple conditional flat computes (the Reduction Theorem, Theorem 1).

theorem EgreRossiSprenger2026a.reduction {ι : Type u_1} (φ : Trivalent.Formula ι) : ∃ (A : Trivalent.Formula ι) (B : Trivalent.Formula ι), NoCond A ∧ NoCond B ∧ CooperEquiv φ (A.cond B)

The flat fragment is as expressive as the whole language, Theorem 1 in the paper's form.

The logic C of certain inference

The paper takes from [ERS25] the logic C, preservation of probability 1, and its trivalent characterization as preservation of the LP-designated values. Here the characterization is the definition and the probabilistic description is the theorem.

def EgreRossiSprenger2026a.CEntails {ι : Type u_1} (Γ : List (Trivalent.Formula ι)) (B : Trivalent.Formula ι) : Prop

An inference is certain when every Cooper valuation designating the premises designates the conclusion.

Equations

• EgreRossiSprenger2026a.CEntails Γ B = ∀ (v : ι → Bool), (∀ A ∈ Γ, 0 ≤ EgreRossiSprenger2026a.cooperEval v A) → 0 ≤ EgreRossiSprenger2026a.cooperEval v B

@[instance_reducible]

instance EgreRossiSprenger2026a.instDecidableCEntailsOfFintypeOfDecidableEq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Γ : List (Trivalent.Formula ι)) (B : Trivalent.Formula ι) : Decidable (CEntails Γ B)

Equations

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

theorem EgreRossiSprenger2026a.cEntails_iff_forall_prob {ι : Type u_1} [MeasurableSpace (ι → Bool)] [DiscreteMeasurableSpace (ι → Bool)] {Γ : List (Trivalent.Formula ι)} {B : Trivalent.Formula ι} : CEntails Γ B ↔ ∀ (μ : MeasureTheory.Measure (ι → Bool)), MeasureTheory.IsProbabilityMeasure μ → (∀ A ∈ Γ, (Trivalent.prob μ fun (x : ι → Bool) => cooperEval x A) = 1) → (Trivalent.prob μ fun (x : ι → Bool) => cooperEval x B) = 1

Certain inference preserves probability 1 under every credence over the valuations, and conversely (Definition 4 and [ERS25]'s characterization).

Trivalent probability over a world space

@[reducible, inline]

abbrev EgreRossiSprenger2026a.value {ι : Type u_1} {W : Type u_2} (t : W → ι → Bool) (φ : Trivalent.Formula ι) : W → SignType

The trivalent proposition a formula expresses over a world space whose worlds t maps to classical valuations of the atoms.

Equations

• EgreRossiSprenger2026a.value t φ w = EgreRossiSprenger2026a.cooperEval (t w) φ

theorem EgreRossiSprenger2026a.prob_value_top {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} [MeasureTheory.IsProbabilityMeasure μ] (i : ι) : Trivalent.prob μ (value t (top i)) = 1

⊤ is certain, the first principle.

theorem EgreRossiSprenger2026a.prob_value_bot {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} [MeasureTheory.IsProbabilityMeasure μ] (i : ι) : Trivalent.prob μ (value t (bot i)) = 0

⊥ is impossible, the first principle.

theorem EgreRossiSprenger2026a.additivity_all_void {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (t : W → ι → Bool) (i : ι) : Trivalent.posExt (value t ((bot i).cond (top i))) = ∅ ∧ Trivalent.prob μ (value t (((bot i).cond (top i)).disj ((bot i).cond (top i)))) = 1 ∧ Trivalent.prob μ (value t ((bot i).cond (top i))) + Trivalent.prob μ (value t ((bot i).cond (top i))) = 2

The third principle (prob_value_disj below) fails without its properness clause, which the printed axiom omits: a certainly void disjunction of certainly void disjuncts has probability 1 by the All Void convention, while the disjuncts' probabilities sum to 2.

Conditional probability and Stalnaker's Thesis

theorem EgreRossiSprenger2026a.axiom2'_all_void {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (t : W → ι → Bool) (i : ι) : CEntails [] ((bot i).cond (top i)).neg ∧ CEntails [] (top i) ∧ Trivalent.prob μ (value t ((top i).cond ((bot i).cond (top i)))) = 1

Axiom 2′ fails as printed. C refutes ⊥ → ⊤ and makes ⊤ certain, yet the conditional probability of ⊥ → ⊤ given ⊤ is 1 by the All Void convention, not 0.

theorem EgreRossiSprenger2026a.prob_cond_congr_left {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} {A A' : Trivalent.Formula ι} (h₁ : CEntails [A] A') (h₂ : CEntails [A'] A) (C : Trivalent.Formula ι) : Trivalent.prob μ (value t (A.cond C)) = Trivalent.prob μ (value t (A'.cond C))

Antecedents equivalent in C give the same conditional probabilities (Left Logical Equivalence, axiom 4′), which is also Proposition 5 on updating.

theorem EgreRossiSprenger2026a.stalnaker_thesis {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} (A B C : Trivalent.Formula ι) : Trivalent.prob μ (value t (A.cond (B.cond C))) = Trivalent.prob μ (value t ((A.conj B).cond C))

The conditional probability of B → C given A is the conditional probability of C given A ∧ B (Stalnaker's Thesis, Theorem 3), for arbitrary formulas and with no hypotheses, since Import-Export is a pointwise identity.

theorem EgreRossiSprenger2026a.designated_cond_iff_material {ι : Type u_1} {A B : Trivalent.Formula ι} (hA : NoCond A) (hB : NoCond B) (v : ι → Bool) : 0 ≤ cooperEval v (A.cond B) ↔ 0 ≤ cooperEval v (material A B)

In antecedent position a simple indicative and its material conditional are designated together.

theorem EgreRossiSprenger2026a.prob_cond_material_eq {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} {A B : Trivalent.Formula ι} (hA : NoCond A) (hB : NoCond B) (H : Trivalent.Formula ι) : Trivalent.prob μ (value t ((A.cond B).cond H)) = Trivalent.prob μ (value t ((material A B).cond H))

Learning A → B is learning the material conditional A ⊃ B, for conditional-free A and B (Updating on Simple Conditionals, Proposition 6).

The model refuting the printed 5′: three atomic conditionals, pairwise constrained so that conditions (ii) and (iii) hold at every valuation, read at the single all-false world.

def EgreRossiSprenger2026a.AllVoid.A : Trivalent.Formula (Fin 4)

p → q.

Equations

• EgreRossiSprenger2026a.AllVoid.A = (Trivalent.Formula.atom 0).cond (Trivalent.Formula.atom 1)

def EgreRossiSprenger2026a.AllVoid.B : Trivalent.Formula (Fin 4)

p → ¬q, so that A ∧ B is never true and condition (ii) holds globally.

Equations

• EgreRossiSprenger2026a.AllVoid.B = (Trivalent.Formula.atom 0).cond (Trivalent.Formula.atom 1).neg

def EgreRossiSprenger2026a.AllVoid.C : Trivalent.Formula (Fin 4)

r → s, designated but void at the all-false world.

Equations

• EgreRossiSprenger2026a.AllVoid.C = (Trivalent.Formula.atom 2).cond (Trivalent.Formula.atom 3)

def EgreRossiSprenger2026a.AllVoid.assign : Unit → Fin 4 → Bool

The single world, carrying the all-false valuation.

Equations

• EgreRossiSprenger2026a.AllVoid.assign x✝¹ x✝ = false

theorem EgreRossiSprenger2026a.additivity_cond_all_void : CEntails [AllVoid.C] (AllVoid.A.conj AllVoid.B).neg ∧ ¬CEntails [AllVoid.C] (AllVoid.A.conj AllVoid.B) ∧ (∀ (v : Fin 4 → Bool), 0 ≤ cooperEval v AllVoid.C → (cooperEval v AllVoid.A = 0 ↔ cooperEval v AllVoid.B = 0)) ∧ (MeasureTheory.Measure.dirac ()) {w : Unit | 0 ≤ value AllVoid.assign AllVoid.C w} ≠ 0 ∧ Trivalent.prob (MeasureTheory.Measure.dirac ()) (value AllVoid.assign (AllVoid.C.cond (AllVoid.A.disj AllVoid.B))) = 1 ∧ Trivalent.prob (MeasureTheory.Measure.dirac ()) (value AllVoid.assign (AllVoid.C.cond AllVoid.A)) + Trivalent.prob (MeasureTheory.Measure.dirac ()) (value AllVoid.assign (AllVoid.C.cond AllVoid.B)) = 2

Axiom 5′ fails as printed. With the credence concentrated where both disjuncts are void, all three conditional probabilities are 1 by the All Void convention, although every printed hypothesis holds, the designated weight of C included.

The principles under a live defined region

The remaining principles divide credence by the weight of the defined region, so they read the measure of explicit sets and hold under the discrete σ-algebra of the paper's finite models.

theorem EgreRossiSprenger2026a.prob_value_neg {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] {φ : Trivalent.Formula ι} (h : μ (Function.support (value t φ)) ≠ 0) : Trivalent.prob μ (value t φ.neg) = 1 - Trivalent.prob μ (value t φ)

Negation complements probability unless the sentence is void almost surely, the second principle with its printed exception.

theorem EgreRossiSprenger2026a.prob_value_disj {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} [DiscreteMeasurableSpace W] {φ ψ : Trivalent.Formula ι} (hsupp : Function.support (value t φ) = Function.support (value t ψ)) (hdisj : Disjoint (Trivalent.posExt (value t φ)) (Trivalent.posExt (value t ψ))) (h : μ (Function.support (value t φ)) ≠ 0) : Trivalent.prob μ (value t (φ.disj ψ)) = Trivalent.prob μ (value t φ) + Trivalent.prob μ (value t ψ)

Disjuncts that are never true together and take classical values in the same worlds add, when the common defined region has positive credence (the third principle).

theorem EgreRossiSprenger2026a.prob_cond_eq_one_of_cEntails {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] {A B : Trivalent.Formula ι} (h : CEntails [A] B) : Trivalent.prob μ (value t (A.cond B)) = 1

A conditional certain in C has conditional probability 1 (axiom 3′), with no properness needed, since the All Void convention points the right way here.

theorem EgreRossiSprenger2026a.prob_cond_eq_zero_of_cEntails_neg {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} [DiscreteMeasurableSpace W] {A B : Trivalent.Formula ι} (h : CEntails [] B.neg) (hproper : μ (Function.support (value t (A.cond B))) ≠ 0) : Trivalent.prob μ (value t (A.cond B)) = 0

Where C refutes the consequent and the conditional is not void almost surely, the conditional probability is 0, which is axiom 2′ repaired with properness.

theorem EgreRossiSprenger2026a.prob_cond_disj {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {t : W → ι → Bool} [DiscreteMeasurableSpace W] {A B C : Trivalent.Formula ι} (hii : CEntails [C] (A.conj B).neg) (hiii : ∀ (v : ι → Bool), 0 ≤ cooperEval v C → (cooperEval v A = 0 ↔ cooperEval v B = 0)) (hproper : μ (Function.support (value t (C.cond A))) ≠ 0) : Trivalent.prob μ (value t (C.cond (A.disj B))) = Trivalent.prob μ (value t (C.cond A)) + Trivalent.prob μ (value t (C.cond B))

Trivalent Additivity (axiom 5′) holds under conditions (ii) and (iii) in their designated-value form together with a live defined region for C → A, the properness the printed version lacks.

Adams's conditionals are conditional events

[Ada75] gives if A then B the conditional probability of B given A and no truth conditions. On the trivalent semantics his formula denotes Cooper's simple conditional, the conditional event of its consequent on its antecedent, whose trivalent probability is his conditional probability; his proper assignments are those under which no formula is void almost surely; and his simple conditionals exhaust the trivalent propositions, the semantic content of the Reduction Theorem.

noncomputable def EgreRossiSprenger2026a.ofAdams {W : Type u_2} (φ : Adams1975.Formula W) : W → SignType

The trivalent proposition an [Ada75] formula denotes, Cooper's conditional of its consequent on its antecedent.

Equations

• EgreRossiSprenger2026a.ofAdams φ w = SignType.condAssert Trivalent.Designation.lp (SignType.ofProp (w ∈ φ.ante)) (SignType.ofProp (w ∈ φ.cons))

theorem EgreRossiSprenger2026a.ofAdams_eq_indicator {W : Type u_2} (φ : Adams1975.Formula W) : ofAdams φ = φ.ante.indicator fun (w : W) => SignType.ofProp (w ∈ φ.cons)

@[simp]

theorem EgreRossiSprenger2026a.support_ofAdams {W : Type u_2} (φ : Adams1975.Formula W) : Function.support (ofAdams φ) = φ.ante

theorem EgreRossiSprenger2026a.exists_ofAdams_eq {W : Type u_2} (p : W → SignType) : ∃ (φ : Adams1975.Formula W), ofAdams φ = p

Adams's simple conditionals exhaust the trivalent propositions, each being the conditional event of its truth on its definedness.

theorem EgreRossiSprenger2026a.ofAdams_eq_ofAdams_iff {W : Type u_2} {φ ψ : Adams1975.Formula W} : ofAdams φ = ofAdams ψ ↔ φ.ante = ψ.ante ∧ φ.ante ∩ φ.cons = ψ.ante ∩ ψ.cons

Two Adams formulas denote the same proposition exactly when they have the same antecedent and agree on it, de Finetti's identity of conditional events.

theorem EgreRossiSprenger2026a.value_cond_eq_ofAdams {ι : Type u_1} {W : Type u_2} {A B : Trivalent.Formula ι} (hA : NoCond A) (hB : NoCond B) (t : W → ι → Bool) : value t (A.cond B) = ofAdams { ante := {w : W | cooperEval (t w) A = 1}, cons := {w : W | cooperEval (t w) B = 1} }

A simple conditional of conditional-free formulas denotes the Adams formula of their truth sets.

theorem EgreRossiSprenger2026a.prob_ofAdams {W : Type u_2} [MeasurableSpace W] [DiscreteMeasurableSpace W] {μ : MeasureTheory.Measure W} {φ : Adams1975.Formula W} (h : μ φ.ante ≠ 0) : Trivalent.prob μ (ofAdams φ) = μ[φ.cons | φ.ante]

The trivalent probability of an Adams formula with a live antecedent is his conditional probability.

theorem EgreRossiSprenger2026a.adams_thesis {ι : Type u_1} {W : Type u_2} [MeasurableSpace W] [DiscreteMeasurableSpace W] {μ : MeasureTheory.Measure W} {A B : Trivalent.Formula ι} (hA : NoCond A) (hB : NoCond B) {t : W → ι → Bool} (h : μ {w : W | cooperEval (t w) A = 1} ≠ 0) : Trivalent.prob μ (value t (A.cond B)) = μ[{w : W | cooperEval (t w) B = 1} | {w : W | cooperEval (t w) A = 1}]

For conditional-free A and B with a live antecedent, the probability of A → B is the conditional probability of B given A (Adams's Thesis).

theorem EgreRossiSprenger2026a.pEntails_iff_prob {W : Type u_2} [MeasurableSpace W] [DiscreteMeasurableSpace W] {κ : Type u_3} {s : Finset κ} {X : κ → Adams1975.Formula W} {d : Adams1975.Formula W} : Adams1975.PEntails s X d ↔ ∀ ε > 0, ∃ δ > 0, ∀ (μ : MeasureTheory.Measure W), MeasureTheory.IsProbabilityMeasure μ → μ (Function.support (ofAdams d)) ≠ 0 → (∀ i ∈ s, μ (Function.support (ofAdams (X i))) ≠ 0) → (∀ i ∈ s, 1 - δ ≤ Trivalent.prob μ (ofAdams (X i))) → 1 - ε ≤ Trivalent.prob μ (ofAdams d)

[Ada75]'s p-entailment is a condition on trivalent probabilities, with his proper assignments the credences under which no premise or conclusion is void almost surely.

The die and coin models

The fair models the paper computes in: Goldstein and Santorio's die, Santorio and Wellwood's partition die, Edgington's coin, and the two-world model where p(X ∧ Y) ≤ p(X) fails.

def EgreRossiSprenger2026a.dieVal : Fin 6 → Fin 3 → Bool

Outcome n + 1 of a fair die as a valuation of the atoms even, two-or-four, six.

Equations

• EgreRossiSprenger2026a.dieVal = ![![false, false, false], ![true, true, false], ![false, false, false], ![true, true, false], ![false, false, false], ![true, false, true]]

theorem EgreRossiSprenger2026a.goldstein_santorio_die : Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) (value dieVal ((Trivalent.Formula.atom 0).cond ((Trivalent.Formula.atom 1).neg.cond (Trivalent.Formula.atom 2)))) = 1 ∧ Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) (value dieVal ((Trivalent.Formula.atom 1).neg.cond (Trivalent.Formula.atom 2))) = 1 / 4 ∧ Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) (value dieVal (Trivalent.Formula.atom 0)) = 1 / 2 ∧ Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) (value dieVal (((Trivalent.Formula.atom 1).neg.cond (Trivalent.Formula.atom 2)).conj (Trivalent.Formula.atom 0))) = 1 / 2

Goldstein and Santorio's die (§5). A is if the die landed even, then if it didn't land on two or four, it landed on six, B its inner conditional, C the die landed even. The semantics assigns the probabilities their argument demands, p(A) = 1, p(B) = 1/4 and p(C) = 1/2, and blocks their triviality step at p(B ∧ C) = 1/2 ≠ p(B): B ∧ C is a conjunction of a conditional with a factual sentence, and such conjunctions are not classical.

def EgreRossiSprenger2026a.dieVal' : Fin 6 → Fin 3 → Bool

Outcome n + 1 of a fair die as a valuation of the atoms even, two, one.

Equations

• EgreRossiSprenger2026a.dieVal' = ![![false, false, true], ![true, true, false], ![false, false, false], ![true, false, false], ![false, false, false], ![true, false, false]]

theorem EgreRossiSprenger2026a.santorio_wellwood_die : Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) (value dieVal' (((Trivalent.Formula.atom 0).cond (Trivalent.Formula.atom 1)).conj ((Trivalent.Formula.atom 0).neg.cond (Trivalent.Formula.atom 2)))) = 1 / 3

In Santorio and Wellwood's die (§4, example 3), if the outcome was even, it was two; and if it was odd, it was one is true exactly when the die landed 1 or 2, so it has probability 1/3, above what classical conjunction would allow.

def EgreRossiSprenger2026a.coinVal : Fin 4 → Fin 3 → Bool

The four equiprobable worlds of Edgington's coin (§6) as valuations of double-headed, flipped, heads.

Equations

• EgreRossiSprenger2026a.coinVal = ![![true, true, true], ![true, false, false], ![false, true, false], ![false, false, false]]

theorem EgreRossiSprenger2026a.edgington_coin : Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) (value coinVal (((Trivalent.Formula.atom 1).cond (Trivalent.Formula.atom 2)).cond (Trivalent.Formula.atom 0))) = 2 / 3

In Edgington's coin (§6), after learning if the coin was flipped, it landed heads, the probability that it is double-headed is p((F → H) → D) = 2/3, not the 1 Edgington's intuition demands, which the paper reads pragmatically.

def EgreRossiSprenger2026a.lawVal : Bool → Fin 2 → Bool

The two-world valuation behind the failure of p(X ∧ Y) ≤ p(X): the first atom tracks the world, the second is true everywhere.

Equations

• EgreRossiSprenger2026a.lawVal w i = if i = 0 then w else true

theorem EgreRossiSprenger2026a.prob_conj_gt : Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) (value lawVal ((Trivalent.Formula.atom 0).cond (bot 1))) = 0 ∧ Trivalent.prob (ProbabilityTheory.uniformOn Set.univ) (value lawVal (((Trivalent.Formula.atom 0).cond (bot 1)).conj (Trivalent.Formula.atom 1))) = 1 / 2

The standard law p(X ∧ Y) ≤ p(X) fails (§2, §4). The bet on A → ⊥ is lost or called off, while the bet on its conjunction with a truth is won at the world where it is called off.