English Focus-Sensitive Particles

@cite{rooth-1992} @cite{karttunen-peters-1979} @cite{francescotti-1995}

Lexical entries for English focus-sensitive particles, typed by Semantics.FocusParticles theory types.

structure Fragments.English.FocusParticles.Entry : Type

A focus-sensitive particle lexical entry.

• form : String

  Surface form

• truthFunctional : Bool

  Does the particle affect truth conditions?

• contributionLayer : Core.Semantics.ContentLayer.ContentLayer

  Which content layer carries the particle's contribution

• threshold : Option Semantics.FocusParticles.EvenThreshold

  For scalar particles: threshold on alternatives exceeded

• application : Features.InformationStructure.FIPApplication

  FIP application type

• exclusionVariety : Option Core.Discourse.Coherence.CoherenceRelation

  Discourse-relation flavor of exclusion (@cite{umbach-2004}): only excludes additional alternatives → .contrast; contrastive focus excludes by substitution → .correction. Encoded directly as Core.Discourse.Coherence.CoherenceRelation (the IS-vocabulary "additional vs substitution" is recoverable from CONTRAST/CORRECTION per Umbach 2004's own decomposition). none for non-exclusive particles like even and also.

def Fragments.English.FocusParticles.instReprEntry.repr : Entry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.FocusParticles.instReprEntry : Repr Entry

Equations

• Fragments.English.FocusParticles.instReprEntry = { reprPrec := Fragments.English.FocusParticles.instReprEntry.repr }

@[implicit_reducible]

instance Fragments.English.FocusParticles.instBEqEntry : BEq Entry

Equations

• Fragments.English.FocusParticles.instBEqEntry = { beq := Fragments.English.FocusParticles.instBEqEntry.beq }

def Fragments.English.FocusParticles.instBEqEntry.beq : Entry → Entry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.FocusParticles.instBEqEntry.beq x✝¹ x✝ = false

def Fragments.English.FocusParticles.even_ : Entry

"even" — scalar focus particle. @cite{francescotti-1995}: not truth-functional (Equivalence Thesis), contributes via conventional implicature, felicity requires exceeding MOST alternatives in surprise.

Equations

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

def Fragments.English.FocusParticles.only_ : Entry

"only" — exclusive focus particle. Truth-functional (asserts exclusion of alternatives), prejacent is a presupposition. @cite{umbach-2004} §2.3: only excludes additional alternatives — it excludes the possibility that someone in addition to the focused item satisfies the predicate.

Equations

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

def Fragments.English.FocusParticles.also : Entry

"also"/"too" — additive focus particle. Presupposes existence of a true alternative.

Equations

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

def Fragments.English.FocusParticles.too_ : Entry

"too" — additive focus particle, sentence-final. @cite{thomas-2026}: felicity requires existence of an antecedent fact and a contextually relevant question RQ such that the Antecedent, Conjunction, and Prejacent Conditions (Def. 64) all hold. Subsumes @cite{heim-1992}'s individual-based presupposition as a special case of the standard focus-alternative use. Unlike sentence-initial "also", subject to the full Prejacent Condition including maximality (Def. 64c.ii).

Equations

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

def Fragments.English.FocusParticles.either_ : Entry

"either" — negative-polarity additive focus particle. @cite{rullmann-2003}: complementary distribution with "too" in polarity contexts. @cite{thomas-2026} defers full characterization to future work (footnote 9); felicity conditions likely share the core Antecedent/Conjunction structure with additional polarity constraints. See @cite{ahn-2015} for a Boolean algebra account.

Equations

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

def Fragments.English.FocusParticles.just_ : Entry

"just" — domain-widening focus particle. @cite{deo-thomas-2025}: just signals that the CQ is the widest answerable construal of an underspecified question. Unlike only, just does not conventionally encode exclusion — exhaustification arises as a mandatory Quantity implicature. Not truth-functional: the at-issue content is simply the prejacent. The CQ-signaling component is backgrounded (fn. 22 of the paper leaves the precise status as presupposition vs conventional implicature open for future research).

Equations

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

def Fragments.English.FocusParticles.allEntries : List Entry

Equations

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

theorem Fragments.English.FocusParticles.even_not_truth_functional : even_.truthFunctional = false

"even" does not affect truth conditions (Equivalence Thesis).

theorem Fragments.English.FocusParticles.even_is_implicature : even_.contributionLayer = Core.Semantics.ContentLayer.ContentLayer.implicature

"even" contributes via conventional implicature.

theorem Fragments.English.FocusParticles.even_uses_most_threshold : even_.threshold = some Semantics.FocusParticles.EvenThreshold.most

"even" uses Francescotti's "most" threshold.

theorem Fragments.English.FocusParticles.only_is_truth_functional : only_.truthFunctional = true

"only" IS truth-functional (unlike "even").

theorem Fragments.English.FocusParticles.even_only_differ_on_truth : even_.truthFunctional ≠ only_.truthFunctional

"even" and "only" differ on truth-functionality.

theorem Fragments.English.FocusParticles.only_excludes_additional : only_.exclusionVariety = some Core.Discourse.Coherence.CoherenceRelation.contrast

"only" is an exclusive particle: contrast (= "additional"-flavor) exclusion. @cite{umbach-2004} §2.3 (UNVERIFIED): excludes alternatives in addition to X, mapping to the CONTRAST discourse relation.

theorem Fragments.English.FocusParticles.also_not_exclusive : also.exclusionVariety = none

"also" is additive, not exclusive — no exclusion variety.

theorem Fragments.English.FocusParticles.even_not_exclusive : even_.exclusionVariety = none

"even" is scalar, not exclusive — no exclusion variety.

theorem Fragments.English.FocusParticles.too_not_truth_functional : too_.truthFunctional = false

"too" is additive, not truth-functional — like "also".

theorem Fragments.English.FocusParticles.too_is_presuppositional : too_.contributionLayer = Core.Semantics.ContentLayer.ContentLayer.presupposition

"too" contributes via presupposition.

theorem Fragments.English.FocusParticles.too_matches_also : too_.truthFunctional = also.truthFunctional ∧ too_.contributionLayer = also.contributionLayer ∧ too_.threshold = also.threshold

"too" and "also" have the same semantic profile.

theorem Fragments.English.FocusParticles.either_not_truth_functional : either_.truthFunctional = false

"either" is additive, not truth-functional.

theorem Fragments.English.FocusParticles.either_same_profile_as_too : either_.truthFunctional = too_.truthFunctional ∧ either_.contributionLayer = too_.contributionLayer

"either" and "too" differ only in form (and polarity, which is not captured in the Entry type — polarity licensing is in Theories.Pragmatics.Particles.Additive).

theorem Fragments.English.FocusParticles.just_not_truth_functional : just_.truthFunctional = false

"just" does not affect truth conditions (prejacent is the at-issue content).

theorem Fragments.English.FocusParticles.just_not_exclusive : just_.exclusionVariety = none

"just" is not an exclusive — no conventional exclusion. Exhaustification arises pragmatically via mandatory Quantity implicature (@cite{deo-thomas-2025} §4.1).

theorem Fragments.English.FocusParticles.just_only_differ : just_.truthFunctional ≠ only_.truthFunctional ∧ just_.exclusionVariety ≠ only_.exclusionVariety

"just" and "only" differ on truth-functionality and exclusion. This is the core of @cite{deo-thomas-2025}'s argument: just is not a variant of only — it has a fundamentally different discourse function. only conventionally excludes alternatives; just widens the question.

theorem Fragments.English.FocusParticles.just_even_same_truth_diff_layer : just_.truthFunctional = even_.truthFunctional ∧ just_.contributionLayer ≠ even_.contributionLayer

"just" and "even" are both non-truth-functional but differ in content layer. even contributes via conventional implicature (likelihood presupposition); just contributes via presupposition (CQ-signaling).