Focus-sensitive particles: even and only

Traditional truth-conditional semantics for focus-sensitive particles (even, only), with NPI licensing derived from the scalar presupposition of even.

Main definitions

• FocusStructure α: alternative-semantics pair of an ordinary value and a list of alternatives.
• LikelihoodOrder W: relation on W → Bool predicates expressing context-dependent likelihood.
• TraditionalEven, TraditionalOnly: bundled semantics of even and only.
• EvenThreshold + evenPresupWith: existential / universal / most variants of the even scalar presupposition.
• npiLicensed: NPI licensing condition keyed on ContextPolarity.
• LikelihoodMonotone: monotonicity of a likelihood ordering with respect to entailment.

References

• [Lah98], [Crn14], [KP79], [Ben82], [Fra95], [Roo92].

structure Semantics.Focus.Particles.FocusStructure (α : Type u_3) : Type u_3

Alternative-semantics pair: an ordinary value plus a list of alternatives.

• ordinary : α

  The ordinary semantic value.

• alternatives : List α

  The focus alternatives.

def Semantics.Focus.Particles.LikelihoodOrder (World : Type u_3) : Type u_3

Context-dependent likelihood ordering on World → Bool predicates. lo a b holds when a is less likely (more surprising) than b.

Equations

• Semantics.Focus.Particles.LikelihoodOrder World = ((World → Bool) → (World → Bool) → Prop)

structure Semantics.Focus.Particles.TraditionalEven {World : Type u_1} : Type u_1

Traditional EVEN semantics

• prejacent : World → Bool

  The prejacent proposition

• alternatives : List (World → Bool)

  Focus alternatives

• likelihood : LikelihoodOrder World

  Likelihood ordering

def Semantics.Focus.Particles.TraditionalEven.assertion {World : Type u_1} (even : TraditionalEven) : World → Bool

EVEN asserts the prejacent

Equations

• even.assertion = even.prejacent

def Semantics.Focus.Particles.TraditionalEven.presupposition {World : Type u_1} (even : TraditionalEven) : Prop

EVEN presupposes prejacent is least likely. This is [KP79]'s universal threshold: the prejacent must be less likely than ALL alternatives. [Fra95] 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.Focus.Particles.TraditionalEven.defined {World : Type u_1} (even : TraditionalEven) : Prop

EVEN is defined (presupposition satisfied)

Equations

• even.defined = even.presupposition

def Semantics.Focus.Particles.TraditionalEven.trueAt {World : Type u_1} (even : TraditionalEven) (w : World) : Prop

Full EVEN meaning: defined and true

Equations

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

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

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

Equations

• Semantics.Focus.Particles.npiLicensed NaturalLogic.ContextPolarity.downward npiDomain regularDomain _hWider = True
• Semantics.Focus.Particles.npiLicensed NaturalLogic.ContextPolarity.upward npiDomain regularDomain _hWider = False
• Semantics.Focus.Particles.npiLicensed NaturalLogic.ContextPolarity.nonMonotonic npiDomain regularDomain _hWider = False

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

NPI licensed in DE contexts

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

NPI unlicensed in UE contexts

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

NPI unlicensed in non-monotonic contexts

structure Semantics.Focus.Particles.TraditionalOnly {World : Type u_1} : Type u_1

Traditional "only" semantics

• prejacent : World → Bool

  The prejacent (the focused element's contribution)

• alternatives : List (World → Bool)

  The alternatives (what focus evokes)

def Semantics.Focus.Particles.TraditionalOnly.presupposition {World : Type u_1} (only : TraditionalOnly) : World → Bool

"only" presupposes the prejacent

Equations

• only.presupposition = only.prejacent

def Semantics.Focus.Particles.TraditionalOnly.assertion {World : Type u_1} (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.Focus.Particles.TraditionalOnly.trueAt {World : Type u_1} (only : TraditionalOnly) (w : World) : Prop

Full "only" meaning

Equations

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

def Semantics.Focus.Particles.LikelihoodMonotone {W : Type u_3} (lessLikely : (W → Bool) → (W → Bool) → Prop) : Prop

A likelihood ordering is monotone with respect to entailment when a stronger proposition (true at fewer worlds) is less likely than a weaker one.

Equations

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

inductive Semantics.Focus.Particles.EvenThreshold : Type

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

• [Ben82]: at least one (too weak)

• 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.Focus.Particles.instDecidableEqEvenThreshold : DecidableEq EvenThreshold

Equations

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

def Semantics.Focus.Particles.instReprEvenThreshold.repr : EvenThreshold → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Focus.Particles.instReprEvenThreshold : Repr EvenThreshold

Equations

• Semantics.Focus.Particles.instReprEvenThreshold = { reprPrec := Semantics.Focus.Particles.instReprEvenThreshold.repr }

def Semantics.Focus.Particles.countExceeded {α : Type u_3} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] : ℕ

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

Equations

• Semantics.Focus.Particles.countExceeded prejacent alternatives moreSurprising = (List.filter (fun (a : α) => decide (moreSurprising prejacent a)) alternatives).length

def Semantics.Focus.Particles.evenPresupWith {α : Type u_3} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] (threshold : EvenThreshold) : Prop

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

Equations

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

@[implicit_reducible]

instance Semantics.Focus.Particles.instDecidableEvenPresupWith {α : Type u_3} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] (threshold : EvenThreshold) : Decidable (evenPresupWith prejacent alternatives moreSurprising threshold)

Equations

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