Additive Particle Data

@cite{heim-1992} @cite{kripke-2009} @cite{rooth-1992}

Empirical data on additive particles (too, also, either) and their felicity conditions.

Main definitions

• AdditiveParticleDatum: Data point for additive particle use
• FelicityJudgment: Acceptability ratings (ok/marginal/odd)
• UseType: Standard, argument-building, scalar, contrastive uses

inductive Phenomena.Focus.AdditiveParticles.FelicityJudgment : Type

Felicity judgment for additive particle examples.

• ok : FelicityJudgment
• marginal : FelicityJudgment
• odd : FelicityJudgment

instance Phenomena.Focus.AdditiveParticles.instDecidableEqFelicityJudgment : DecidableEq FelicityJudgment

Equations

• Phenomena.Focus.AdditiveParticles.instDecidableEqFelicityJudgment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Focus.AdditiveParticles.instReprFelicityJudgment.repr : FelicityJudgment → Nat → Std.Format

Equations

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

instance Phenomena.Focus.AdditiveParticles.instReprFelicityJudgment : Repr FelicityJudgment

Equations

• Phenomena.Focus.AdditiveParticles.instReprFelicityJudgment = { reprPrec := Phenomena.Focus.AdditiveParticles.instReprFelicityJudgment.repr }

instance Phenomena.Focus.AdditiveParticles.instBEqFelicityJudgment : BEq FelicityJudgment

Equations

• Phenomena.Focus.AdditiveParticles.instBEqFelicityJudgment = { beq := Phenomena.Focus.AdditiveParticles.instBEqFelicityJudgment.beq }

def Phenomena.Focus.AdditiveParticles.instBEqFelicityJudgment.beq : FelicityJudgment → FelicityJudgment → Bool

Equations

• Phenomena.Focus.AdditiveParticles.instBEqFelicityJudgment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.Focus.AdditiveParticles.UseType : Type

Type of additive particle use.

Binary classification following @cite{thomas-2026}: standard (focus-alternative) vs argument-building. Degree-"too" ("too expensive") is a distinct lexeme, not an additive particle use.

• standard : UseType
• argumentBuilding : UseType

instance Phenomena.Focus.AdditiveParticles.instDecidableEqUseType : DecidableEq UseType

Equations

• Phenomena.Focus.AdditiveParticles.instDecidableEqUseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Focus.AdditiveParticles.instReprUseType : Repr UseType

Equations

• Phenomena.Focus.AdditiveParticles.instReprUseType = { reprPrec := Phenomena.Focus.AdditiveParticles.instReprUseType.repr }

def Phenomena.Focus.AdditiveParticles.instReprUseType.repr : UseType → Nat → Std.Format

Equations

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

instance Phenomena.Focus.AdditiveParticles.instBEqUseType : BEq UseType

Equations

• Phenomena.Focus.AdditiveParticles.instBEqUseType = { beq := Phenomena.Focus.AdditiveParticles.instBEqUseType.beq }

def Phenomena.Focus.AdditiveParticles.instBEqUseType.beq : UseType → UseType → Bool

Equations

• Phenomena.Focus.AdditiveParticles.instBEqUseType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Focus.AdditiveParticles.AdditiveParticleDatum : Type

Empirical data point for additive particles.

• sentence : String
• antecedent : String
• prejacent : String
• particle : String
• resolvedQuestion : Option String
• felicity : FelicityJudgment
• useType : UseType
• notes : String
• source : String

def Phenomena.Focus.AdditiveParticles.instReprAdditiveParticleDatum.repr : AdditiveParticleDatum → Nat → Std.Format

Equations

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

instance Phenomena.Focus.AdditiveParticles.instReprAdditiveParticleDatum : Repr AdditiveParticleDatum

Equations

• Phenomena.Focus.AdditiveParticles.instReprAdditiveParticleDatum = { reprPrec := Phenomena.Focus.AdditiveParticles.instReprAdditiveParticleDatum.repr }

def Phenomena.Focus.AdditiveParticles.johnCameMaryToo : AdditiveParticleDatum

Classic "too" with focus alternatives.

Equations

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

def Phenomena.Focus.AdditiveParticles.maryAlsoCame : AdditiveParticleDatum

"Also" in medial position.

Equations

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

def Phenomena.Focus.AdditiveParticles.johnSingsJohnDancesToo : AdditiveParticleDatum

Same subject, different properties.

Equations

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

def Phenomena.Focus.AdditiveParticles.classicExamples : List AdditiveParticleDatum

Equations

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

def Phenomena.Focus.AdditiveParticles.missingAntecedent : AdditiveParticleDatum

Equations

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

def Phenomena.Focus.AdditiveParticles.irrelevantAntecedent : AdditiveParticleDatum

Antecedent doesn't answer RQ.

Equations

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

