Cancellation conditions

Scott's cancellation vocabulary for comparative probability, in the balanced-sequence form of [Sco64] and [HTHI16]: a pair of event-sequences is balanced when every state lies in equally many events on each side; finite cancellation (representability by a single additive measure, [Sco64] reformulating [KPS59]) and its generalized strengthening (representability by a nonempty set of measures, [RI92]; [AL14]).

Scott.lean proves Scott's theorem through an equivalent weighted-portfolio device; the bridge from that device to the balanced-sequence statement is TODO. What is here: the definitions, the derived properties of a cancellation order, and the soundness directions — measures induce cancellation orders, and representable qualitative probability orders satisfy finite cancellation.

Main definitions

• BalancedSeqs, FiniteCancellation, GeneralizedFiniteCancellation.
• CancellationOrder — reflexivity, positivity, non-triviality, and generalized finite cancellation, bundled; totality not assumed.

Main statements

• FiniteCancellation.of_generalized; CancellationOrder.trans/mono/complRev.
• CancellationOrder.ofMeasure, Representable.finiteCancellation.

References

[Sco64], [KPS59], [RI92], [AL14], [HTHI16]

noncomputable def ComparativeProbability.seqCount {W : Type u_1} (s : W) (Es : List (Set W)) : ℕ

Indicator count of a state across an event sequence.

Equations

• ComparativeProbability.seqCount s Es = (List.map (fun (E : Set W) => if s ∈ E then 1 else 0) Es).sum

def ComparativeProbability.BalancedSeqs {W : Type u_1} (Es Fs : List (Set W)) : Prop

A balanced pair of event-sequences: every state lies in equally many events on the left as on the right.

Equations

• ComparativeProbability.BalancedSeqs Es Fs = ∀ (s : W), ComparativeProbability.seqCount s Es = ComparativeProbability.seqCount s Fs

def ComparativeProbability.FiniteCancellation {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Finite Cancellation ([Sco64]'s axiom, reformulating [KPS59]): for every balanced pair ⟨…, X⟩ / ⟨…, Y⟩ whose premise comparisons all hold, Y ≿ X. (prem carries the paired premise events; X/Y are the heads.)

Equations

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

def ComparativeProbability.GeneralizedFiniteCancellation {W : Type u_1} (ge : Set W → Set W → Prop) : Prop

Generalized Finite Cancellation ([RI92]; [AL14]): like FiniteCancellation, but the distinguished pair may be repeated r ≥ 1 times. Strictly stronger than FiniteCancellation for incomplete relations ([HTHI16]); equivalent under totality.

Equations

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

theorem ComparativeProbability.FiniteCancellation.of_generalized {W : Type u_1} {ge : Set W → Set W → Prop} (h : GeneralizedFiniteCancellation ge) : FiniteCancellation ge

GFC implies FC (the r = 1 instance).

structure ComparativeProbability.CancellationOrder (W : Type u_2) : Type u_2

A cancellation order: reflexivity, positivity, non-triviality, and generalized finite cancellation — the comparative probability orders of [RI92] and [AL14], which on a finite state space are exactly those represented by a nonempty set of additive probability measures (E ≿ F ↔ ∀ μ ∈ P, μ E ≥ μ F). Totality is not assumed. Transitivity, monotonicity, and complement reversal are derived from cancellation (CancellationOrder.trans/mono/complRev), not stipulated.

• ge : Set W → Set W → Prop

  The "at least as likely as" relation on propositions.

• refl (A : Set W) : self.ge A A

  Reflexivity.

• positivity (A : Set W) : self.ge A ∅

  Positivity: every proposition is at least as likely as the contradiction.

• nonTriviality : ¬self.ge ∅ Set.univ

  Non-triviality: the contradiction is not at least as likely as the tautology.

• gfc : GeneralizedFiniteCancellation self.ge

  Generalized finite cancellation.

theorem ComparativeProbability.CancellationOrder.fc {W : Type u_1} (G : CancellationOrder W) : FiniteCancellation G.ge

A GFC order satisfies finite cancellation.

theorem ComparativeProbability.CancellationOrder.trans {W : Type u_1} (G : CancellationOrder W) {A B C : Set W} (hAB : G.ge A B) (hBC : G.ge B C) : G.ge A C

Transitivity is derived from cancellation (balanced sequence ⟨A,B,C⟩/⟨B,C,A⟩).

theorem ComparativeProbability.CancellationOrder.mono {W : Type u_1} (G : CancellationOrder W) {A B : Set W} (hAB : A ⊆ B) : G.ge B A

Monotonicity is derived from positivity + cancellation (balanced sequence ⟨B∖A, A⟩/⟨∅, B⟩).

theorem ComparativeProbability.CancellationOrder.complRev {W : Type u_1} (G : CancellationOrder W) {A B : Set W} (hAB : G.ge A B) : G.ge Bᶜ Aᶜ

Complement reversal is derived from cancellation (balanced sequence ⟨A, Aᶜ⟩/⟨B, Bᶜ⟩).

Measures induce GFC orders

def ComparativeProbability.CancellationOrder.ofMeasure {W : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Fintype W] (m : FinAddMeasure K W) : CancellationOrder W

Every finitely additive measure's induced order is a cancellation order — the soundness direction of the representation (a single measure μ is the nonempty set {μ}).

Equations

• ComparativeProbability.CancellationOrder.ofMeasure m = { ge := m.inducedGe, refl := ⋯, positivity := ⋯, nonTriviality := ⋯, gfc := ⋯ }

theorem ComparativeProbability.Representable.finiteCancellation {W : Type u_1} [Fintype W] {sys : QualitativeProbability (Set W)} (h : Representable sys) : FiniteCancellation sys.ge

A representable qualitative probability order satisfies finite cancellation (the soundness half of Scott's theorem, in balanced-sequence form).