Comparative probability

Comparative-likelihood orders ≿ on propositions (Set W) — "A is at least as likely as B" — after [HI13]: an axiom hierarchy, finitely- and qualitatively-additive measure semantics, the two world-ordering lifts, and the generalized finite cancellation theory of imprecise (multi-prior) comparative probability.

Main definitions

• RightUnion, DeterminedBySingletons — the two likelihood axioms with no mathlib/Defs analog (the rest are Reflexive and the Defs.lean mixins).
• EpistemicSystemW/F/FA — bundled axiom systems; EpistemicSystemFA is [HI13]'s logic FA.
• FinAddMeasure/QualAddMeasure — finitely- and qualitatively-additive probability measures over an ordered field, with their induced orders.
• dominationLift/matchingLift — the l- and m-liftings of a world preorder.
• GeneralizedFiniteCancellation and GFCOrder — the cancellation axiom and the GFC order of [HTHI16].

Main statements

• FinAddMeasure.toSystemFA, QualAddMeasure.toSystemFA — measures satisfy FA.
• FinAddMeasure.toGFCOrder — a measure induces a GFC order.
• GFCOrder.trans/mono/complRev — derived from cancellation, not stipulated.

Implementation notes

EpistemicSystemW/F are coarse staging toward EpistemicSystemFA, not [HI13]'s logics W/F (whose W-to-F step is totality); labels R/T are mnemonic for the paper's Mon and reflexivity.

The measures are generic over an ordered field K: ℝ gives the paper's literal [0,1]-valued measures, ℚ the computable theory. On a finite state space the two agree (rational and real linear feasibility coincide), and only ℚ supports the constructive Farkas (FourierMotzkin.lean) and decide-checked models (Representability.lean) behind the representation theorems. FinAddMeasure overlaps mathlib's MeasureTheory.AddContent and could be re-founded on it; FinAddMeasure.inducedGe is Order.Preimage m.mu (· ≥ ·).

References

[HI13], [Hal03], [vdH96], [KPS59], [HTHI16], [HTHI18]

Axioms

Two likelihood-relation axioms of [HI13] with no mathlib or Defs.lean analog. The remaining axioms are mathlib's Reflexive and the Defs.lean mixin classes IsLikelihoodMono (monotonicity, the paper's Mon), IsQualitativeAdditive, and IsNontrivial; the systems below carry those as plain propositional fields.

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

Right-union (axiom J of [HI13], Figure 4): A ≿ B → A ≿ C → A ≿ B ∪ C.

Equations

• ComparativeProbability.RightUnion ge = ∀ (A B C : Set W), ge A B → ge A C → ge A (B ∪ C)

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

Determination by singletons: A ≿ {b} → ∃ a ∈ A, {a} ≿ {b}.

Equations

• ComparativeProbability.DeterminedBySingletons ge = ∀ (A : Set W) (b : W), ge A {b} → ∃ a ∈ A, ge {a} {b}

Axiom systems

EpistemicSystemW/F are coarse staging toward EpistemicSystemFA. Fields hold the bare propositions; the matching Defs.lean mixin instances are below.

structure ComparativeProbability.EpistemicSystemW (W : Type u_1) : Type u_1

