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 [HI13]. 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).

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)

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.