Validity patterns for comparative probability

The intuitively valid (V1–V13) and invalid (I1–I3) inference patterns for comparative epistemic modals ([HI13], Figure 1; [Yal10]), stated for an abstract likelihood relation r on a Boolean algebra and proved once at the weakest axiom hypotheses. Models whose relations carry the ComparativeProbability.* mixins unconditionally (e.g. FinAddMeasure.inducedGe) discharge each pattern by instance resolution. The world-ordering lifts (Scales/EpistemicScale/Entailments.lean) instead validate most patterns for arbitrary world relations — strictly weaker hypotheses than the mixin route, which would demand reflexivity, transitivity, and (for the m-lift) finiteness — so their V2–V7 proofs are deliberately bespoke; they consume this layer exactly where its hypotheses are genuinely required (V11/V12).

I1–I3 are stated but not proved here: they are invalid for additive models (refuted by measure counterexamples) yet valid for the l-lifting, so their status is model-specific.

Main statements

• patternV1_holds — V1 holds for every relation (pure logic).
• patternV2, patternV3, patternV4, patternV5, patternV7 — from monotonicity (+ transitivity).
• patternV6 — additionally needs additivity and non-triviality.
• patternV11, patternV12 — from transitivity + complement reversal.
• patternV13 — from monotonicity + additivity.

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

V1: △a → ¬△aᶜ.

Equations

• ComparativeProbability.patternV1 r = ∀ (a : α), ComparativeProbability.Probably r a → ¬ComparativeProbability.Probably r aᶜ

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

V2: △(a ⊓ b) → △a ∧ △b.

Equations

• ComparativeProbability.patternV2 r = ∀ (a b : α), ComparativeProbability.Probably r (a ⊓ b) → ComparativeProbability.Probably r a ∧ ComparativeProbability.Probably r b

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

V3: △a → △(a ⊔ b).

Equations

• ComparativeProbability.patternV3 r = ∀ (a b : α), ComparativeProbability.Probably r a → ComparativeProbability.Probably r (a ⊔ b)

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

V4: a ≽ ⊥.

Equations

• ComparativeProbability.patternV4 r = ∀ (a : α), r a ⊥

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

V5: ⊤ ≽ a.

Equations

• ComparativeProbability.patternV5 r = ∀ (a : α), r ⊤ a

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

V6: □a → △a, where □a is ⊥ ≽ aᶜ.

Equations

• ComparativeProbability.patternV6 r = ∀ (a : α), r ⊥ aᶜ → ComparativeProbability.Probably r a

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

V7: △a → ◇a.

Equations

• ComparativeProbability.patternV7 r = ∀ (a : α), ComparativeProbability.Probably r a → ComparativeProbability.Possibly r a

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

V11: b ≽ a → △a → △b.

Equations

• ComparativeProbability.patternV11 r = ∀ (a b : α), r b a → ComparativeProbability.Probably r a → ComparativeProbability.Probably r b

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

V12: b ≽ a → a ≽ aᶜ → b ≽ bᶜ.

Equations

• ComparativeProbability.patternV12 r = ∀ (a b : α), r b a → r a aᶜ → r b bᶜ

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

V13: (a \ b) ≻ ⊥ → (a ⊔ b) ≻ b.

Equations

• ComparativeProbability.patternV13 r = ∀ (a b : α), ComparativeProbability.Strict r (a \ b) ⊥ → ComparativeProbability.Strict r (a ⊔ b) b

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

I1: a ≽ b → a ≽ c → a ≽ (b ⊔ c).

Equations

• ComparativeProbability.patternI1 r = ∀ (a b c : α), r a b → r a c → r a (b ⊔ c)

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

I2: a ≽ aᶜ → a ≽ b.

Equations

• ComparativeProbability.patternI2 r = ∀ (a b : α), r a aᶜ → r a b

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

I3: △a → a ≽ b.

Equations

• ComparativeProbability.patternI3 r = ∀ (a b : α), ComparativeProbability.Probably r a → r a b

theorem ComparativeProbability.patternV1_holds {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} : patternV1 r

V1 holds for any relation: it is pure logic about Strict and double complement, requiring no axioms.

theorem ComparativeProbability.patternV2_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsLikelihoodMono r] [IsTrans α r] : patternV2 r

V2 from monotonicity and transitivity.

theorem ComparativeProbability.patternV3_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsLikelihoodMono r] [IsTrans α r] : patternV3 r

V3 from monotonicity and transitivity.

theorem ComparativeProbability.patternV4_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsLikelihoodMono r] : patternV4 r

V4 from monotonicity.

theorem ComparativeProbability.patternV5_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsLikelihoodMono r] : patternV5 r

V5 from monotonicity.

theorem ComparativeProbability.patternV6_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsLikelihoodMono r] [IsTrans α r] [hq : IsQualitativeAdditive r] [IsNontrivial r] : patternV6 r

V6 from monotonicity, transitivity, additivity, and non-triviality.

theorem ComparativeProbability.patternV7_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsLikelihoodMono r] [IsTrans α r] : patternV7 r

V7 from monotonicity and transitivity.

theorem ComparativeProbability.patternV11_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsTrans α r] [IsComplementReversing r] : patternV11 r

V11 from transitivity and complement reversal.

theorem ComparativeProbability.patternV12_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsTrans α r] [IsComplementReversing r] : patternV12 r

V12 from transitivity and complement reversal.

theorem ComparativeProbability.patternV13_of {α : Type u_1} [BooleanAlgebra α] {r : α → α → Prop} [IsLikelihoodMono r] [IsQualitativeAdditive r] : patternV13 r

V13 from monotonicity and additivity.