Documentation

Linglib.Theories.Semantics.Lexical.Particle.Additive

Additive Particles: too, also, either #

@cite{heim-1992} @cite{kripke-2009} @cite{thomas-2026}

Felicity conditions for additive particles following @cite{thomas-2026} "A probabilistic, question-based approach to additivity".

Heim 1992 Subsumption #

@cite{thomas-2026} §6 argues that Def. 64 subsumes @cite{heim-1992}'s individual-based additive presupposition as a special case. This is proved formally by heim_subsumption: when ANT and π each entail distinct alternatives of RQ (the Heim setup), the Antecedent and Conjunction Conditions (Def. 64a-b) hold automatically.

Insight: Argument-Building Use #

The novel contribution of @cite{thomas-2026} is explaining the "argument-building" use of "too" where the antecedent and prejacent aren't focus alternatives but jointly build an argument for some conclusion.

Example (@cite{thomas-2026}, ex. 1c/14c/65): "A room just opened up at this hotel. It looks kind of fancy, too."

Definition 64: Felicity Conditions for TOO(π) #

Given resolved question RQ and antecedent ANT:

  1. Antecedent Condition: ANT probabilistically answers RQ
  2. Conjunction Condition: ANT ∧ ⟦π⟧ evidences some resolution A more strongly than ANT alone
  3. Prejacent Conditions:
    • ⟦π⟧ doesn't entail the evidenced resolution
    • No weaker proposition works as well

Standard vs Argument-Building Uses #

Standard use: ANT and π are focus alternatives

Argument-building use: ANT and π jointly support a conclusion

