Probabilistic Aristotelian relations

When the model class W is equipped with a probability measure μ : PMF W, the four Aristotelian relations have natural probabilistic generalisations as linear (in)equalities on the probabilities P_μ[φ] := μ({w | φ w = true}):

Boolean Aristotelian relation	Probabilistic counterpart
Contradictory φ ψ	P[φ] + P[ψ] = 1
Contrary φ ψ	P[φ] + P[ψ] ≤ 1
Subcontrary φ ψ	P[φ] + P[ψ] ≥ 1
Subaltern φ ψ	P[φ] ≤ P[ψ]

This is the convex extension of the Boolean Aristotelian geometry: the discrete case (each μ a ∈ {0,1}) recovers Definition 1 of @cite{demey-smessaert-2018} exactly; the convex case is what Bayesian listeners actually compute.

Why this matters for RSA / Bayesian-pragmatic models

The Tessler–Tenenbaum–Goodman 2022 syllogistic model (and any RSA-style Bayesian-pragmatic model that reasons about quantifier inference) computes a posterior μ : PMF W over states given premises, then evaluates conclusion probabilities P_μ[c]. The Belief Alignment / State Communication / Literal Speaker utilities are functionals of these P_μ[c] values across the conclusion space — and those values are jointly constrained by the probabilistic Aristotelian inequalities. Subalternation P[All A-C] ≤ P[Some A-C] for the same posterior μ is a constraint the speaker model respects automatically.

Transfer theorems

The key result of this file: if φ and ψ stand in a Boolean Aristotelian relation, then they stand in the corresponding probabilistic relation under every probability measure μ. The Boolean → probabilistic direction is free; the converse fails (μ-specific equalities can hold without Boolean entailment). For example, two Boolean-Unconnected predicates φ, ψ can satisfy P_μ[φ] + P_μ[ψ] = 1 for a particular μ that happens to allocate measure exactly to {φ ∨ ψ} and zero to {¬φ ∧ ¬ψ}, without being Boolean-contradictory.

Related literature

The probabilistic-square tradition is distinct from the Logica Universalis "abstract Aristotelian diagrams" tradition that this file specializes. Pfeifer and collaborators (Pfeifer 2006, Pfeifer & Sanfilippo subsequent work) develop probabilistic squares of opposition based on coherent conditional probability; that line gives a different (conditional, not absolute) reading of the four inequalities. The version here is the unconditional / absolute form, appropriate for RSA-style models where the posterior μ : PMF W over states is the object of study. (Bib entries for the Pfeifer line not yet in linglib; add when a consumer needs the conditional version.)

noncomputable def Core.Opposition.boolProb {W : Type u_1} (μ : PMF W) (φ : W → Bool) : ENNReal

The probability of a Boolean predicate φ : W → Bool under μ : PMF W, i.e. μ({w | φ w = true}). Built on Finite.probOfSet.

Equations

• P[φ ; μ] = μ.probOfSet {w : W | φ w = true}

def Core.Opposition.«termP[_;_]» : Lean.ParserDescr

The probability of a Boolean predicate φ : W → Bool under μ : PMF W, i.e. μ({w | φ w = true}). Built on Finite.probOfSet.

Equations

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

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

Total probability: P[φ] + P[¬φ] = 1. The basic conservation law. Proof: convert each side to a Finset sum via toOuterMeasure_apply_fintype, then observe that the two indicators are pointwise complementary and sum to μ x at every x; PMF totality (tsum_coe) closes the result.

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

Probabilistic contradictoriness: P[φ] + P[ψ] = 1. Discrete case recovers Contradictory.

Equations

• Core.Opposition.ProbContradictory μ φ ψ = (P[φ ; μ] + P[ψ ; μ] = 1)

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

Probabilistic contrariety: P[φ] + P[ψ] ≤ 1, with strict inequality possible. Discrete case recovers Contrary (where P[φ] + P[ψ] < 1 when neither holds at some world).

Equations

• Core.Opposition.ProbContrary μ φ ψ = (P[φ ; μ] + P[ψ ; μ] ≤ 1)

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

Probabilistic subcontrariety: P[φ] + P[ψ] ≥ 1. Discrete case recovers Subcontrary (where P[φ] + P[ψ] > 1 when both hold at some world).

Equations

• Core.Opposition.ProbSubcontrary μ φ ψ = (P[φ ; μ] + P[ψ ; μ] ≥ 1)

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

Probabilistic subalternation: P[φ] ≤ P[ψ]. Discrete case (Boolean Subaltern φ ψ) implies this for every μ via monotonicity of μ.

Equations

• Core.Opposition.ProbSubaltern μ φ ψ = (P[φ ; μ] ≤ P[ψ ; μ])

theorem Core.Opposition.Contradictory.toProb {W : Type u_1} [Fintype W] {φ ψ : W → Bool} (h : Contradictory φ ψ) (μ : PMF W) : ProbContradictory μ φ ψ

Boolean contradictoriness implies probabilistic contradictoriness for every probability measure. Direct from boolProb_add_compl once we note that Contradictory φ ψ makes ψ pointwise !φ.

theorem Core.Opposition.Subaltern.toProb {W : Type u_1} [Fintype W] {φ ψ : W → Bool} (h : Subaltern φ ψ) (μ : PMF W) : ProbSubaltern μ φ ψ

Boolean subalternation implies probabilistic subalternation: if φ ⊨ ψ holds pointwise, then P_μ[φ] ≤ P_μ[ψ] for every μ (PMF monotonicity).

theorem Core.Opposition.Contrary.toProb {W : Type u_1} [Fintype W] {φ ψ : W → Bool} (h : Contrary φ ψ) (μ : PMF W) : ProbContrary μ φ ψ

Boolean contrariety implies probabilistic contrariety: if φ and ψ cannot both be true, then P[φ] + P[ψ] ≤ 1. At each x, the two indicators sum to at most μ x (both nonzero would mean φ ∧ ψ at x).

theorem Core.Opposition.Subcontrary.toProb {W : Type u_1} [Fintype W] {φ ψ : W → Bool} (h : Subcontrary φ ψ) (μ : PMF W) : ProbSubcontrary μ φ ψ

Boolean subcontrariety implies probabilistic subcontrariety: if φ ∨ ψ is valid, then P[φ] + P[ψ] ≥ 1. At each x, the indicator sum is at least μ x (at least one of φ, ψ is true at x by h.2).