Francescotti 1995 — the felicity condition of even

[Fra95] defends the Implicature Account of even against [Lyc91]'s quantifier approach and revises its felicity condition (§IV, p. 162): an even-sentence is felicitous iff its even-less core S* is more surprising than most of its true neighbors — pace [Ben82], for whom one true neighbor suffices, and [KP79], who require all.

EvenThreshold compares the three conditions on the paper's two counterexamples (§I, pp. 155–156); the characters and dialectic are the paper's, the surprise levels and extra classmates ours. The paper's further requirement that neighbors be contextually determined, true, and part of a more general truth with S* is held fixed as background. The gradient discussion (pp. 163–164) contributes the margin dimension (meanExcess) and the proportion dimension, threshold work done by the vagueness of "most".

The three threshold conditions

inductive Francescotti1995.EvenThreshold : Type

How many true neighbors S* must exceed in surprise for even to be felicitous: at least one ([Ben82], §I), all ([KP79]), or most ([Fra95] §IV, p. 162).

• existential : EvenThreshold

  S* more surprising than at least one true neighbor.

• universal : EvenThreshold

  S* more surprising than all true neighbors.

• most : EvenThreshold

  S* more surprising than most (a strict majority of the) true neighbors.

@[instance_reducible]

instance Francescotti1995.instDecidableEqEvenThreshold : DecidableEq EvenThreshold

Equations

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

def Francescotti1995.instReprEvenThreshold.repr : EvenThreshold → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Francescotti1995.instReprEvenThreshold : Repr EvenThreshold

Equations

• Francescotti1995.instReprEvenThreshold = { reprPrec := Francescotti1995.instReprEvenThreshold.repr }

def Francescotti1995.countExceeded {α : Type u_1} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] : ℕ

Number of alternatives the prejacent exceeds in surprise.

Equations

• Francescotti1995.countExceeded prejacent alternatives moreSurprising = List.countP (fun (a : α) => decide (moreSurprising prejacent a)) alternatives

def Francescotti1995.evenPresupWith {α : Type u_1} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] (threshold : EvenThreshold) : Prop

The even felicity condition, parameterized by threshold.

Equations

• One or more equations did not get rendered due to their size.
• Francescotti1995.evenPresupWith prejacent alternatives moreSurprising Francescotti1995.EvenThreshold.existential = (0 < Francescotti1995.countExceeded prejacent alternatives moreSurprising)

@[instance_reducible]

instance Francescotti1995.instDecidableEvenPresupWith {α : Type u_1} (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.

theorem Francescotti1995.evenPresupWith_existential_iff {α : Type u_1} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] : evenPresupWith prejacent alternatives moreSurprising EvenThreshold.existential ↔ ∃ a ∈ alternatives, moreSurprising prejacent a

The existential threshold is [Ben82]'s condition (iii).

theorem Francescotti1995.evenPresupWith_universal_iff {α : Type u_1} (prejacent : α) (alternatives : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] : evenPresupWith prejacent alternatives moreSurprising EvenThreshold.universal ↔ ∀ a ∈ alternatives, moreSurprising prejacent a

The universal threshold is [KP79]'s "least likely" condition.

theorem Francescotti1995.evenPresup_iff_universal {W : Type u_2} (r : Set W → Set W → Prop) [DecidableRel r] (p : Set W) (alts : List (Set W)) : Focus.Particles.evenPresup r p alts ↔ evenPresupWith p alts r EvenThreshold.universal

The universal threshold coincides with the traditional scalar presupposition of even (Focus.Particles.evenPresup).

The two counterexamples (§I, pp. 155–156)

structure Francescotti1995.EvenScenario : Type

A numeric even scenario: surprise levels for S* and its true neighbors (higher = more surprising), plus the reported felicity.

• prejacent : ℕ

  Surprise level of S*.

• neighbors : List ℕ

  Surprise levels of the contextually-determined true neighbors.

• felicitous : Bool

  Reported felicity of the even-sentence.

@[instance_reducible]

instance Francescotti1995.instReprEvenScenario : Repr EvenScenario

Equations

• Francescotti1995.instReprEvenScenario = { reprPrec := Francescotti1995.instReprEvenScenario.repr }

