Comparative probability orders on a Boolean algebra

This file develops the abstract theory of comparative (qualitative) probability: a relation r a b read "a is at least as likely as b" on a Boolean algebra α, following [holliday-icard-2013]. The axioms of the paper's logics are stated as unbundled mixin Prop-classes on the relation, so the validity patterns (ComparativeProbability.Patterns) can be proved once at the weakest hypotheses and reused by every concrete model — finitely-additive measures, qualitatively- additive measures, world-ordering lifts — through instances.

Transitivity reuses mathlib's IsTrans; only the genuinely Boolean-algebra-flavored axioms (monotonicity, complement reversal, qualitative additivity, non-triviality) get bespoke classes.

Main definitions

• ComparativeProbability.Strict, Probably, Possibly — the derived operators a ≻ b, △a, ◇a.
• IsLikelihoodMono, IsComplementReversing, IsQualitativeAdditive, IsNontrivial — the axiom mixin classes.

Main statements

• instComplementReversingOfQualitativeAdditive — qualitative additivity implies complement reversal, via bᶜ \ aᶜ = a \ b (compl_sdiff_compl).
• The instances registering a QualitativeProbability's ge (and a measure's inducedGe) as carriers of the mixins: QualitativeProbability on Set W is [holliday-icard-2013]'s logic FA, sound and complete for qualitatively additive measure semantics (Theorem 6; [van-der-hoek-1996]) and strictly weaker than finite additivity for |W| ≥ 5 (Theorem 8, after [kraft-pratt-seidenberg-1959]).

def ComparativeProbability.Strict {α : Type u_1} (r : α → α → Prop) (a b : α) : Prop

Strict r a b ("a ≻ b"): a is at least as likely as b but not conversely.

Equations

• ComparativeProbability.Strict r a b = (r a b ∧ ¬r b a)

@[instance_reducible]

instance ComparativeProbability.instDecidableRelStrict {α : Type u_1} {r : α → α → Prop} [DecidableRel r] : DecidableRel (Strict r)

Equations

• ComparativeProbability.instDecidableRelStrict x✝¹ x✝ = ComparativeProbability.instDecidableRelStrict._aux_1 x✝¹ x✝

def ComparativeProbability.Probably {α : Type u_1} [BooleanAlgebra α] (r : α → α → Prop) (a : α) : Prop

Probably r a ("△a"): a is strictly more likely than its complement.

Equations

• ComparativeProbability.Probably r a = ComparativeProbability.Strict r a aᶜ

def ComparativeProbability.Possibly {α : Type u_1} [BooleanAlgebra α] (r : α → α → Prop) (a : α) : Prop

Possibly r a ("◇a"): a is not certainly impossible (¬ ⊥ ≽ a).

Equations

• ComparativeProbability.Possibly r a = ¬r ⊥ a

class ComparativeProbability.IsLikelihoodMono {α : Type u_1} [BooleanAlgebra α] (r : α → α → Prop) : Prop

Axiom T (monotonicity): larger events are at least as likely.

• mono (a b : α) : a ≤ b → r b a

class ComparativeProbability.IsComplementReversing {α : Type u_1} [BooleanAlgebra α] (r : α → α → Prop) : Prop

Axiom C (complement reversal): a ≽ b → bᶜ ≽ aᶜ.

• complRev (a b : α) : r a b → r bᶜ aᶜ

class ComparativeProbability.IsQualitativeAdditive {α : Type u_1} [BooleanAlgebra α] (r : α → α → Prop) : Prop

Axiom A (qualitative additivity): a ≽ b ↔ (a \ b) ≽ (b \ a).

• qadd (a b : α) : r a b ↔ r (a \ b) (b \ a)

class ComparativeProbability.IsNontrivial {α : Type u_1} [BooleanAlgebra α] (r : α → α → Prop) : Prop

Axiom BT (non-triviality): ⊥ is not at least as likely as ⊤.

• bot_not_ge_top : ¬r ⊥ ⊤

@[instance 100]

instance ComparativeProbability.instComplementReversingOfQualitativeAdditive {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [h : IsQualitativeAdditive r] : IsComplementReversing r

Qualitative additivity implies complement reversal: bᶜ \ aᶜ = a \ b and aᶜ \ bᶜ = b \ a turn the additivity equivalence for bᶜ, aᶜ into the one for a, b.

Qualitative probability orders carry the mixins

QualitativeProbability.ge is defeq the mixin classes' relation, so the instances below register it as a comparative-probability order, and the validity patterns V1–V13 (Patterns.lean) transfer by instance resolution.

instance ComparativeProbability.instIsLikelihoodMonoGe {α : Type u_2} [BooleanAlgebra α] (sys : QualitativeProbability α) : IsLikelihoodMono sys.ge

instance ComparativeProbability.instIsTransGe {α : Type u_2} [BooleanAlgebra α] (sys : QualitativeProbability α) : IsTrans α sys.ge

instance ComparativeProbability.instIsQualitativeAdditiveGe {α : Type u_2} [BooleanAlgebra α] (sys : QualitativeProbability α) : IsQualitativeAdditive sys.ge

instance ComparativeProbability.instIsNontrivialGe {α : Type u_2} [BooleanAlgebra α] (sys : QualitativeProbability α) : IsNontrivial sys.ge

Connection to the ComparativeProbability theory

Every finitely-additive measure's induced order is a comparative-probability order (monotone, transitive, qualitatively additive, non-trivial), so the validity patterns V1–V13 transfer for free from ComparativeProbability.Patterns by instance resolution — no per-measure arithmetic.

instance ComparativeProbability.instIsLikelihoodMonoSetInducedGe {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_3} (m : FinAddMeasure K W) : IsLikelihoodMono m.inducedGe

instance ComparativeProbability.instIsTransSetInducedGe {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_3} (m : FinAddMeasure K W) : IsTrans (Set W) m.inducedGe

instance ComparativeProbability.instIsQualitativeAdditiveSetInducedGe {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_3} (m : FinAddMeasure K W) : IsQualitativeAdditive m.inducedGe

instance ComparativeProbability.instIsNontrivialSetInducedGe {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_3} (m : FinAddMeasure K W) : IsNontrivial m.inducedGe

Likewise for qualitatively additive measures, whose induced order is the ge of QualAddMeasure.toQualitativeProbability.

instance ComparativeProbability.instIsLikelihoodMonoSetInducedGe_1 {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_3} (m : QualAddMeasure K W) : IsLikelihoodMono m.inducedGe

instance ComparativeProbability.instIsTransSetInducedGe_1 {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_3} (m : QualAddMeasure K W) : IsTrans (Set W) m.inducedGe

instance ComparativeProbability.instIsQualitativeAdditiveSetInducedGe_1 {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_3} (m : QualAddMeasure K W) : IsQualitativeAdditive m.inducedGe

instance ComparativeProbability.instIsNontrivialSetInducedGe_1 {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_3} (m : QualAddMeasure K W) : IsNontrivial m.inducedGe