Documentation

Linglib.Theories.Semantics.Modality.PosteriorThreshold

Posterior-threshold modality #

A simplified posterior-based necessity operator: must φ iff P(φ) > θ for some contextual threshold. This is the baseline posterior competitor against which more sophisticated probabilistic operators (@cite{lassiter-2017}, @cite{chung-mascarenhas-2024}, @cite{goodhue-2017}, the threshold-PMF tradition) define themselves.

It is not a faithful Lassiter operator — Lassiter's account adds context-conditionalization, an alternatives clause, and an epistemic / deontic asymmetry. Use mustPosterior only where the goal is to expose posterior-monotonicity as a structural constraint that necessity accounts may or may not satisfy.

Headline structural fact #

posterior_cannot_predict_conjunction_fallacy: a one-line corollary of the substrate theorem Semantics.Modality.ThresholdOperator.subsetFallacy_blocked_by_monotone applied to posteriorEval_isPosteriorMonotone. The modal-conjunction- fallacy direction (sub-claim true at θ, super-claim false at θ) is impossible under any posterior-monotone eval — and posteriorEval is trivially posterior-monotone via PMF.probOfSet_mono.

source
noncomputable def Semantics.Modality.PosteriorThreshold.posteriorEval {W : Type u_1} [Fintype W] :
ThresholdOperator.EvalFn W

The posterior eval function as an EvalFn: just probOfSet packaged in the shared shape.

Equations
Instances For
    source
    theorem Semantics.Modality.PosteriorThreshold.posteriorEval_isPosteriorMonotone {W : Type u_1} [Fintype W] :
    ThresholdOperator.IsPosteriorMonotone posteriorEval

    Posterior is monotone — immediate from PMF.probOfSet_mono.

    source
    def Semantics.Modality.PosteriorThreshold.mustPosterior {W : Type u_1} [Fintype W] (p : PMF W) (φ : Set W) (θ : ENNReal) :
    Prop

    Posterior-threshold necessity: must φ iff P(φ) > θ. The simplest probability-based necessity operator.

    Equations
    Instances For
      source
      theorem Semantics.Modality.PosteriorThreshold.posterior_cannot_predict_conjunction_fallacy {W : Type u_1} [Fintype W] (p : PMF W) {sub super : Set W} (hSub : sub ⊆ super) (θ : ENNReal) :
      ¬(mustPosterior p sub θ ∧ ¬mustPosterior p super θ)

      Structural impossibility of the modal conjunction fallacy under posterior-threshold necessity. One-line corollary of subsetFallacy_blocked_by_monotone applied to posteriorEval_isPosteriorMonotone.