Types of additive particles.

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

      Check if particle is licensed in a given polarity context.

      Equations
      Instances For

        Discourse context for evaluating additive particle felicity.

        @cite{thomas-2026} requires:

        • A resolved question (RQ) in the discourse
        • An antecedent proposition (ANT) that answers RQ
        • A prior probability distribution
        Instances For

          Create a context from a polar question.

          Equations
          Instances For

            Create a context from a list of alternatives.

            Equations
            Instances For

              Condition 1: Antecedent probabilistically answers RQ (Def. 64a).

              The antecedent must raise the probability of some resolution.

              Uses probAnswers (condition (a) of Def. 62 only), which checks that some alternative's conditional probability exceeds its prior. For polar/binary QUDs, this is equivalent to the full Def. 62 (probAnswersFull) by probAnswersFull_eq_simple_binary. For non-binary questions, the full definition additionally requires Bayes-factor dominance (condition (b)).

              Equations
              Instances For

                Condition 2: Conjunction answers RQ and evidences more strongly.

                @cite{thomas-2026} Def. 64b: ANT ∩ ⟦π⟧ Answers RQ, AND RQ|_{ANT∩⟦π⟧} is Evidenced more strongly by ANT ∩ ⟦π⟧ than by ANT.

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

                  Get the resolution(s) that are strengthened by the conjunction.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Semantics.Lexical.Particle.Additive.nonTrivialityConditionWith {W : Type u_1} (prejacent : WBool) (strengthened : List (Discourse.InfoState W)) (worlds : List W) :

                    Condition 3a: Prejacent doesn't entail the evidenced resolution.

                    π shouldn't make the conclusion trivially certain. Uses a provided world list for computability.

                    TODO: This checks .any over all strengthened alternatives, but should check against the specific Q|_{ANT∩π} from Def. 62. For singleton resolutions (all paper examples), the behavior is identical.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Semantics.Lexical.Particle.Additive.maximalityCondition {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (strengthened : List (Discourse.InfoState W)) (worlds : List W) :

                      Condition 3b: No weaker proposition works as well (Def. 64c.ii).

                      For every strengthened resolution R, no strict weakening S ⊃ ⟦π⟧ should evidence R at least as strongly as π does given ANT.

                      Over finite types this reduces to an entailment check: for every world w with positive prior, ANT(w) ∧ R(w) → π(w). If this holds, then for any S ⊃ ⟦π⟧, since ANT ∩ S ⊇ ANT ∩ π, conditioning on the larger set ANT ∩ S can only dilute the probability of R (subset dilution of conditional probability), so P(R | ANT ∩ π) ≥ P(R | ANT ∩ S), preserving strict evidence advantage.

                      TODO: Like nonTrivialityConditionWith, this uses all strengthened alternatives instead of the specific Q|_{ANT∩π}. Correct for singleton resolutions (all paper examples).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Semantics.Lexical.Particle.Additive.tooFelicitousWith {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (worlds : List W) :

                        Full felicity conditions for TOO(π) with explicit world list.

                        Definition 64 from @cite{thomas-2026}.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          noncomputable def Semantics.Lexical.Particle.Additive.tooFelicitous {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) :

                          Noncomputable version using Fintype.elems.

                          Equations
                          Instances For
                            noncomputable def Semantics.Lexical.Particle.Additive.alsoFelicitous {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) :

                            Felicity for "also" — same core conditions as "too".

                            @cite{thomas-2026} §6 (ex. 86) observes that sentence-initial "also" is NOT subject to the Prejacent Condition part (ii) (maximality): "Also, Bailey plays the cello" is acceptable where "#Bailey plays the cello, too" is not. This implementation does not model syntactic position and applies full felicity conditions regardless. A position-sensitive version would skip maximalityCondition for sentence-initial "also".

                            Equations
                            Instances For
                              noncomputable def Semantics.Lexical.Particle.Additive.eitherFelicitous {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (inNegativeContext : Bool) :

                              Felicity for "either" — placeholder, gates on negative polarity.

                              @cite{thomas-2026} explicitly defers a precise characterization of "either" to future work (footnote 9). This placeholder simply gates on polarity; the actual felicity conditions for "either" likely involve additional constraints (see @cite{ahn-2015} for an alternative account using ⊔ in a Boolean algebra).

                              Equations
                              Instances For

                                Types of additive particle uses (@cite{thomas-2026}).

                                Thomas's framework is binary: either ANT and π are focus alternatives (standard) or they are not (argument-building).

                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Semantics.Lexical.Particle.Additive.isFocusAlternativeUseWith {W : Type u_1} (ant prejacent : WBool) (rq : Discourse.Issue W) (worlds : List W) :

                                    Heuristic: check if ANT and π each overlap some alternative of RQ.

                                    This is a NECESSARY but not SUFFICIENT condition for focus-alternative use. It only checks that both ANT and π are non-trivially consistent with some RQ alternative — this is much weaker than actual focus-alternative structure (which would require ANT and π to be related by substitution of the focused constituent). Every pair of non-trivial propositions passes this check for sufficiently fine-grained questions.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      noncomputable def Semantics.Lexical.Particle.Additive.isFocusAlternativeUse {W : Type u_1} [Fintype W] (ant prejacent : WBool) (rq : Discourse.Issue W) :

                                      Noncomputable version using Fintype.

                                      Equations
                                      Instances For
                                        noncomputable def Semantics.Lexical.Particle.Additive.isArgumentBuildingUse {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) :

                                        Check if this is an argument-building use.

                                        In argument-building use:

                                        1. ANT and π are NOT focus alternatives
                                        2. Together they provide cumulative evidence for some conclusion
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          noncomputable def Semantics.Lexical.Particle.Additive.classifyUse {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) :

                                          Classify the use type of an additive particle.

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

                                            Central Theorems #

                                            These theorems capture the key linguistic insights of @cite{thomas-2026}:

                                            1. Standard Use Reduction: When π directly determines an alternative of RQ, the probabilistic felicity conditions reduce to the traditional analysis.

                                            2. Argument-Building Characterization: Argument-building arises exactly when neither ANT nor π directly determines an alternative, but together they provide cumulative evidence.

                                            3. Cumulative Evidence Necessity: If π provides no additional evidence beyond ANT, "too" is infelicitous.

                                            def Semantics.Lexical.Particle.Additive.directlyDetermines {W : Type u_1} (p alt : WBool) (worlds : List W) :

                                            A proposition "directly determines" an alternative if it entails that alternative.

                                            When p directly determines alt, learning p makes P(alt) = 1.

                                            Equations
                                            Instances For

                                              Check if a proposition directly determines SOME alternative of an issue.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem Semantics.Lexical.Particle.Additive.standard_use_reduction {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (alt : Discourse.InfoState W) (_hAltInQ : alt ctx.resolvedQuestion.alternatives) (hEntails : ∀ (w : W), prejacent w = truealt w = true) (hNotAlreadyCertain : Questions.ProbabilisticAnswerhood.conditionalProb ctx.prior ctx.antecedent alt < 1) (_hAntPossible : Questions.ProbabilisticAnswerhood.probOfProp ctx.prior ctx.antecedent > 0) (hConjPossible : (Questions.ProbabilisticAnswerhood.probOfProp ctx.prior fun (w : W) => ctx.antecedent w && prejacent w) > 0) :

                                                Theorem: Standard Use Reduction

                                                When π directly determines an alternative A of the resolved question, and that alternative isn't already certain given ANT, then the conjunction condition is automatically satisfied.

                                                This captures why standard "too" works: if π = "Mary came" and this IS an alternative of "Who came?", then learning π guarantees that alternative, so ANT ∧ π always evidences it more strongly than ANT alone (unless ANT already entailed it).

                                                Linguistically: In standard focus-alternative uses, the general probabilistic conditions REDUCE TO the simple requirement that ANT be true and π be true. The complex probability calculations aren't needed - direct entailment suffices.

                                                theorem Semantics.Lexical.Particle.Additive.standard_use_conjunction_condition {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (alt : Discourse.InfoState W) (hAltInQ : alt ctx.resolvedQuestion.alternatives) (hEntails : ∀ (w : W), prejacent w = truealt w = true) (hNotAlreadyCertain : Questions.ProbabilisticAnswerhood.conditionalProb ctx.prior ctx.antecedent alt < 1) (hAntPossible : Questions.ProbabilisticAnswerhood.probOfProp ctx.prior ctx.antecedent > 0) (hConjPossible : (Questions.ProbabilisticAnswerhood.probOfProp ctx.prior fun (w : W) => ctx.antecedent w && prejacent w) > 0) (hAltNotCertain : Questions.ProbabilisticAnswerhood.probOfState ctx.prior alt < 1) :

                                                Corollary: Standard use satisfies the conjunction condition.

                                                When π directly determines some alternative and that alternative isn't already certain (neither given ANT nor a priori), the conjunction condition holds.

                                                theorem Semantics.Lexical.Particle.Additive.heim_subsumption {W : Type u_1} [Fintype W] [DecidableEq W] (ctx : AdditiveContext W) (prejacent : WBool) (altAnt altPi : Discourse.InfoState W) (hAntInQ : altAnt ctx.resolvedQuestion.alternatives) (hPiInQ : altPi ctx.resolvedQuestion.alternatives) (hAntEntails : ∀ (w : W), ctx.antecedent w = truealtAnt w = true) (hPiEntails : ∀ (w : W), prejacent w = truealtPi w = true) (hAntPossible : Questions.ProbabilisticAnswerhood.probOfProp ctx.prior ctx.antecedent > 0) (hConjPossible : (Questions.ProbabilisticAnswerhood.probOfProp ctx.prior fun (w : W) => ctx.antecedent w && prejacent w) > 0) (hAntAltNotCertain : Questions.ProbabilisticAnswerhood.probOfState ctx.prior altAnt < 1) (hPiAltNotCertain : Questions.ProbabilisticAnswerhood.probOfState ctx.prior altPi < 1) (hPiNotCertainGivenAnt : Questions.ProbabilisticAnswerhood.conditionalProb ctx.prior ctx.antecedent altPi < 1) :

                                                Theorem: Heim 1992 Subsumption (@cite{thomas-2026} §6).

                                                @cite{heim-1992}'s additive presupposition for TOO(π) requires: ∃x ≠ y such that P(x) is established and π = "y P'd".

                                                Under @cite{thomas-2026}'s Def. 64, this falls out as a SPECIAL CASE of the standard focus-alternative use. When ANT and π each entail distinct alternatives of RQ:

                                                • The Antecedent Condition holds because ANT entails an alternative, raising its probability to 1 (by probAnswers_when_entailing).
                                                • The Conjunction Condition holds because π entails another alternative that wasn't already certain given ANT, so ANT ∧ π provides new evidence (by standard_use_conjunction_condition).

                                                The remaining conditions (non-triviality, maximality) depend on the question structure and are verified concretely in the pizza/spaghetti scenario (Thomas2026.pizza_spaghetti_too_felicitous).

                                                This theorem makes precise the claim in @cite{thomas-2026} §6 that Def. 64 subsumes @cite{heim-1992}'s individual-based presupposition: every Heim-felicitous "too" is Thomas-felicitous, but Thomas additionally explains argument-building uses that Heim cannot.

                                                Theorem: Argument-Building Characterization

                                                Argument-building use arises exactly when:

                                                1. Neither ANT nor π directly determines any alternative of RQ
                                                2. But together, ANT ∧ π evidences some alternative more strongly than ANT alone

                                                This is the DEFINITION of argument-building: ANT and π are not themselves answers to RQ, but jointly serve as EVIDENCE for some answer.

                                                Example (@cite{thomas-2026}, ex. 1c/65): "A room just opened up at this hotel. It looks kind of fancy, too."

                                                • RQ = "What would be a good hotel?" (implicit)
                                                • ANT = "room just opened up" - doesn't determine which hotel is good
                                                • π = "looks fancy" - doesn't determine which hotel is good
                                                • But ANT ∧ π together raise the probability that this hotel is good
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Argument-building requires that the resolved question be about something OTHER than what ANT and π directly assert.

                                                  This captures the "implicit QUD" requirement: in argument-building, the question being addressed isn't "Did ANT happen?" or "Did π happen?" but rather some further question that ANT and π provide evidence for.

                                                  Two propositions are probabilistically independent given a third if P(A | B ∧ C) = P(A | B).

                                                  When π is independent of all alternatives given ANT, π provides no additional evidence - it's irrelevant to the question at hand.

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

                                                    π is evidentially irrelevant to Q given ANT if π doesn't change the probability of any alternative when we already know ANT.

                                                    Equations
                                                    Instances For
                                                      theorem Semantics.Lexical.Particle.Additive.cumulative_evidence_necessary {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (hIrrelevant : evidentiallyIrrelevant ctx.antecedent prejacent ctx.resolvedQuestion ctx.prior) :

                                                      Theorem: Cumulative Evidence Necessity

                                                      If π is evidentially irrelevant to RQ given ANT (i.e., π doesn't change the probability of any alternative), then the conjunction condition fails, and "too" is infelicitous.

                                                      This explains WHY "too" requires the prejacent to contribute something: if π is just noise that doesn't affect the question at hand, it can't felicitously be marked with "too".

                                                      Example of failure:

                                                      • "Sue cooks, and she has brown hair, too."
                                                      • If hair color is independent of who should host the dinner party, this is infelicitous (or requires a different implicit QUD).
                                                      theorem Semantics.Lexical.Particle.Additive.irrelevant_prejacent_infelicitous {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (worlds : List W) (hIrrelevant : evidentiallyIrrelevant ctx.antecedent prejacent ctx.resolvedQuestion ctx.prior) :
                                                      tooFelicitousWith ctx prejacent worlds = false

                                                      Corollary: If π is irrelevant, "too" is infelicitous.

                                                      This follows from cumulative_evidence_necessary plus the fact that conjunctionCondition is required for felicity.

                                                      theorem Semantics.Lexical.Particle.Additive.standard_use_felicitous {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (worlds : List W) (hAnt : antecedentCondition ctx = true) (hConj : conjunctionCondition ctx prejacent = true) (hNonTriv : nonTrivialityConditionWith prejacent (strengthenedResolutions' ctx prejacent) worlds = true) (hMax : maximalityCondition ctx prejacent (strengthenedResolutions' ctx prejacent) worlds = true) :
                                                      tooFelicitousWith ctx prejacent worlds = true

                                                      Standard use satisfies felicity when both ANT and π answer RQ.

                                                      In standard "too" use where ANT and π are both partial answers to the resolved question, the felicity conditions are satisfied.

                                                      Argument-building use is distinct from standard use.

                                                      If we have an argument-building use, the antecedent and prejacent are not focus alternatives.

                                                      theorem Semantics.Lexical.Particle.Additive.no_antecedent_infelicitous {W : Type u_1} [Fintype W] (ctx : AdditiveContext W) (prejacent : WBool) (worlds : List W) (hNoAnt : antecedentCondition ctx = false) :
                                                      tooFelicitousWith ctx prejacent worlds = false

                                                      If ANT alone doesn't answer RQ, "too" is infelicitous.

                                                      The antecedent must be established as relevant to the resolved question.