Francescotti (1995): Even: The Conventional Implicature Approach Reconsidered

This file formalizes [Fra95]'s felicity condition for even: the sentence without even must be more surprising than most of its contextually determined true neighbors, against [Ben82]'s one neighbor and [KP79]'s all. The three conditions are one threshold on the number of neighbors the prejacent surpasses (Meets); they are ordered (meets_most_of_universal, meets_existential_of_most), and the paper's two counterexamples are the two gaps between them: surpassing exactly one of several neighbors meets Bennett's condition but not the majority (not_meets_most_of_one), and surpassing all but one meets the majority but not Karttunen and Peters' (meets_most_of_all_but_one). The universal threshold is the scalar presupposition Focus.Particles.evenPresup.

Implementation notes

Neighbors are a list of alternatives with a surprise comparison, and the thresholds read the count of neighbors the prejacent surpasses, so the vagueness of most is the threshold itself; the paper's second gradient, the margin of surprise, is not formalized. The rows record the paper's scenarios by the counts its descriptions fix: how many neighbors the prejacent surpasses and how many there are.

References

• [Fra95]
• [Ben82]
• [KP79]
• [Kay90]
• [Lyc91]

inductive Francescotti1995.Threshold : Type

How many true neighbors the prejacent must surpass in surprise: at least one, all, or most.

• existential : Threshold
• universal : Threshold
• most : Threshold

@[instance_reducible]

instance Francescotti1995.instDecidableEqThreshold : DecidableEq Threshold

Equations

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

def Francescotti1995.instReprThreshold.repr : Threshold → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Francescotti1995.instReprThreshold : Repr Threshold

Equations

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

def Francescotti1995.Meets : Threshold → ℕ → ℕ → Prop

Surpassing k of n neighbors meets the threshold.

Equations

• Francescotti1995.Meets Francescotti1995.Threshold.existential x✝¹ x✝ = (0 < x✝¹)
• Francescotti1995.Meets Francescotti1995.Threshold.universal x✝¹ x✝ = (x✝¹ = x✝)
• Francescotti1995.Meets Francescotti1995.Threshold.most x✝¹ x✝ = (x✝ < 2 * x✝¹)

@[instance_reducible]

instance Francescotti1995.instDecidableMeets (t : Threshold) (k n : ℕ) : Decidable (Meets t k n)

Equations

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

theorem Francescotti1995.meets_most_of_universal {k n : ℕ} (hn : 0 < n) (h : Meets Threshold.universal k n) : Meets Threshold.most k n

All is most, when there are neighbors.

theorem Francescotti1995.meets_existential_of_most {k n : ℕ} (h : Meets Threshold.most k n) : Meets Threshold.existential k n

Most is at least one.

theorem Francescotti1995.not_meets_most_of_one {n : ℕ} (hn : 2 ≤ n) : Meets Threshold.existential 1 n ∧ ¬Meets Threshold.most 1 n

Bennett's counterexample: surpassing exactly one of several neighbors, as Albert's passing surpasses Marie's, meets the existential threshold but not the majority.

theorem Francescotti1995.meets_most_of_all_but_one {n : ℕ} (hn : 3 ≤ n) : Meets Threshold.most (n - 1) n ∧ ¬Meets Threshold.universal (n - 1) n

The failing scenario: surpassing all but one neighbor, everyone but Marie, meets the majority but not the universal threshold.

theorem Francescotti1995.not_meets_most_of_half {k : ℕ} : ¬Meets Threshold.most k (2 * k)

Exactly half is not most: Andre barely in the taller half.

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

The number of neighbors the prejacent surpasses in surprise.

Equations

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

def Francescotti1995.Felicitous {α : Type u_1} (prejacent : α) (neighbors : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] (t : Threshold) : Prop

The felicity condition at a threshold.

Equations

• Francescotti1995.Felicitous prejacent neighbors moreSurprising t = Francescotti1995.Meets t (Francescotti1995.surpassed prejacent neighbors moreSurprising) neighbors.length

theorem Francescotti1995.surpassed_le {α : Type u_1} (prejacent : α) (neighbors : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] : surpassed prejacent neighbors moreSurprising ≤ neighbors.length

theorem Francescotti1995.felicitous_existential_iff {α : Type u_1} (prejacent : α) (neighbors : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] : Felicitous prejacent neighbors moreSurprising Threshold.existential ↔ ∃ a ∈ neighbors, moreSurprising prejacent a

The existential threshold is Bennett's condition.

theorem Francescotti1995.felicitous_universal_iff {α : Type u_1} (prejacent : α) (neighbors : List α) (moreSurprising : α → α → Prop) [DecidableRel moreSurprising] : Felicitous prejacent neighbors moreSurprising Threshold.universal ↔ ∀ a ∈ neighbors, moreSurprising prejacent a

The universal threshold is Karttunen and Peters' condition.

theorem Francescotti1995.evenPresup_iff_universal {W : Type u_2} {α : Type u_3} [PartialOrder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (μ : Set W → α) (p : Set W) (alts : List (Set W)) : Focus.Particles.evenPresup μ p {q : Set W | q ∈ alts} ↔ Felicitous p alts (fun (x1 x2 : Set W) => μ x1 < μ x2) Threshold.universal

The universal threshold is the scalar presupposition of even.

The paper's scenarios

structure Francescotti1995.Row : Type

A scenario of the data: how many true neighbors the prejacent surpasses in surprise, how many there are, and whether the even-sentence is felicitous.

• surpassed : ℕ
• neighbors : ℕ
• felicitous : Bool

def Francescotti1995.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Francescotti1995.instDecidableEqRow : DecidableEq Row

Equations

• Francescotti1995.instDecidableEqRow = Francescotti1995.instDecidableEqRow.decEq

def Francescotti1995.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Francescotti1995.rows : List Row

Equations

• Francescotti1995.rows = List.filterMap Francescotti1995.Row.ofDatum Francescotti1995.Examples.all

theorem Francescotti1995.rows_most (r : Row) : r ∈ rows → (r.felicitous = true ↔ Meets Threshold.most r.surpassed r.neighbors)

The majority threshold fits every scenario.

theorem Francescotti1995.rows_not_existential : ¬∀ r ∈ rows, r.felicitous = true ↔ Meets Threshold.existential r.surpassed r.neighbors

Bennett's threshold does not: it licenses Even Albert passed the exam.

theorem Francescotti1995.rows_not_universal : ¬∀ r ∈ rows, r.felicitous = true ↔ Meets Threshold.universal r.surpassed r.neighbors

Karttunen and Peters' threshold does not: it blocks Even Albert failed the exam.