Documentation

Linglib.Phenomena.Focus.AdditiveParticles.Studies.Thomas2026

Thomas (2026): Probabilistic, question-based additivity #

@cite{thomas-2026} @cite{ciardelli-groenendijk-roelofsen-2018} @cite{frank-goodman-2012}

Formalisation of @cite{thomas-2026} "A probabilistic, question-based approach to additivity" (S&P 19:1). The paper unifies the canonical additive use of too with a previously unstudied "argument-building use" by formalising felicity in terms of Bayesian inquisitive answerhood — Def 62 of the paper. The substrate primitives (Answers, IsResolutionEvidencedBy, evidencesResolutionMore) live in Theories/Semantics/Questions/Probabilistic.lean; this file encodes Def 64 (TOO felicity) and the abstract consequences that account for the empirical contrasts in §3 and §4.

Def 64: TOO(π) felicity #

TOO(π) is felicitous iff there exists a contextually relevant question RQ and an antecedent fact ANT such that:

(i) prevents too from being felicitous when the prejacent already entails the answer suggested by the conjunction (the @cite{beaver-clark-2008} ecstatic case (29a)). (ii) prevents too from being felicitous when a weaker prejacent would do (the "some-instrument vs cello" case (30)).

TOO felicity (@cite{thomas-2026} Def 64) #

source
structure Phenomena.AdditiveParticles.Thomas2026.IsTooFelicitous {W : Type u_1} (prejacent antecedent : Set W) (rq : Core.Question W) (μ : PMF W) :
Prop

TOO(π) felicity in the sense of @cite{thomas-2026} Def 64. The five conditions are bundled below as a structure so consumers can project them by name.

Instances For

    Abstract consequences #

    source
    theorem Phenomena.AdditiveParticles.Thomas2026.IsTooFelicitous.antecedent_probOfSet_pos {W : Type u_1} {μ : PMF W} {prejacent antecedent : Set W} {rq : Core.Question W} (h : IsTooFelicitous prejacent antecedent rq μ) :
    μ.probOfSet antecedent > 0

    TOO felicity entails that the antecedent puts positive prior mass: a direct corollary of Answers.probOfSet_pos applied to the antecedent condition.

    source
    theorem Phenomena.AdditiveParticles.Thomas2026.IsTooFelicitous.conjunction_probOfSet_pos {W : Type u_1} {μ : PMF W} {prejacent antecedent : Set W} {rq : Core.Question W} (h : IsTooFelicitous prejacent antecedent rq μ) :
    μ.probOfSet (antecedent ∩ prejacent) > 0

    TOO felicity entails that the conjunction puts positive prior mass — same corollary applied to the conjunction condition.

    source
    theorem Phenomena.AdditiveParticles.Thomas2026.IsTooFelicitous.exists_strict_improvement {W : Type u_1} {μ : PMF W} {prejacent antecedent : Set W} {rq : Core.Question W} (h : IsTooFelicitous prejacent antecedent rq μ) :
    ∃ (𝒜 : Set (Set W)), Semantics.Questions.Probabilistic.IsResolutionEvidencedBy rq 𝒜 (antecedent ∩ prejacent) μ ∧ μ.condProbSet (antecedent ∩ prejacent) (⋂₀ 𝒜) > μ.condProbSet antecedent (⋂₀ 𝒜)

    TOO felicity entails that the conjunction is genuinely stronger evidence than the antecedent alone (the @cite{thomas-2026} §4.4 intuition that too marks a strict improvement). The witness 𝒜 from the conjunction-stronger field exhibits this.

    RQ vs CQ — the contextual-relevance layer (@cite{thomas-2026} §5.4.3, §5.5) #

    The RQ in IsTooFelicitous need not be a Current Question (CQ) in the discourse tree — it only needs to be relevant to one (the DQ or some other in-scope question). This generalization is what licenses too in cases like (45c) [implicit RQ] and (71) [single wh-answer to multiple-wh CQ]. The relevance check uses Probabilistic.IsRelevantTo (Def 61).

    source
    def Phenomena.AdditiveParticles.Thomas2026.IsTooLicensedByDQ {W : Type u_1} (prejacent antecedent : Set W) (rq dq : Core.Question W) (μ : PMF W) :
    Prop

    TOO licensed by an RQ that is in turn relevant to some discourse question DQ. This is the full felicity condition (@cite{thomas-2026} Def 64) — IsTooFelicitous itself only constrains rq, but the paper requires rq to be Relevant to some dq in the discourse tree.

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

      Predicted infelicity #

      If the RQ does not satisfy the felicity conditions for any candidate in the discourse, too is predicted infelicitous. Two characteristic infelicity patterns from §5.5:

      source
      def Phenomena.AdditiveParticles.Thomas2026.IsTooInfelicitous {W : Type u_1} (prejacent antecedent : Set W) (μ : PMF W) :
      Prop

      @cite{thomas-2026} §5.5 (ex 72): if no contextually relevant rq has the prejacent providing additional evidence beyond the antecedent, too is infelicitous. The infelicity is captured by the absence of any felicitous RQ for the given (prejacent, ant).

      Equations
      Instances For
        source
        def Phenomena.AdditiveParticles.Thomas2026.IsTooInfelicitousAgainstCQ {W : Type u_1} (prejacent antecedent : Set W) (cq : Core.Question W) (μ : PMF W) :
        Prop

        @cite{thomas-2026} §5.5.1 (ex 75): if a single wh-answer (e.g., "Bailey ate spaghetti") is offered against a multiple-wh CQ (e.g., "Who ate what?") whose resolutions specify what every salient individual ate, no rq over alt(CQ) satisfies the Conjunction Condition because the antecedent alone (e.g., "Avery ate pizza") doesn't constrain Bailey. Too is infelicitous unless the CQ is reinterpreted (cf. ex 77, where multiple-wh admits a mention-some single-pair reading).

        Equations
        Instances For

          Empirical predictions catalog #

          The proposal accounts for the following data from the paper. Each entry pairs a numbered example with the structural reason it is licensed (✓) or predicted infelicitous (✗). Worked numerical formalisations are deferred to per-example study artifacts.

          Argument-building uses (§3, §5.3) #

          Canonical additive uses (§5.4) #

          Predicted infelicity (§5.5) #

          Other distributional facts (§5.5.2) #