Documentation

Linglib.Semantics.Conditionals.Probabilistic

Probabilistic Conditional Semantics #

[Ada65] [JE91] [Dou08] [Kau05a] [Kau13] [Pea13]

The conditional if φ then γ as the expected value of γ given φ.

[Ada65] proposes that the assertability of an indicative conditional if φ then ψ equals the conditional probability P(ψ ∣ φ). [JE91] push this further: the conditional denotation is P(ψ ∣ φ). [Dou08] provides the evidential support theory variant; [Kau05a] [Kau13] extend to causal premise semantics; [Pea13] develops the structural-counterfactual face.

[CM23] eq. 44 promotes the consequent from a proposition to a measure function γ : W → ℝ≥0∞:

⟦if φ, γ⟧^w = E_w[γ ∣ φ]

When γ is the indicator of ψ this reduces to the [Ada65]/[JE91] conditional probability (condIf_propositional). When γ is the count-of-relevant-propositions μ_R(w) = |{r ∈ R ∣ r true at w}|, it yields C&M's "explanatory value" / "expected utility". One operator, two flavors.

condIf is an abbrev for PMF.condExpect: the wrapping is for linguistic naming only; the equality is definitional. The Lewis 1976 triviality results bear on identifying the conditional with a proposition in some space; we are content to identify it with a number (an expected value), so they do not bite.

Out of scope #

Counterfactual conditionals (intervention semantics [Pea13]; see Core/Causal/SEM/Counterfactual.lean) and the Stalnaker selection-function tradition (Semantics/Conditionals/SelectionFunction.lean) are formalized elsewhere. Their relation to the probabilistic conditional is itself a research question ([Sch11b], [CZC18]).

@[reducible, inline]
noncomputable abbrev Semantics.Conditionals.Probabilistic.condIf {W : Type u_1} [Fintype W] (p : PMF W) (φ : Set W) (γ : WENNReal) :
ENNReal

[CM23] compositional conditional: ⟦if φ, γ⟧^w = E_w[γ ∣ φ]. Definitionally condExpect.

Equations
Instances For
    theorem Semantics.Conditionals.Probabilistic.condIf_propositional {W : Type u_1} [Fintype W] (p : PMF W) (φ ψ : Set W) :
    condIf p φ (ψ.indicator fun (x : W) => 1) = p.condProbSet φ ψ

    [Ada65]: when the consequent is the indicator of ψ, the conditional reduces to the conditional probability P(ψ ∣ φ).