structure Semantics.FocusParticles.FocusStructure (α : Type) : Type

Alternative semantics: focused element evokes alternatives

• ordinary : α

  The ordinary semantic value

• alternatives : List α

  The focus alternatives

Covert EVEN (@cite{crnic-2014}, building on @cite{lahiri-1998})

@cite{rooth-1992}

EVEN has two semantic contributions:

1. Scalar presupposition: The focused element is least likely among alternatives
2. Additive presupposition: At least one alternative is true (for "also" reading)
3. Assertion: The prejacent is true

For NPI licensing, only the scalar presupposition matters.

def Semantics.FocusParticles.LikelihoodOrder (World : Type) : Type

Likelihood ordering over propositions (context-dependent). likelihood a b holds when a is less likely (more surprising) than b.

Equations

• Semantics.FocusParticles.LikelihoodOrder World = ((World → Bool) → (World → Bool) → Prop)

structure Semantics.FocusParticles.TraditionalEven {World : Type} : Type

Traditional EVEN semantics

• prejacent : World → Bool

  The prejacent proposition

• alternatives : List (World → Bool)

  Focus alternatives

• likelihood : LikelihoodOrder World

  Likelihood ordering

def Semantics.FocusParticles.TraditionalEven.assertion {World : Type} (even : TraditionalEven) : World → Bool

EVEN asserts the prejacent

Equations

• even.assertion = even.prejacent

def Semantics.FocusParticles.TraditionalEven.presupposition {World : Type} (even : TraditionalEven) : Prop

EVEN presupposes prejacent is least likely. This is @cite{karttunen-peters-1979}'s universal threshold: the prejacent must be less likely than ALL alternatives. @cite{francescotti-1995} argues this is too strong — see EvenThreshold.most for the revised condition.

Equations

• even.presupposition = ∀ (alt : World → Bool), alt ∈ even.alternatives → even.likelihood even.prejacent alt

def Semantics.FocusParticles.TraditionalEven.defined {World : Type} (even : TraditionalEven) : Prop

EVEN is defined (presupposition satisfied)

Equations

• even.defined = even.presupposition

def Semantics.FocusParticles.TraditionalEven.trueAt {World : Type} (even : TraditionalEven) (w : World) : Prop

Full EVEN meaning: defined and true

Equations

• even.trueAt w = (even.defined ∧ even.prejacent w = true)

NPI Licensing Mechanism

The key insight: In DE contexts, wide-domain NPIs make the prejacent LESS likely, satisfying EVEN's presupposition.