A reflexive, monotone likelihood relation (weaker than [HI13]'s logic W; see the module docstring).

• ge : Set W → Set W → Prop

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

• refl : Reflexive self.ge

  Reflexivity.

• mono (A B : Set W) : A ⊆ B → self.ge B A

  Monotonicity: supersets are at least as likely.

structure ComparativeProbability.EpistemicSystemF (W : Type u_1) extends ComparativeProbability.EpistemicSystemW W : Type u_1

Adds Ω ≿ ∅ and non-triviality.

• ge : Set W → Set W → Prop
• refl : Reflexive self.ge
• mono (A B : Set W) : A ⊆ B → self.ge B A
• bottom : self.ge Set.univ ∅

  The tautology is at least as likely as the contradiction.

• nonTrivial : ¬self.ge ∅ Set.univ

  Non-triviality: excludes the degenerate all-equivalent order.

structure ComparativeProbability.EpistemicSystemFA (W : Type u_1) extends ComparativeProbability.EpistemicSystemF W : Type u_1

[HI13]'s logic FA: a total, transitive, qualitatively additive likelihood order. Sound and complete for qualitatively additive measure semantics (Theorem 6; [vdH96]), and strictly weaker than finite additivity for |W| ≥ 5 (Theorem 8, after [KPS59]).

• ge : Set W → Set W → Prop
• refl : Reflexive self.ge
• mono (A B : Set W) : A ⊆ B → self.ge B A
• bottom : self.ge Set.univ ∅
• nonTrivial : ¬self.ge ∅ Set.univ
• total (A B : Set W) : self.ge A B ∨ self.ge B A

  Totality: any two propositions are comparable.

• trans (A B C : Set W) : self.ge A B → self.ge B C → self.ge A C

  Transitivity.

• additive (A B : Set W) : self.ge A B ↔ self.ge (A \ B) (B \ A)

  Qualitative additivity: A ≿ B ↔ (A \ B) ≿ (B \ A).

FA systems carry the comparative-probability mixins

An FA system's fields are defeq the Defs.lean mixin classes (a ≤ b is a ⊆ b on Set W), so the instances below register its relation as a comparative- probability order, and the validity patterns V1–V13 transfer from ComparativeProbability.Patterns by instance resolution.

instance ComparativeProbability.instIsLikelihoodMonoSetGe {W : Type u_1} (sys : EpistemicSystemFA W) : IsLikelihoodMono sys.ge

instance ComparativeProbability.instIsTransSetGe {W : Type u_1} (sys : EpistemicSystemFA W) : IsTrans (Set W) sys.ge

instance ComparativeProbability.instIsQualitativeAdditiveSetGe {W : Type u_1} (sys : EpistemicSystemFA W) : IsQualitativeAdditive sys.ge

instance ComparativeProbability.instIsNontrivialSetGe {W : Type u_1} (sys : EpistemicSystemFA W) : IsNontrivial sys.ge

Consequences of the FA axioms

theorem ComparativeProbability.ge_union_context {W : Type u_1} (sys : EpistemicSystemFA W) (X Y C : Set W) (hCX : Disjoint C X := by grind) (hCY : Disjoint C Y := by grind) : sys.ge X Y ↔ sys.ge (X ∪ C) (Y ∪ C)

Add common context: for C disjoint from both X and Y, X ≿ Y ↔ (X ∪ C) ≿ (Y ∪ C).

theorem ComparativeProbability.ge_add_context {W : Type u_1} (sys : EpistemicSystemFA W) {X Y C : Set W} (h : sys.ge X Y) (hCX : Disjoint C X := by grind) (hCY : Disjoint C Y := by grind) : sys.ge (X ∪ C) (Y ∪ C)

Forward form of ge_union_context: context C disjoint from both sides preserves ≿.

theorem ComparativeProbability.ge_generalized_merge {W : Type u_1} (sys : EpistemicSystemFA W) {X₁ Y₁ X₂ Y₂ : Set W} (h1 : sys.ge X₁ Y₁) (h2 : sys.ge X₂ Y₂) (hX : Disjoint X₁ X₂) (hY : Disjoint Y₁ Y₂) : sys.ge (X₁ ∪ X₂) (Y₁ ∪ Y₂)

Generalized merge: two valid comparisons with disjoint left parts and disjoint right parts merge into their union, even with pivot overlaps. Derivation: add context to each side, transit through X₂ ∪ Y₁, then restore the pivot X₂ ∩ Y₁ via Axiom A.

theorem ComparativeProbability.ge_mono_dominated {W : Type u_1} (sys : EpistemicSystemFA W) {X Y P Q : Set W} (h : sys.ge X Y) (hXP : X ⊆ P) (hQY : Q ⊆ Y) : sys.ge P Q

Mono-domination: a valid comparison X ≿ Y with X ⊆ P and Q ⊆ Y proves P ≿ Q.

theorem ComparativeProbability.ge_empty_target {W : Type u_1} (sys : EpistemicSystemFA W) (P : Set W) : sys.ge P ∅

P ≿ ∅ always (monotonicity).

Measure semantics

structure ComparativeProbability.FinAddMeasure (K : Type u_1) [Field K] [LinearOrder K] [IsStrictOrderedRing K] (W : Type u_2) : Type (max u_1 u_2)

A finitely additive probability measure on subsets of W, valued in an ordered field K. The value type is left generic: instantiate at ℚ for the constructive, decide-able representation theory and at ℝ for the paper's literal [0,1]-valued measures (see the module docstring).

• mu : Set W → K

  The measure function

• nonneg (A : Set W) : 0 ≤ self.mu A

  Non-negativity

• additive (A B : Set W) : Disjoint A B → self.mu (A ∪ B) = self.mu A + self.mu B

  Finite additivity: μ(A ∪ B) = μ(A) + μ(B) for disjoint A, B

• total : self.mu Set.univ = 1

  Normalization

def ComparativeProbability.FinAddMeasure.inducedGe {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) (A B : Set W) : Prop

Measure-induced comparative likelihood: A ≿ B ↔ μ(A) ≥ μ(B).

Equations

• m.inducedGe A B = (m.mu A ≥ m.mu B)

@[simp]

theorem ComparativeProbability.FinAddMeasure.mu_empty {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) : m.mu ∅ = 0

μ(∅) = 0 for any finitely additive measure. Follows from additivity: μ(∅ ∪ ∅) = μ(∅) + μ(∅), but ∅ ∪ ∅ = ∅.

theorem ComparativeProbability.FinAddMeasure.mu_mono {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) {A B : Set W} (h : A ⊆ B) : m.mu A ≤ m.mu B

Subset monotonicity: A ⊆ B → μ(A) ≤ μ(B).

theorem ComparativeProbability.FinAddMeasure.mu_compl {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) (A : Set W) : m.mu A + m.mu Aᶜ = 1

Complement measure: μ(A) + μ(Aᶜ) = 1.

theorem ComparativeProbability.FinAddMeasure.mu_qadd {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) (A B : Set W) : m.mu A ≥ m.mu B ↔ m.mu (A \ B) ≥ m.mu (B \ A)

Qualitative additivity for a finitely additive measure: splitting A and B into the shared part A ∩ B and the private parts cancels the shared part.

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

Every finitely additive measure satisfies the FA axioms. A fortiori from [HI13] Theorem 6 soundness, since every finitely additive measure is qualitatively additive.

Equations

• m.toSystemFA = { ge := m.inducedGe, refl := ⋯, mono := ⋯, bottom := ⋯, nonTrivial := ⋯, total := ⋯, trans := ⋯, additive := ⋯ }

Qualitatively additive measures

structure ComparativeProbability.QualAddMeasure (K : Type u_1) [Field K] [LinearOrder K] [IsStrictOrderedRing K] (W : Type u_2) : Type (max u_1 u_2)

A qualitatively additive measure on subsets of W. Unlike FinAddMeasure, this does NOT require μ(A ∪ B) = μ(A) + μ(B) for disjoint A, B. Instead it requires the weaker qualitative additivity condition: μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A).

