Thomas (2026): A probabilistic, question-based approach to additivity

[Tho26] [CGR18] [FG12]

Formalisation of [Tho26], which unifies the canonical additive use of too with a previously unstudied "argument-building" use by stating felicity in terms of Bayesian inquisitive answerhood. The substrate primitives (Answers, IsResolutionEvidencedBy, evidencesResolutionMore, IsRelevantTo) live in Semantics/Questions/Probabilistic.lean; this file encodes the felicity conditions of [Tho26] Def 64 and their abstract consequences.

Main definitions

• IsTooFelicitous — conditions (a)-(c) of [Tho26] Def 64: the antecedent and the conjunction each answer a relevant question, the conjunction answers it more strongly, and the prejacent is neither redundant nor replaceable by a weaker proposition.
• IsTooLicensedByDQ — the full Def 64: IsTooFelicitous plus the requirement that the relevant question be relevant to a discourse question.
• IsTooInfelicitous — too is predicted infelicitous when no relevant question licenses it.

Main statements

• IsTooFelicitous.antecedent_probOfSet_pos, IsTooFelicitous.conjunction_probOfSet_pos — felicity forces positive prior mass on the antecedent and on the conjunction.
• IsTooFelicitous.exists_strict_improvement — the conjunction is strictly better Bayesian evidence for its resolution than the antecedent alone.
• Witness.answers_discriminates — a concrete Fin-3 model in which Answers holds of informative evidence and fails of the trivial univ, exercising the raises_prob and dominates fields of the answerhood structure.
• too_acceptable_iff_def64_satisfied — over the paper's examples (Data/Examples/Thomas2026.json), a too row is acceptable iff the paper's Def 64 diagnosis is "satisfied"; the equation is uniform across the standard and argument-building uses, which is the paper's unification thesis.

Implementation notes

The relevant question RQ need not be a Current Question; [Tho26] §5.4.3 requires only that it be relevant to some discourse question, which IsTooLicensedByDQ captures via IsRelevantTo. The two prejacent conditions rule out the [BC08] ecstatic case (the prejacent already entails the answer) and the "some-instrument vs cello" case (a weaker prejacent would do); see the per-field docstrings of IsTooFelicitous.

TOO felicity

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

Conditions (a)-(c) of [Tho26] Def 64. The full Def 64 additionally requires the relevant question to be relevant to a discourse question; that is IsTooLicensedByDQ.

• antecedent_answers : Semantics.Questions.Probabilistic.Answers antecedent rq μ

  Def 64a: the antecedent answers the relevant question.

• conjunction_answers : Semantics.Questions.Probabilistic.Answers (antecedent ∩ prejacent) rq μ

  Def 64b (first half): the conjunction answers the relevant question.

• conjunction_stronger : ∃ (𝒜 : Set (Set W)), Semantics.Questions.Probabilistic.IsResolutionEvidencedBy rq 𝒜 (antecedent ∩ prejacent) μ ∧ Semantics.Questions.Probabilistic.evidencesResolutionMore μ 𝒜 (antecedent ∩ prejacent) antecedent

  Def 64b (second half): the conjunction evidences its resolution more strongly than the antecedent alone does.

• prejacent_not_entails (𝒜 : Set (Set W)) : Semantics.Questions.Probabilistic.IsResolutionEvidencedBy rq 𝒜 (antecedent ∩ prejacent) μ → ¬prejacent ⊆ ⋂₀ 𝒜

  Def 64c.i: the prejacent does not by itself entail the resolution the conjunction evidences (rules out the [BC08] ecstatic case "Sam is happy. #He's ecstatic, too").

• prejacent_minimal (S : Set W) : prejacent ⊆ S → S ≠ prejacent → ∀ (𝒜 : Set (Set W)), Semantics.Questions.Probabilistic.IsResolutionEvidencedBy rq 𝒜 (antecedent ∩ prejacent) μ → Semantics.Questions.Probabilistic.evidencesResolutionMore μ 𝒜 (antecedent ∩ prejacent) (antecedent ∩ S)

  Def 64c.ii: no proper weakening S ⊋ prejacent licenses the same resolution as well as the prejacent does (rules out the "some-instrument vs cello" case).

Abstract consequences

