Trivalent probability

A trivalent proposition is true, false or void at each world, and a bet on it is won, lost or called off. Its probability is the weight of its truth relative to that of its truth and falsity together: the conditional probability that it is true given that it is not void, and 1 by convention when it is void almost surely ([ERS26b]). On a two-valued proposition it is the probability that the proposition is true, and on a conditional assertion of a two-valued consequent it is the conditional probability of the consequent given the condition, which is Adams's Thesis.

Main definitions

• Trivalent.prob: the probability of a trivalent proposition.

Main statements

• Trivalent.prob_eq_div: the weight of truth over that of truth and falsity.
• Trivalent.prob_eq_one_iff, Trivalent.prob_eq_zero_iff: probability 1 is almost sure non-falsity, and probability 0 is almost sure non-truth where falsity has positive weight.
• Trivalent.prob_ofProp, Trivalent.prob_indicator_ofProp: ordinary probability on two-valued propositions, and Adams's Thesis on conditional assertions.
• Trivalent.prob_neg: negation complements the probability unless the proposition is void almost surely.
• Trivalent.prob_joinBelnap: additivity for disjuncts that are defined together and never true together.
• Trivalent.prob_smul, Trivalent.prob_uniformOn_univ, Trivalent.prob_count_eq: only relative weights matter, so the uniform credence counts worlds.

Implementation notes

The credence is any measure on a discrete measurable space, as the finite world spaces of the literature are, and probabilities are ℝ≥0∞-valued.

References

• [ERS26b]

noncomputable def Trivalent.prob {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (p : W → SignType) : ENNReal

The probability of a trivalent proposition is the conditional probability that it is true given that it is not void, and 1 when it is void almost surely.

Equations

• Trivalent.prob μ p = if μ (Function.support p) = 0 then 1 else μ[Trivalent.posExt p | Function.support p]

theorem Trivalent.prob_of_measure_support_eq_zero {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} (h : μ (Function.support p) = 0) : prob μ p = 1

theorem Trivalent.prob_of_measure_support_ne_zero {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} (h : μ (Function.support p) ≠ 0) : prob μ p = μ[posExt p | Function.support p]

theorem Trivalent.prob_le_one {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} [MeasureTheory.IsFiniteMeasure μ] : prob μ p ≤ 1

theorem Trivalent.prob_smul {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} {c : ENNReal} (hc0 : c ≠ 0) (hc : c ≠ ⊤) : prob (c • μ) p = prob μ p

Trivalent probability reads only the relative weights, so it is invariant under rescaling the credence.

theorem Trivalent.prob_uniformOn_univ {W : Type u_1} [MeasurableSpace W] [Fintype W] [Nonempty W] (p : W → SignType) : prob (ProbabilityTheory.uniformOn Set.univ) p = prob MeasureTheory.Measure.count p

Against the uniform credence on a finite world space, trivalent probability counts worlds.

@[simp]

theorem Trivalent.prob_ofProp {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} [MeasureTheory.IsProbabilityMeasure μ] (A : W → Prop) [DecidablePred A] : (prob μ fun (w : W) => SignType.ofProp (A w)) = μ {w : W | A w}

On a two-valued proposition, trivalent probability is the probability of truth.

theorem Trivalent.prob_eq_div {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} [DiscreteMeasurableSpace W] (h : μ (Function.support p) ≠ 0) : prob μ p = μ (posExt p) / (μ (posExt p) + μ (negExt p))

Where a proposition is not void almost surely, its probability is the weight of its truth over that of its truth and falsity together.

theorem Trivalent.prob_eq_div_measure_support {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} [DiscreteMeasurableSpace W] (h : μ (Function.support p) ≠ 0) : prob μ p = μ (posExt p) / μ (Function.support p)

The weight of truth and falsity together is the weight of the defined region.

theorem Trivalent.prob_count_eq {W : Type u_1} [MeasurableSpace W] {p : W → SignType} [DiscreteMeasurableSpace W] {P S : Finset W} (hpos : ∀ (w : W), p w = 1 ↔ w ∈ P) (hsupp : ∀ (w : W), p w ≠ 0 ↔ w ∈ S) (hS : S.Nonempty) : prob MeasureTheory.Measure.count p = ↑P.card / ↑S.card

Against the counting credence, trivalent probability is a ratio of world counts.

theorem Trivalent.prob_joinBelnap {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} [DiscreteMeasurableSpace W] {q : W → SignType} (hsupp : Function.support p = Function.support q) (hdisj : Disjoint (posExt p) (posExt q)) (h : μ (Function.support p) ≠ 0) : (prob μ fun (w : W) => (p w).joinBelnap (q w)) = prob μ p + prob μ q

Trivalent additivity. Disjoining propositions that are defined together and never true together adds their probabilities, the additivity of [ERS26b]'s trivalent probability; without the properness hypothesis all three probabilities can be 1 by the all-void convention.

theorem Trivalent.prob_eq_one_iff {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] : prob μ p = 1 ↔ μ (negExt p) = 0

Probability 1 is almost sure non-falsity.

@[simp]

theorem Trivalent.prob_dirac_eq_one_iff {W : Type u_1} [MeasurableSpace W] {p : W → SignType} [DiscreteMeasurableSpace W] {w : W} : prob (MeasureTheory.Measure.dirac w) p = 1 ↔ 0 ≤ p w

Against a point mass, a proposition has probability 1 exactly where it is not false.

theorem Trivalent.prob_eq_zero_iff {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] : prob μ p = 0 ↔ μ (posExt p) = 0 ∧ μ (negExt p) ≠ 0

Probability 0 is almost sure non-truth where falsity has positive weight.

theorem Trivalent.prob_indicator_ofProp {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} [DiscreteMeasurableSpace W] (s : Set W) (B : W → Prop) [DecidablePred B] (h : μ s ≠ 0) : prob μ (s.indicator fun (w : W) => SignType.ofProp (B w)) = μ[{w : W | B w} | s]

Adams's Thesis. A conditional assertion of a two-valued consequent on the condition s has the conditional probability of the consequent given s.

theorem Trivalent.prob_neg {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {p : W → SignType} [DiscreteMeasurableSpace W] [MeasureTheory.IsFiniteMeasure μ] (h : μ (Function.support p) ≠ 0) : prob μ (-p) = 1 - prob μ p

Negation complements the probability, unless the proposition is void almost surely, when both probabilities are 1.