def Phenomena.Focus.AdditiveParticles.contextMismatch : AdditiveParticleDatum

Out-of-the-blue "too" with clear context mismatch.

Equations

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

def Phenomena.Focus.AdditiveParticles.infelicitousExamples : List AdditiveParticleDatum

Infelicitous examples.

Equations

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

def Phenomena.Focus.AdditiveParticles.eitherNegative : AdditiveParticleDatum

"Either" in negative context - felicitous.

Equations

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

def Phenomena.Focus.AdditiveParticles.eitherPositive : AdditiveParticleDatum

"Either" in positive context - infelicitous.

Equations

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

def Phenomena.Focus.AdditiveParticles.eitherWontCome : AdditiveParticleDatum

"Either" with negation scope.

Equations

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

def Phenomena.Focus.AdditiveParticles.eitherExamples : List AdditiveParticleDatum

Either examples.

Equations

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

structure Phenomena.Focus.AdditiveParticles.CrossLinguisticDatum : Type

A structure for cross-linguistic comparison data.

• language : String
• additiveParticle : String
• gloss : String
• notes : String

instance Phenomena.Focus.AdditiveParticles.instReprCrossLinguisticDatum : Repr CrossLinguisticDatum

Equations

• Phenomena.Focus.AdditiveParticles.instReprCrossLinguisticDatum = { reprPrec := Phenomena.Focus.AdditiveParticles.instReprCrossLinguisticDatum.repr }

def Phenomena.Focus.AdditiveParticles.instReprCrossLinguisticDatum.repr : CrossLinguisticDatum → Nat → Std.Format

Equations

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

def Phenomena.Focus.AdditiveParticles.germanAuch : CrossLinguisticDatum

German "auch".

Equations

• Phenomena.Focus.AdditiveParticles.germanAuch = { language := "German", additiveParticle := "auch", gloss := "also, too", notes := "Similar distribution to English 'too'/'also'" }

def Phenomena.Focus.AdditiveParticles.japaneseMo : CrossLinguisticDatum

Japanese "mo".

Equations

• Phenomena.Focus.AdditiveParticles.japaneseMo = { language := "Japanese", additiveParticle := "も (mo)", gloss := "also, too", notes := "Particle attached to NP; broader range of uses" }

def Phenomena.Focus.AdditiveParticles.dutchOok : CrossLinguisticDatum

Dutch "ook".

Equations

• Phenomena.Focus.AdditiveParticles.dutchOok = { language := "Dutch", additiveParticle := "ook", gloss := "also, too", notes := "Similar to German 'auch'" }

def Phenomena.Focus.AdditiveParticles.frenchAussi : CrossLinguisticDatum

French "aussi".

Equations

• Phenomena.Focus.AdditiveParticles.frenchAussi = { language := "French", additiveParticle := "aussi", gloss := "also, too", notes := "Typically sentence-medial or final" }

def Phenomena.Focus.AdditiveParticles.crossLinguisticData : List CrossLinguisticDatum

Equations

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

Rooth's Focus-Based Analysis

@cite{rooth-1992} §2.2 analyzes "too" via the Focus Interpretation Principle (FIP):

• The antecedent must be a focus alternative of the prejacent
• "Mary read Lear, and she read Macbeth too"
• Focus: MACBETH
• ⟦Macbeth⟧f = {Lear, Macbeth, Hamlet,...}
• Antecedent "Lear" ∈ ⟦Macbeth⟧f ✓

See Theories/Semantics/Focus/Interpretation.lean for formalization.

def Phenomena.Focus.AdditiveParticles.roothTooLear : AdditiveParticleDatum

Rooth's classic "too" example

Equations

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

def Phenomena.Focus.AdditiveParticles.roothTooSing : AdditiveParticleDatum

Rooth's example with verb focus

Equations

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

def Phenomena.Focus.AdditiveParticles.roothTooMary : AdditiveParticleDatum

Parallel subject focus

Equations

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

def Phenomena.Focus.AdditiveParticles.roothExamples : List AdditiveParticleDatum

Equations

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

def Phenomena.Focus.AdditiveParticles.allExamples : List AdditiveParticleDatum

All additive particle examples in this file. Note: Argument-building examples are in Studies/Thomas2026.lean Note: Ahn's "either" analysis is in Studies/Ahn2015.lean

Equations

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

def Phenomena.Focus.AdditiveParticles.felicitousCount : Nat

Count felicitous examples.

Equations

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

def Phenomena.Focus.AdditiveParticles.infelicitousCount : Nat

Count infelicitous examples.

Equations

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

def Phenomena.Focus.AdditiveParticles.totalCount : Nat

Total example count.

Equations

• Phenomena.Focus.AdditiveParticles.totalCount = Phenomena.Focus.AdditiveParticles.allExamples.length