Probabilistic Aristotelian relations

When W carries a probability measure μ : PMF W, the four Aristotelian relations generalise to linear (in)equalities on P_μ[φ] := μ {w | φ w = true}:

Boolean relation	Probabilistic counterpart
IsContradictory φ ψ	P[φ] + P[ψ] = 1
IsContrary φ ψ	P[φ] + P[ψ] ≤ 1
IsSubcontrary φ ψ	P[φ] + P[ψ] ≥ 1
IsSubaltern φ ψ	P[φ] ≤ P[ψ]

The discrete case (μ a ∈ {0,1}) recovers Definition 1 of [DS18a]. The main results are the transfer theorems: a Boolean Aristotelian relation implies its probabilistic counterpart under every μ (the converse fails).

Probability of a Boolean predicate

@[reducible, inline]

noncomputable abbrev Aristotelian.boolProb {W : Type u_1} (μ : PMF W) (φ : W → Bool) : ENNReal

The probability of φ : W → Bool under μ : PMF W, i.e. μ {w | φ w = true}.

Equations

• Aristotelian.boolProb μ φ = μ.probOfSet {w : W | φ w = true}

theorem Aristotelian.boolProb_add_compl {W : Type u_1} [Fintype W] (μ : PMF W) (φ : W → Bool) : (boolProb μ φ + boolProb μ fun (w : W) => !φ w) = 1

Total probability: P[φ] + P[¬φ] = 1, via PMF.probOfSet_compl_add.

Probabilistic Aristotelian relations (Definition 1, convex form)

def Aristotelian.ProbContradictory {W : Type u_1} (μ : PMF W) (φ ψ : W → Bool) : Prop

Probabilistic contradictoriness: P[φ] + P[ψ] = 1.

Equations

• Aristotelian.ProbContradictory μ φ ψ = (Aristotelian.boolProb μ φ + Aristotelian.boolProb μ ψ = 1)

def Aristotelian.ProbContrary {W : Type u_1} (μ : PMF W) (φ ψ : W → Bool) : Prop

Probabilistic contrariety: P[φ] + P[ψ] ≤ 1.

Equations

• Aristotelian.ProbContrary μ φ ψ = (Aristotelian.boolProb μ φ + Aristotelian.boolProb μ ψ ≤ 1)

def Aristotelian.ProbSubcontrary {W : Type u_1} (μ : PMF W) (φ ψ : W → Bool) : Prop

Probabilistic subcontrariety: P[φ] + P[ψ] ≥ 1.

Equations

• Aristotelian.ProbSubcontrary μ φ ψ = (Aristotelian.boolProb μ φ + Aristotelian.boolProb μ ψ ≥ 1)

def Aristotelian.ProbSubaltern {W : Type u_1} (μ : PMF W) (φ ψ : W → Bool) : Prop

Probabilistic subalternation: P[φ] ≤ P[ψ].

Equations

• Aristotelian.ProbSubaltern μ φ ψ = (Aristotelian.boolProb μ φ ≤ Aristotelian.boolProb μ ψ)

Transfer theorems: Boolean ⇒ Probabilistic (for every μ)

theorem Aristotelian.ProbContradictory.of_isContradictory {W : Type u_1} [Fintype W] {φ ψ : W → Bool} (h : IsContradictory φ ψ) (μ : PMF W) : ProbContradictory μ φ ψ

Boolean contradictoriness transfers to every measure: {ψ} is the complement of {φ}.

theorem Aristotelian.ProbSubaltern.of_isSubaltern {W : Type u_1} {φ ψ : W → Bool} (h : IsSubaltern φ ψ) (μ : PMF W) : ProbSubaltern μ φ ψ

Boolean subalternation transfers to every measure (probOfSet monotonicity).

theorem Aristotelian.ProbContrary.of_isContrary {W : Type u_1} [Fintype W] {φ ψ : W → Bool} (h : IsContrary φ ψ) (μ : PMF W) : ProbContrary μ φ ψ

Boolean contrariety transfers to every measure: {φ} ⊆ {ψ}ᶜ, so P[φ] ≤ 1 - P[ψ].

theorem Aristotelian.ProbSubcontrary.of_isSubcontrary {W : Type u_1} [Fintype W] {φ ψ : W → Bool} (h : IsSubcontrary φ ψ) (μ : PMF W) : ProbSubcontrary μ φ ψ

Boolean subcontrariety transfers to every measure: {ψ}ᶜ ⊆ {φ}, so 1 - P[ψ] ≤ P[φ].