Documentation

Linglib.Logic.ComparativeProbability.Completeness

Representation and completeness theorems #

Kraft, Pratt and Seidenberg show that every qualitative probability on fewer than five atoms is represented by a probability measure, and give one on five atoms that is not; padding it with null atoms gives one at every larger size. Following van der Hoek, every qualitative probability on a finite carrier is still represented by a qualitatively additive measure, since any normalized numerical representation of it is one (QualAddMeasure.ofRepr).

Main statements #

References #

The Kraft–Pratt–Seidenberg counterexample #

source
def ComparativeProbability.finsetIdx (s : Finset (Fin 5)) :
ℕ

finsetIdx s encodes a subset of Fin 5 as a bitmask.

Equations
Instances For
    source
    def ComparativeProbability.kpsRankNat (idx : ℕ) :
    ℕ

    kpsRankNat ranks the 32 subsets of Fin 5, indexed by bitmask, in the Kraft–Pratt–Seidenberg order. With atoms p, q, r, s, t numbered 0, …, 4, the lower half is ∅ < q < r < s < qr < qs < p < pq < rs < t < qrs < rp < ps < tq < qrp < rt, and the complements follow in reverse order.

    Equations
    Instances For
      source
      def ComparativeProbability.kpsRank (s : Finset (Fin 5)) :
      ℕ

      kpsRank s is the rank of s in the Kraft–Pratt–Seidenberg order.

      Equations
      Instances For
        source
        theorem ComparativeProbability.kps_mono_finset (a b : Finset (Fin 5)) :
        a ⊆ b → kpsRank b ≥ kpsRank a
        source
        noncomputable def ComparativeProbability.kpsRankSet (A : Set (Fin 5)) :
        ℕ

        kpsRankSet A is the Kraft–Pratt–Seidenberg rank of a set.

        Equations
        Instances For
          source
          noncomputable def ComparativeProbability.kpsGe (A B : Set (Fin 5)) :
          Prop

          kpsGe A B compares two sets by their Kraft–Pratt–Seidenberg rank.

          Equations
          Instances For
            source
            instance ComparativeProbability.instIsQualitativeProbabilitySetFinOfNatNatKpsGe :
            IsQualitativeProbability kpsGe

            The Kraft–Pratt–Seidenberg order is a qualitative probability on the subsets of Fin 5.

            source
            theorem ComparativeProbability.kps_not_representable :
            ¬Representable kpsGe

            The Kraft–Pratt–Seidenberg order is not representable. Its four comparisons kpsFamily hold strictly and their sign vectors cancel, so Scott's theorem (representable_iff_cancellation) would force qs ≿ p.

            Padding with null atoms #

            source
            theorem ComparativeProbability.representable_of_pad {n : ℕ} {r : Set (Fin n) → Set (Fin n) → Prop} [Std.Refl r] (h : Representable (Set.preimage Fin.castSucc ⁻¹'o r)) :
            Representable r

            Padding reflects representability. Pulling r back along the preimage of Fin.castSucc adds a null atom Fin.last n; a measure for the padded relation gives that atom measure zero, and its restriction along Fin.castSucc represents r.

            source
            theorem ComparativeProbability.exists_nonrepresentable_fin {n : ℕ} (h : 5 ≤ n) :
            ∃ (r : Set (Fin n) → Set (Fin n) → Prop), IsQualitativeProbability r ∧ ¬Representable r

            For every n ≥ 5 some qualitative probability on Fin n is not representable, as the Kraft–Pratt–Seidenberg counterexample padded with null atoms shows.

            The Kraft–Pratt–Seidenberg theorems #

            source
            theorem ComparativeProbability.representable_of_card_lt_five {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (r : Set W → Set W → Prop) [IsQualitativeProbability r] (hcard : Fintype.card W < 5) :
            Representable r

            Kraft–Pratt–Seidenberg below five atoms. Every qualitative probability on fewer than five atoms is representable by a probability measure.

            source
            theorem ComparativeProbability.exists_nonrepresentable_of_five_le_card {W : Type u_1} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] (hcard : 5 ≤ Fintype.card W) :
            ∃ (r : Set W → Set W → Prop), IsQualitativeProbability r ∧ ¬Representable r

            Kraft–Pratt–Seidenberg from five atoms on. Some qualitative probability is not representable by any probability measure.

            Qualitatively additive representation #

            source
            theorem ComparativeProbability.exists_qualAddMeasure_repr {W : Type u_1} [Fintype W] (r : Set W → Set W → Prop) [IsQualitativeProbability r] :
            ∃ (m : QualAddMeasure ℚ W), ∀ (A B : Set W), r A B ↔ m.inducedGe A B

            Qualitatively additive representation. Every qualitative probability on a finite carrier is represented by a qualitatively additive measure: the count of dominated sets, affinely renormalised so that μ(∅) = 0 and μ(Ω) = 1, is a normalized numerical representation (QualAddMeasure.ofRepr).

            Qualitative and finite additivity #

            source
            theorem ComparativeProbability.axiomA_iff_fa {W : Type u_1} (ge : Set W → Set W → Prop) :
            (∀ (A B : Set W), ge A B ↔ ge (A \ B) (B \ A)) ↔ ∀ (A B C : Set W), (∀ x ∈ A, x ∉ C) → (∀ x ∈ B, x ∉ C) → (ge A B ↔ ge (A ∪ C) (B ∪ C))

            For any comparison on sets, qualitative additivity is equivalent to finite additivity in the form that adding a disjoint set to both sides preserves the comparison.