Focus-sensitive particles: even and only

Truth-conditional semantics for the focus particles even and only, with propositions as Set World. Even's scalar presupposition ([KP79]) requires the prejacent to be less likely than every focus alternative; only's assertion ([Roo92]) excludes every alternative; and LikelihoodMonotone — a likelihood ordering respecting entailment — is the property from which [Lah98] derives the distribution of even one NPIs (cf. [Crn14]). [Fra95] weakens the presupposition's universal force to a majority threshold — see Studies/Francescotti1995.lean.

Main definitions

• evenPresup: the prejacent is less likely than every alternative.
• onlyAssertion: no focus alternative holds.
• LikelihoodMonotone: entailment-monotonicity of a likelihood ordering.

def Focus.Particles.evenPresup {World : Type u_1} (r : Set World → Set World → Prop) (p : Set World) (alts : List (Set World)) : Prop

The scalar presupposition of even ([KP79]): the prejacent p is less likely than every focus alternative, where r p q reads "p is less likely than q".

Equations

• Focus.Particles.evenPresup r p alts = ∀ (q : Set World), q ∈ alts → r p q

def Focus.Particles.onlyAssertion {World : Type u_1} (alts : List (Set World)) : Set World

The assertion of only: no focus alternative holds. The prejacent is presupposed separately; the alternative list excludes it.

Equations

• Focus.Particles.onlyAssertion alts = {w : World | ∀ (q : Set World), q ∈ alts → ¬w ∈ q}

def Focus.Particles.LikelihoodMonotone {World : Type u_1} (r : Set World → Set World → Prop) : Prop

A likelihood ordering respects entailment: a stronger proposition is at most as likely.

Equations

• Focus.Particles.LikelihoodMonotone r = ∀ ⦃p q : Set World⦄, p ⊆ q → r p q