def Francescotti1995.instReprEvenScenario.repr : EvenScenario → ℕ → Std.Format

Equations

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

def Francescotti1995.Matches (t : EvenThreshold) (s : EvenScenario) : Prop

A threshold matches a scenario when its predicted felicity agrees with the reported judgment.

Equations

• Francescotti1995.Matches t s = (Francescotti1995.evenPresupWith s.prejacent s.neighbors (fun (x1 x2 : ℕ) => x1 > x2) t ↔ s.felicitous = true)

@[instance_reducible]

instance Francescotti1995.instDecidableMatches (t : EvenThreshold) (s : EvenScenario) : Decidable (Matches t s)

Equations

• Francescotti1995.instDecidableMatches t s = Francescotti1995.instDecidableMatches._aux_1 t s

def Francescotti1995.scenario1 : EvenScenario

The passing scenario ((5), p. 155): Albert, one of the best students, passes unsurprisingly (2), Marie the very best (1), and three weaker classmates pass surprisingly (5, 7, 8; the roster completion is ours). "Even Albert passed the exam" is infelicitous.

Equations

• Francescotti1995.scenario1 = { prejacent := 2, neighbors := [1, 5, 7, 8], felicitous := false }

def Francescotti1995.scenario2 : EvenScenario

The failing scenario ((1), p. 156): everyone fails; Albert's failure is very surprising (8), Marie's would be more so (9), the weaker classmates' are not (3, 2, 1). "Even Albert failed the exam" is felicitous.

Equations

• Francescotti1995.scenario2 = { prejacent := 8, neighbors := [9, 3, 2, 1], felicitous := true }

theorem Francescotti1995.bennett_too_weak : ¬Matches EvenThreshold.existential scenario1 ∧ Matches EvenThreshold.existential scenario2

The one-neighbor condition wrongly licenses "Even Albert passed the exam", though it gets the failing scenario right.

theorem Francescotti1995.karttunen_peters_too_strong : Matches EvenThreshold.universal scenario1 ∧ ¬Matches EvenThreshold.universal scenario2

The all-neighbors condition wrongly blocks "Even Albert failed the exam", since Marie is even less likely to fail.

theorem Francescotti1995.francescotti_correct : Matches EvenThreshold.most scenario1 ∧ Matches EvenThreshold.most scenario2

The most-threshold predicts both judgments correctly.

Gradient felicity (pp. 163–164)

Felicity varies in degree in two ways: by how much S* surpasses its neighbors in surprise, and by how many it surpasses — the latter is threshold work done by the vagueness of "most".

def Francescotti1995.meanExcess (s : EvenScenario) : ℚ

Mean surprise margin over the neighbors exceeded: the paper's first gradient dimension, rendered numerically.

Equations

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

def Francescotti1995.scenarioAndreFar : EvenScenario

Andre is by far the tallest ((21), pp. 163–164): "Even Andre cannot reach the top shelf" is very felicitous.

Equations

• Francescotti1995.scenarioAndreFar = { prejacent := 9, neighbors := [3, 4, 5, 2, 3], felicitous := true }

def Francescotti1995.scenarioAndreBarely : EvenScenario

Andre is tallest by only a small margin (p. 163): the sentence is still felicitous, but less so.

Equations

• Francescotti1995.scenarioAndreBarely = { prejacent := 6, neighbors := [5, 5, 4, 5, 5], felicitous := true }

theorem Francescotti1995.andre_margin : meanExcess scenarioAndreBarely < meanExcess scenarioAndreFar

Both Andre scenarios exceed every neighbor, but the by-far scenario does so by a larger mean margin.

def Francescotti1995.scenarioAndreHalf : EvenScenario

Andre is barely in the taller half of a half-tall, half-short reference class (p. 164): not taller than the majority, so the sentence is infelicitous.

Equations

• Francescotti1995.scenarioAndreHalf = { prejacent := 8, neighbors := [9, 9, 1, 1], felicitous := false }

theorem Francescotti1995.andre_half_infelicitous : Matches EvenThreshold.most scenarioAndreHalf

Exceeding exactly half the neighbors is not "most": the threshold correctly predicts infelicity.