The Kraft–Pratt–Seidenberg five-atom counterexample

This file formalizes the simple ordering displayed in Section 4 of Kraft–Pratt–Seidenberg, Intuitive Probability on Finite Sets (1959). The five atoms p q r s t are represented by 0 1 2 3 4 : Fin 5.

The rank table below is the paper's displayed order, from the empty event through the full event. Its four decisive comparisons are

qs < p, pq < rs, ps < tq, and rt < spq.

The finite de Finetti properties are checked by evaluating all events. The non-representability argument itself is symbolic: finite additivity turns the four strict event comparisons into four incompatible linear inequalities between singleton weights.

@[reducible, inline]

abbrev Scott1964.MeasurementStructures.Probability.KPSCounterexample.Atom : Type

The five outcomes in the Kraft--Pratt--Seidenberg example.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.Atom = Fin 5

@[reducible, inline]

abbrev Scott1964.MeasurementStructures.Probability.KPSCounterexample.Event : Type

Events are subsets of the five outcomes.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.Event = Finset Scott1964.MeasurementStructures.Probability.KPSCounterexample.Atom

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.p : Atom

Outcome p in the notation of the original rank table.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.p = 0

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.q : Atom

Outcome q in the notation of the original rank table.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.q = 1

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.r : Atom

Outcome r in the notation of the original rank table.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.r = 2

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.s : Atom

Outcome s in the notation of the original rank table.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.s = 3

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.t : Atom

Outcome t in the notation of the original rank table.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.t = 4

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.eventCode (A : Event) : ℕ

Binary code for an event, with p q r s t as bits 0 1 2 3 4.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.eventCode A = ∑ i ∈ A, 2 ^ ↑i

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.kpsRank (A : Event) : ℕ

Position in the strict 32-event order printed by KPS.

Equations

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

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.KPSLe (A B : Event) : Prop

The weak comparison induced by the original 32-event rank table.

Equations

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

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.KPSLt (A B : Event) : Prop

The strict comparison induced by the original 32-event rank table.

Equations

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

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.KPSGe (A B : Event) : Prop

The KPS order oriented as “at least as probable”, matching the shared qualitative-probability API.

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.KPSGe A B = Scott1964.MeasurementStructures.Probability.KPSCounterexample.KPSLe B A

@[instance_reducible]

instance Scott1964.MeasurementStructures.Probability.KPSCounterexample.instDecidableRelEventKPSLe : DecidableRel KPSLe

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.instDecidableRelEventKPSLe A B = id inferInstance

@[instance_reducible]

instance Scott1964.MeasurementStructures.Probability.KPSCounterexample.instDecidableRelEventKPSLt : DecidableRel KPSLt

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.instDecidableRelEventKPSLt A B = id inferInstance

@[instance_reducible]

instance Scott1964.MeasurementStructures.Probability.KPSCounterexample.instDecidableRelEventKPSGe : DecidableRel KPSGe

Equations

• Scott1964.MeasurementStructures.Probability.KPSCounterexample.instDecidableRelEventKPSGe A B = id inferInstance

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.kpsRank_injective : Function.Injective kpsRank

The table gives distinct ranks to all 32 events.

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.comparable (A B : Event) : KPSLe A B ∨ KPSLe B A

Comparability (C).

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.transitive {A B C : Event} : KPSLe A B → KPSLe B C → KPSLe A C

Transitivity (T).

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.empty_le (A : Event) : KPSLe ∅ A

The empty event is no more likely than every event.

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.disjoint_union_invariance (A B C : Event) (hCA : Disjoint C A) (hCB : Disjoint C B) : KPSLe A B ↔ KPSLe (A ∪ C) (B ∪ C)

De Finetti's disjoint-union invariance (A). The finite check only concerns inserting one atom; induction gives arbitrary disjoint unions.

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.qs_lt_p : KPSLt {q, s} {p}

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.pq_lt_rs : KPSLt {p, q} {r, s}

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.ps_lt_tq : KPSLt {p, s} {t, q}

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.rt_lt_spq : KPSLt {r, t} {s, p, q}

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.measure_eq_sum_singletons {μ : Event → ℝ} (hμ : IsProbability μ) (A : Event) : μ A = ∑ i ∈ A, μ {i}

Finite additivity determines every event from its singleton values.

def Scott1964.MeasurementStructures.Probability.KPSCounterexample.StrictlyRepresents (μ : Event → ℝ) : Prop

Strict numerical representation of the KPS strict order.

Equations

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

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.no_strictly_representing_probability : ¬∃ (μ : Event → ℝ), IsProbability μ ∧ StrictlyRepresents μ

No real finitely additive probability strictly represents the displayed Kraft–Pratt–Seidenberg order.

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.kpsGe_nontrivial : ¬KPSGe ⊥ ⊤

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.kpsGe_bottom (A : Event) : KPSGe A ⊥

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.kpsGe_total : ProbTotal KPSGe

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.kpsGe_transitive : ProbTransitive KPSGe

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.kpsGe_disjointUnionInvariant : ProbDisjointUnionInvariant KPSGe

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.kpsGe_deFinettiAxioms : DeFinettiAxioms KPSGe

The exact KPS order satisfies de Finetti's five axioms, with condition (i) in its original weak form ¬ R ⊥ ⊤.

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.measure_strict_of_kpsLt {μ : Event → ℝ} (hrep : ∀ (A B : Event), KPSGe A B ↔ μ A ≥ μ B) {A B : Event} (hAB : KPSLt A B) : μ A < μ B

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.not_realizableProbability_kpsGe : ¬RealizableProbability KPSGe

No shared-API probability weakly represents the exact KPS “at least as probable” order. The contradiction uses the paper's four decisive inequalities.

theorem Scott1964.MeasurementStructures.Probability.KPSCounterexample.deFinetti_axioms_insufficient : DeFinettiAxioms KPSGe ∧ ¬RealizableProbability KPSGe

De Finetti's five axioms are insufficient for finite additive-probability representation.