Docs / Logic / ComparativeProbability / Defs

Qualitative probability

import Linglib.Logic.ComparativeProbability.Defs · namespace ComparativeProbability

Source

Comparative probability reads a relation r a b on a Boolean algebra α as "a is at least as likely as b". This file states the axioms of the subject as unbundled mixin classes on such a relation, in the style of IsTrans, and collects de Finetti's system, the standard base of comparative probability that Kraft, Pratt and Seidenberg and Scott build on, as the class IsQualitativeProbability: ⊥ is not at least as likely as ⊤, every event is at least as likely as ⊥, and the relation is total, transitive and qualitatively additive (a ≿ b ↔ a \ b ≿ b \ a). Monotonicity follows from these axioms.

A likelihood order also defines probably: △a holds when a is strictly more likely than its complement, as in the logics of comparative probability that Holliday and Icard compare. Over a monotone order the contradiction is never probable and, when the order is non-trivial, the tautology always is; over a monotone transitive order probably is upward closed. RightUnion is Halpern's union property J, and DeterminedBySingletons his property that comparisons with a single world reduce to comparisons of single worlds.

Main definitions

Main statements

References

The axioms as mixins

A relation is qualitatively additive when a ≽ b holds exactly when a \ b ≽ b \ a. This is de Finetti's additivity axiom with the common part a ⊓ b cancelled from both sides; isQualitativeAdditive_iff recovers the axiom as printed.

class IsQualitativeAdditiveL63–67
{α : Type u_1} [BooleanAlgebra α] (r : α → α → Prop) :
Prop
  • qadd (a b : α) : r a b ↔ r (a \ b) (b \ a)

Used by instComplementReversingOfQualitativeAdditive, IsQualitativeProbability

Used in Logic/ComparativeProbability/Basic, Logic/ComparativeProbability/Patterns, Logic/ComparativeProbability/Representability, Logic/ComparativeProbability/WorldOrdering, Icard2016

Qualitative probabilities

A qualitative probability on a Boolean algebra α is a relation r, read "a is at least as likely as b", satisfying de Finetti's axioms as Scott 1964 lists them (p. 246): ⊥ is not at least as likely as ⊤, every event is at least as likely as ⊥, any two events compare, r is transitive, and r is qualitatively additive, which is axiom (v) with the common part of the two sides cancelled (isQualitativeAdditive_iff). Every qualitative probability on a finite carrier is represented by a qualitatively additive measure (exists_qualAddMeasure_repr), but by a probability measure only below five atoms (Completeness.lean).

class IsQualitativeProbabilityL87–98
{α : Type u_1} [BooleanAlgebra α] (r : α → α → Prop) extends IsNontrivial r, Std.Total r, IsTrans α r, IsQualitativeAdditive r :
Prop
  • bot_not_ge_top : ¬r ⊥ ⊤
  • total (a b : α) : r a b ∨ r b a
  • trans (a b c : α) : r a b → r b c → r a c
  • qadd (a b : α) : r a b ↔ r (a \ b) (b \ a)
  • rel_bot' (a : α) : r a ⊥

    Every event is at least as likely as ⊥. Use the lemma rel_bot.

Built from ,

Used by IsQualitativeProbability.isLikelihoodMono, IsQualitativeProbability.isPreorder

Used in Logic/ComparativeProbability/Basic, Logic/ComparativeProbability/Cancellation, Logic/ComparativeProbability/CancellationFin4, Logic/ComparativeProbability/Completeness, Logic/ComparativeProbability/Content and 4 more

L107–108

Probably

L129