[HI13] Theorem 6: System FA is sound and complete with respect to qualitatively additive measure models. The completeness construction (exists_qualAddMeasure_repr) realises μ(∅) = 0 by an affine renormalisation of the dominated-set count.

• mu : Set W → K

  The measure function

• nonneg (A : Set W) : 0 ≤ self.mu A

  Non-negativity

• mu_empty : self.mu ∅ = 0

  The impossible proposition has measure zero

• total : self.mu Set.univ = 1

  Normalization

• qualAdd (A B : Set W) : self.mu A ≥ self.mu B ↔ self.mu (A \ B) ≥ self.mu (B \ A)

  Qualitative additivity: μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A)

def ComparativeProbability.QualAddMeasure.inducedGe {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) (A B : Set W) : Prop

Measure-induced comparative likelihood: A ≿ B ↔ μ(A) ≥ μ(B).

Equations

• m.inducedGe A B = (m.mu A ≥ m.mu B)

theorem ComparativeProbability.QualAddMeasure.mu_mono {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) {A B : Set W} (h : A ⊆ B) : m.mu A ≤ m.mu B

Subset monotonicity: A ⊆ B → μ(A) ≤ μ(B). From qualAdd + μ(∅) = 0 + nonneg.

def ComparativeProbability.QualAddMeasure.toSystemFA {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : QualAddMeasure K W) : EpistemicSystemFA W

A qualitatively additive measure induces System FA. Soundness direction of [HI13] Theorem 6: every qualitatively additive measure model satisfies the FA axioms.

Equations

• m.toSystemFA = { ge := m.inducedGe, refl := ⋯, mono := ⋯, bottom := ⋯, nonTrivial := ⋯, total := ⋯, trans := ⋯, additive := ⋯ }

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

Every finitely additive measure is qualitatively additive. Proof: μ(A) = μ(A \ B) + μ(A ∩ B) and μ(B) = μ(B \ A) + μ(A ∩ B), so μ(A) ≥ μ(B) ↔ μ(A \ B) ≥ μ(B \ A).

Equations

• m.toQualAdd = { mu := m.mu, nonneg := ⋯, mu_empty := ⋯, total := ⋯, qualAdd := ⋯ }

World-ordering lifts