"John didn't see anyone" = EVEN [John didn't see anyone] = Presupposes: For all x, P(John didn't see x) ≥ P(John didn't see anyone) = "Not seeing anyone" is less likely than "not seeing some particular person" = Presupposition SATISFIED (negation creates DE context)

"*John saw anyone" = EVEN [John saw anyone] = Presupposes: For all x, P(John saw x) ≥ P(John saw anyone) = "Seeing anyone" is MORE likely than seeing some particular person = Presupposition VIOLATED

def Semantics.FocusParticles.npiLicensed {Entity : Type} (pol : Core.NaturalLogic.ContextPolarity) (npiDomain regularDomain : Set Entity) (_hWider : regularDomain ⊆ npiDomain) : Prop

NPI licensing condition: EVEN presupposition must be satisfiable. Uses ContextPolarity from Core.NaturalLogic.

Equations

• Semantics.FocusParticles.npiLicensed Core.NaturalLogic.ContextPolarity.downward npiDomain regularDomain _hWider = True
• Semantics.FocusParticles.npiLicensed Core.NaturalLogic.ContextPolarity.upward npiDomain regularDomain _hWider = False
• Semantics.FocusParticles.npiLicensed Core.NaturalLogic.ContextPolarity.nonMonotonic npiDomain regularDomain _hWider = False

theorem Semantics.FocusParticles.npi_licensed_de {Entity : Type} (npiDomain regularDomain : Set Entity) (hWider : regularDomain ⊆ npiDomain) : npiLicensed Core.NaturalLogic.ContextPolarity.downward npiDomain regularDomain hWider = True

NPI licensed in DE contexts

theorem Semantics.FocusParticles.npi_unlicensed_ue {Entity : Type} (npiDomain regularDomain : Set Entity) (hWider : regularDomain ⊆ npiDomain) : npiLicensed Core.NaturalLogic.ContextPolarity.upward npiDomain regularDomain hWider = False

NPI unlicensed in UE contexts

theorem Semantics.FocusParticles.npi_unlicensed_nonmon {Entity : Type} (npiDomain regularDomain : Set Entity) (hWider : regularDomain ⊆ npiDomain) : npiLicensed Core.NaturalLogic.ContextPolarity.nonMonotonic npiDomain regularDomain hWider = False

NPI unlicensed in non-monotonic contexts

Overt "only"

"Only" is the overt counterpart of EXH:

• Presupposes: The prejacent is true
• Asserts: No stronger alternative is true

"Only John came" = Presupposes: John came = Asserts: No one other than John came

This is equivalent to EXH with the prejacent as a presupposition.

structure Semantics.FocusParticles.TraditionalOnly {World : Type} : Type

Traditional "only" semantics

• prejacent : World → Bool

  The prejacent (the focused element's contribution)

• alternatives : List (World → Bool)

  The alternatives (what focus evokes)

def Semantics.FocusParticles.TraditionalOnly.presupposition {World : Type} (only : TraditionalOnly) : World → Bool

"only" presupposes the prejacent

Equations

• only.presupposition = only.prejacent

def Semantics.FocusParticles.TraditionalOnly.assertion {World : Type} (only : TraditionalOnly) : World → Bool

"only" asserts no alternative is true. The alternatives list excludes the prejacent (Roothian focus alternatives minus the focused element's contribution).

Equations

• only.assertion w = only.alternatives.all fun (alt : World → Bool) => !alt w

def Semantics.FocusParticles.TraditionalOnly.trueAt {World : Type} (only : TraditionalOnly) (w : World) : Prop

Full "only" meaning

Equations

• only.trueAt w = (only.prejacent w = true ∧ only.assertion w = true)

def Semantics.FocusParticles.LikelihoodMonotone {W : Type} (lessLikely : (W → Bool) → (W → Bool) → Prop) : Prop

A likelihood ordering is MONOTONE w.r.t. entailment when stronger propositions (true in fewer worlds) are less likely.

If p entails q (i.e., p is true only at worlds where q is true), then lessLikely p q (p is at least as unlikely as q).

This is the bridge between Theories/Semantics/Entailment/ and focus particle semantics — the connection that @cite{lahiri-1998} relies on to derive NPI licensing from the cardinality scale.

Equations

• Semantics.FocusParticles.LikelihoodMonotone lessLikely = ∀ (p q : W → Bool), (∀ (w : W), p w = true → q w = true) → lessLikely p q

Focus Particle Comparison

Particle	Presupposition	Assertion	Polarity Effect
EVEN	Least likely	Prejacent	Licenses NPIs (DE)
EXH	None	Prejacent ∧ ¬alternatives	Scalar implicatures (UE)
only	Prejacent	¬alternatives	Explicit exhaustivity

Key Observations

1. EVEN and EXH are duals:

   • EVEN: active in DE contexts (licenses NPIs)
   • EXH: active in UE contexts (generates SIs)

2. Only is overt EXH:

   • Same semantic effect as covert EXH
   • But with prejacent as presupposition, not assertion

inductive Semantics.FocusParticles.EvenThreshold : Type

Threshold variants for the EVEN scalar presupposition. The theoretical dispute concerns how many alternatives the prejacent must exceed in unlikelihood:

• @cite{bennett-1982}: at least one (too weak)
• @cite{karttunen-peters-1979}: all (too strong)
• @cite{francescotti-1995}: most (correct)

• existential : EvenThreshold

  S* more surprising than at least one neighbor

• universal : EvenThreshold

  S* more surprising than all neighbors

• most : EvenThreshold

  S* more surprising than most neighbors

@[implicit_reducible]

instance Semantics.FocusParticles.instDecidableEqEvenThreshold : DecidableEq EvenThreshold

Equations

• Semantics.FocusParticles.instDecidableEqEvenThreshold x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.FocusParticles.instReprEvenThreshold.repr : EvenThreshold → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.FocusParticles.instReprEvenThreshold : Repr EvenThreshold

Equations

• Semantics.FocusParticles.instReprEvenThreshold = { reprPrec := Semantics.FocusParticles.instReprEvenThreshold.repr }

def Semantics.FocusParticles.countExceeded {α : Type} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Bool) : ℕ

Count of alternatives that the prejacent exceeds under a decidable ordering.

Equations

• Semantics.FocusParticles.countExceeded prejacent alternatives moreSurprising = (List.filter (moreSurprising prejacent) alternatives).length

def Semantics.FocusParticles.evenPresupWith {α : Type} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Bool) (threshold : EvenThreshold) : Bool

Generalized EVEN presupposition parameterized by threshold. moreSurprising a b returns true when a is more surprising (less likely) than b.

Equations

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