theorem Thomas2026.IsTooFelicitous.antecedent_probOfSet_pos {W : Type u_1} {μ : PMF W} {prejacent antecedent : Set W} {rq : 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.

theorem Thomas2026.IsTooFelicitous.conjunction_probOfSet_pos {W : Type u_1} {μ : PMF W} {prejacent antecedent : Set W} {rq : 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.

theorem Thomas2026.IsTooFelicitous.exists_strict_improvement {W : Type u_1} {μ : PMF W} {prejacent antecedent : Set W} {rq : 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 [Tho26] §4.4 intuition that too marks a strict improvement). The witness 𝒜 from conjunction_stronger exhibits this; the inequality is evidencesResolutionMore unfolded.

RQ relevance to a discourse question

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

The full [Tho26] Def 64: IsTooFelicitous together with the requirement that rq be relevant to some discourse question dq. The RQ need not be a Current Question — §5.4.3 requires only relevance to a DQ.

Equations

• Thomas2026.IsTooLicensedByDQ prejacent antecedent rq dq μ = (Thomas2026.IsTooFelicitous prejacent antecedent rq μ ∧ Semantics.Questions.Probabilistic.IsRelevantTo rq dq μ)

Predicted infelicity

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

Too is predicted infelicitous for a given (prejacent, antecedent) when no relevant question satisfies the felicity conditions ([Tho26] §5.5).

Equations

• Thomas2026.IsTooInfelicitous prejacent antecedent μ = ∀ (rq : Question W), ¬Thomas2026.IsTooFelicitous prejacent antecedent rq μ

Data conformance

Each row of Data/Examples/Thomas2026.json records the paper's Def 64 diagnosis as a def64_status feature: satisfied, or the condition the paper identifies as failing (antecedent_violation for (3), conjunction_violation for (72)/(19c), prejacent_violation_i for (11), prejacent_violation_ii for (30)). The either row carries no diagnosis — fn. 9 leaves either to future work — so the transfer equation is stated for too rows only.

theorem Thomas2026.too_acceptable_iff_def64_satisfied (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.feature? "particle" = some "too" → (row.judgment = Features.Judgment.acceptable ↔ row.feature? "def64_status" = some "satisfied")

Transfer equation: a too row is acceptable iff the paper exhibits an (ANT, RQ) pair satisfying all of Def 64. Uniform across the standard and argument-building rows — [Tho26]'s unification thesis.

Worked witness

A concrete model showing the answerhood structure underlying TOO felicity is satisfiable and discriminating. Over W = Fin 3 with the uniform prior, the evidence R = {1} answers the two-alternative question Q (alternatives A = {0,1} and B = {2}) via the singleton resolution {A}, while the trivial evidence Set.univ answers nothing. This instantiates the raises_prob and dominates fields that the abstract IsTooFelicitous structure never forces a caller to exhibit.

@[reducible, inline]

abbrev Thomas2026.Witness.W : Type

Equations

• Thomas2026.Witness.W = Fin 3

@[reducible, inline]

abbrev Thomas2026.Witness.A : Set W

Equations

• Thomas2026.Witness.A = {0, 1}

@[reducible, inline]

abbrev Thomas2026.Witness.B : Set W

Equations

• Thomas2026.Witness.B = {2}

@[reducible, inline]

abbrev Thomas2026.Witness.R : Set W

Equations

• Thomas2026.Witness.R = {1}

noncomputable def Thomas2026.Witness.μ : PMF W

The uniform prior on Fin 3.

Equations

• Thomas2026.Witness.μ = PMF.ofFintype (fun (x : Thomas2026.Witness.W) => 3⁻¹) Thomas2026.Witness.μ._proof_2

def Thomas2026.Witness.Q : Question W

The relevant question: Avery invited Bailey? against Avery invited Cameron? — two incomparable alternatives A and B.

Equations

• Thomas2026.Witness.Q = Question.declarative Thomas2026.Witness.A ⊔ Question.declarative Thomas2026.Witness.B

theorem Thomas2026.Witness.hAnotB : ¬A ⊆ B

theorem Thomas2026.Witness.hBnotA : ¬B ⊆ A

theorem Thomas2026.Witness.hRA : R ⊆ A

theorem Thomas2026.Witness.hRcapB : R ∩ B = ∅

theorem Thomas2026.Witness.A_mem_altQ : A ∈ Q.alt

theorem Thomas2026.Witness.B_mem_altQ : B ∈ Q.alt

theorem Thomas2026.Witness.altQ_subset : Q.alt ⊆ {A, B}

theorem Thomas2026.Witness.altQ_eq : Q.alt = {A, B}

theorem Thomas2026.Witness.mu_apply (i : W) : μ i = 3⁻¹

theorem Thomas2026.Witness.probOfSet_R_pos : μ.probOfSet R > 0

theorem Thomas2026.Witness.probOfSet_A_lt_one : μ.probOfSet A < 1

theorem Thomas2026.Witness.hsel (A' : Set W) : A' ∈ Q.alt → A' ≠ A → R ∩ A' = ∅

theorem Thomas2026.Witness.answers_R : Semantics.Questions.Probabilistic.Answers R Q μ

Positive witness: R answers Q, via the singleton resolution {A}.

theorem Thomas2026.Witness.answers_discriminates : Semantics.Questions.Probabilistic.Answers R Q μ ∧ ¬Semantics.Questions.Probabilistic.Answers Set.univ Q μ

Discriminating contrast: Answers distinguishes the informative evidence R from the uninformative Set.univ.