The l-lifting (Lewis's lifting; [HI13], §5) and its injection refinement, the m-lifting (§9). The l-lifting is the Smyth (upper powerdomain) order; the m-lifting requires distinct dominators (an injection), which avoids the disjunction problem (invalidates I1–I3) while validating V1–V13 (Fact 5).

def ComparativeProbability.dominationLift {W : Type u_1} (ge_w : W → W → Prop) (A B : Set W) : Prop

The l-lifting: A ≿ B iff every b ∈ B is dominated by some a ∈ A.

Equations

• ComparativeProbability.dominationLift ge_w A B = ∀ b ∈ B, ∃ a ∈ A, ge_w a b

def ComparativeProbability.matchingLift {W : Type u_1} (ge_w : W → W → Prop) (A B : Set W) : Prop

The m-lifting: A ≿ B iff some injection f : B ↪ A dominates pointwise.

Equations

• ComparativeProbability.matchingLift ge_w A B = ∃ (f : W → W), (∀ b ∈ B, f b ∈ A ∧ ge_w (f b) b) ∧ ∀ (b₁ b₂ : W), b₁ ∈ B → b₂ ∈ B → f b₁ = f b₂ → b₁ = b₂

theorem ComparativeProbability.dominationLift_axiomR {W : Type u_1} {ge_w : W → W → Prop} (hRefl : ∀ (w : W), ge_w w w) : Reflexive (dominationLift ge_w)

The l-lifting of a reflexive relation is reflexive.

theorem ComparativeProbability.dominationLift_axiomT {W : Type u_1} {ge_w : W → W → Prop} (hRefl : ∀ (w : W), ge_w w w) (A B : Set W) : A ⊆ B → dominationLift ge_w B A

The l-lifting of a reflexive relation is monotone.

theorem ComparativeProbability.dominationLift_axiomJ {W : Type u_1} {ge_w : W → W → Prop} : RightUnion (dominationLift ge_w)

The l-lifting satisfies right-union.

theorem ComparativeProbability.strict_dominationLift_iff {W : Type u_1} {ge_w : W → W → Prop} (hTotal : ∀ (a b : W), ge_w a b ∨ ge_w b a) (A B : Set W) : Strict (dominationLift ge_w) A B ↔ ∃ a ∈ A, ∀ b ∈ B, ge_w a b ∧ ¬ge_w b a

Over a total relation, the strict l-lifting collapses to Lewis's ∃∀ comparative possibility: some A-point strictly dominates every B-point. This is the form the metalinguistic comparative takes in [RK24] (there bounded to the cone below an evaluation index, with worlds read as semantic interpretations).

theorem ComparativeProbability.strict_dominationLift_iff_below {W : Type u_1} {ge_w below : W → W → Prop} (hTotal : ∀ (a b : W), ge_w a b ∨ ge_w b a) (hBelow : ∀ (a b : W), below a b ↔ ge_w b a ∧ ¬ge_w a b) (A B : Set W) : Strict (dominationLift ge_w) A B ↔ ∃ a ∈ A, ∀ b ∈ B, below b a

strict_dominationLift_iff with the strict pair packaged as a dominance relation: whenever below is the strict form of the total ge_w, strict l-lifting is an ∃∀ clause in below.

def ComparativeProbability.coneStrictLift {W : Type u_1} (le below : W → W → Prop) (P Q : W → Prop) (i : W) : Prop

Lewis's ∃∀ comparative-possibility clause, localized to the le-cone at an index and comparing difference sets (P∖Q against Q∖P, the shape of [Kra12]'s revised lifting), with the dominance relation a parameter — the single clause behind [RK24]'s ≻ (below the strict ordering) and ≫ (below = far-below).

Equations

• ComparativeProbability.coneStrictLift le below P Q i = ∃ (a : W), le a i ∧ P a ∧ ¬Q a ∧ ∀ (b : W), le b i → Q b → ¬P b → below b a

@[implicit_reducible]

instance ComparativeProbability.instDecidableConeStrictLiftOfFintypeOfDecidableRelOfDecidablePred {W : Type u_1} (le below : W → W → Prop) (P Q : W → Prop) (i : W) [Fintype W] [DecidableRel le] [DecidableRel below] [DecidablePred P] [DecidablePred Q] : Decidable (coneStrictLift le below P Q i)

Equations

• ComparativeProbability.instDecidableConeStrictLiftOfFintypeOfDecidableRelOfDecidablePred le below P Q i = id inferInstance

theorem ComparativeProbability.coneStrictLift_iff_strict_dominationLift {W : Type u_1} {ge_w le below : W → W → Prop} (hTotal : ∀ (a b : W), ge_w a b ∨ ge_w b a) (hBelow : ∀ (a b : W), below a b ↔ ge_w b a ∧ ¬ge_w a b) (P Q : W → Prop) (i : W) : coneStrictLift le below P Q i ↔ Strict (dominationLift ge_w) {x : W | le x i ∧ P x ∧ ¬Q x} {x : W | le x i ∧ Q x ∧ ¬P x}

Whenever below is the strict form of the total ge_w, the cone-localized clause is the strict l-lifting on the cone difference sets.

theorem ComparativeProbability.dominationLift_axiomDS {W : Type u_1} {ge_w : W → W → Prop} : DeterminedBySingletons (dominationLift ge_w)

The l-lifting satisfies determination by singletons.

theorem ComparativeProbability.matchingLift_axiomR {W : Type u_1} {ge_w : W → W → Prop} (hRefl : ∀ (w : W), ge_w w w) : Reflexive (matchingLift ge_w)

The m-lifting of a reflexive relation is reflexive.

theorem ComparativeProbability.matchingLift_axiomT {W : Type u_1} {ge_w : W → W → Prop} (hRefl : ∀ (w : W), ge_w w w) (A B : Set W) : A ⊆ B → matchingLift ge_w B A

The m-lifting of a reflexive relation is monotone.

def ComparativeProbability.dominationLiftSystemW {W : Type u_1} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : EpistemicSystemW W

The l-lifting of a reflexive preorder yields a System W (soundness).

Equations

• ComparativeProbability.dominationLiftSystemW ge_w hRefl = { ge := ComparativeProbability.dominationLift ge_w, refl := ⋯, mono := ⋯ }

def ComparativeProbability.matchingLiftSystemW {W : Type u_1} (ge_w : W → W → Prop) (hRefl : ∀ (w : W), ge_w w w) : EpistemicSystemW W

The m-lifting of a reflexive preorder yields a System W.

Equations

• ComparativeProbability.matchingLiftSystemW ge_w hRefl = { ge := ComparativeProbability.matchingLift ge_w, refl := ⋯, mono := ⋯ }

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_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) : IsLikelihoodMono m.inducedGe

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

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

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

Generalized finite cancellation and GFC orders

The cancellation theory of imprecise (multi-prior) comparative probability, following [HTHI16] (after Ríos Insua 1992 and Alon–Lehrer 2014) and used by [HTHI18]. A pair of event-sequences is balanced when every state lies in equally many events on each side; Finite Cancellation (Scott) and its Generalized strengthening are the cancellation axioms whose Refl + Positivity + Non-triviality companions characterize representability by a single, resp. a set of, additive measures.

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.Balanced {W : Type u_1} (Es Fs : List (Set W)) : Prop

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

Equations

• ComparativeProbability.Balanced 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 (Scott's axiom; [HTHI16]): 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 (Ríos Insua; Alon–Lehrer; the form of [HTHI16]): like FiniteCancellation, but the distinguished pair may be repeated r ≥ 1 times. Strictly stronger than FiniteCancellation for incomplete relations; equivalent under totality.

Equations

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

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

GFC implies FC (the r = 1 instance).

structure ComparativeProbability.GFCOrder (W : Type u_1) : Type u_1

A GFC order ([HTHI18], after [HTHI16]): reflexivity, positivity, non-triviality, and generalized finite cancellation. These four axioms characterize representability by a nonempty set of additive measures (E ≿ F ↔ ∀ μ ∈ P, μ E ≥ μ F). Transitivity, monotonicity, and complement reversal are derived from cancellation (GFCOrder.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.GFCOrder.fc {W : Type u_1} (G : GFCOrder W) : FiniteCancellation G.ge

A GFC order satisfies finite cancellation.

theorem ComparativeProbability.GFCOrder.trans {W : Type u_1} (G : GFCOrder 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.GFCOrder.mono {W : Type u_1} (G : GFCOrder 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.GFCOrder.complRev {W : Type u_1} (G : GFCOrder 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

theorem ComparativeProbability.FinAddMeasure.muFinsetSum {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {W : Type u_2} (m : FinAddMeasure K W) (S : Finset W) : m.mu ↑S = ∑ i ∈ S, m.mu {i}

The measure of a finite set is the sum of its singleton measures.

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

Every finitely additive measure's induced order is a GFC order: the Scott / Alon–Lehrer soundness direction (a single measure μ is the nonempty set {μ}).

Equations

• m.toGFCOrder = { ge := m.inducedGe, refl := ⋯, positivity := ⋯, nonTriviality := ⋯, gfc := ⋯ }