[Ken15]: De-Fregean numerals — neo-Gricean derivation

[Ken15] [Sau04] [Nou10] [GN07] [FG12] [Fra11]

[Ken15] replaces the Horn scale ⟨1, 2, 3, …⟩ with a single lexically-grouped alternative set containing the bare numeral together with all of its surface modifications:

  ALT(n) = {bare n, more than n, fewer than n, at least n, at most n}

The point is anti-Horn-scale: there is no fixed scale direction. The asymmetric-entailment filter of [Sau04]'s primary-implicature operator does the work that a pre-categorized "lower" or "upper" scale would otherwise do. Asserting "at least n" makes only the lower-direction alternatives (bare n, more than n) asymmetrically stronger; the upper-direction alternatives (fewer than n, at most n) are not — they're disjoint or overlapping but not subsets — so they don't trigger primary implicatures. The Class A / Class B distinction (labels from [Nou10], which [Ken15] contests by replacing Nouwen's lexical bifurcation with one denotation + asymmetric entailment) falls out as a structural property of the modifier's relation:

• Class B (≥, ≤) — the bare numeral is asymmetrically stronger than the asserted form (and so is the strict modifier on the same side); two primary implicatures, hence ignorance.
• Class A (>, <) — no alternative in the full set is asymmetrically stronger than the asserted form; no primary implicature.

We formalize both routes:

• §2 derives the predictions symbolically via asymStrongerOn (the polymorphic primitive from Semantics/Entailment/AsymStronger.lean).
• §3 derives the same direction probabilistically through RSA L1.

§3 is our own integration contribution, not Kennedy's — Kennedy's paper discusses [Fra11]'s IBR as the probabilistic counterpart, not [FG12]-style RSA. The two routes are theoretically distinct: §2 follows Kennedy directly; §3 shows the same qualitative predictions emerge from a soft-max listener over the same alternative set and bare-numeral semantics.

The formalization consumes Numeral.Entry.denoteUnder from Semantics/Numerals/Basic.lean directly — there is no separate "Kennedy meaning" function (Kennedy's alternative set is which numeral words to consider, not what they mean).

Domain: cardinality 0–5 (Fin 6, wide enough that Class A "more than 3" needs w = 4 to be non-trivial).

@[reducible, inline]

abbrev Kennedy2015.KCard : Type

Cardinality worlds 0–5. We use Fin 6 directly: decide runs over the type-class-derived Fintype, and the six-element domain is wide enough that Class A "more than 3" needs w = 4 to be non-trivial.

Equations

• Kennedy2015.KCard = Fin 6

inductive Kennedy2015.KUtt : Type

Kennedy's alternative set members for n = 3. One enum unifying bare and all four modifications — Class A vs Class B is read off asymmetric-entailment, not from membership in a pre-split sublist. The RSA analysis lives in Kennedy2015PMF.

• bare3 : KUtt
• moreThan3 : KUtt
• fewerThan3 : KUtt
• atLeast3 : KUtt
• atMost3 : KUtt

@[implicit_reducible]

instance Kennedy2015.instDecidableEqKUtt : DecidableEq KUtt

Equations

• Kennedy2015.instDecidableEqKUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kennedy2015.instReprKUtt.repr : KUtt → ℕ → Std.Format

Equations

• Kennedy2015.instReprKUtt.repr Kennedy2015.KUtt.bare3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kennedy2015.KUtt.bare3")).group prec✝
• Kennedy2015.instReprKUtt.repr Kennedy2015.KUtt.moreThan3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kennedy2015.KUtt.moreThan3")).group prec✝
• Kennedy2015.instReprKUtt.repr Kennedy2015.KUtt.fewerThan3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kennedy2015.KUtt.fewerThan3")).group prec✝
• Kennedy2015.instReprKUtt.repr Kennedy2015.KUtt.atLeast3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kennedy2015.KUtt.atLeast3")).group prec✝
• Kennedy2015.instReprKUtt.repr Kennedy2015.KUtt.atMost3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kennedy2015.KUtt.atMost3")).group prec✝

@[implicit_reducible]

instance Kennedy2015.instReprKUtt : Repr KUtt

Equations

• Kennedy2015.instReprKUtt = { reprPrec := Kennedy2015.instReprKUtt.repr }

@[implicit_reducible]

instance Kennedy2015.instFintypeKUtt : Fintype KUtt

Equations

• Kennedy2015.instFintypeKUtt = { elems := { val := ↑Kennedy2015.KUtt.enumList, nodup := Kennedy2015.KUtt.enumList_nodup }, complete := Kennedy2015.instFintypeKUtt._proof_1 }

def Kennedy2015.KUtt.entry : KUtt → Numeral.Entry

The numeral word (Numeral.Entry) a Kennedy alternative is — all at argument 3, with their surface forms.

Equations

• Kennedy2015.KUtt.bare3.entry = { form := "three", comparison := Core.Order.Comparison.eq, argument := 3 }
• Kennedy2015.KUtt.moreThan3.entry = { form := "more than three", comparison := Core.Order.Comparison.gt, argument := 3 }
• Kennedy2015.KUtt.fewerThan3.entry = { form := "fewer than three", comparison := Core.Order.Comparison.lt, argument := 3 }
• Kennedy2015.KUtt.atLeast3.entry = { form := "at least three", comparison := Core.Order.Comparison.ge, argument := 3 }
• Kennedy2015.KUtt.atMost3.entry = { form := "at most three", comparison := Core.Order.Comparison.le, argument := 3 }

def Kennedy2015.kMean (u : KUtt) (w : KCard) : Prop

Prop-valued meaning of any Kennedy alternative under bilateral (exact) bare semantics — Numeral.Entry.denoteUnder with bare := bareMeaning.

Equations

• Kennedy2015.kMean u w = u.entry.denoteUnder Semantics.Numerals.bareMeaning ↑w

@[implicit_reducible]

noncomputable instance Kennedy2015.instDecidablePredKCardKMean (u : KUtt) : DecidablePred (kMean u)

Equations

• Kennedy2015.instDecidablePredKCardKMean u w = Kennedy2015.instDecidablePredKCardKMean._aux_1 u w

Sauerland's primary-implicature schema applied to Kennedy's single alternative set distinguishes Class A from Class B with no probability:

For asserted φ and alternative set ALT, the primary implicatures are {¬Kψ | ψ ∈ ALT, ψ asymmetrically entails φ over the speaker's worlds}.

Over the six-world domain, the meanings at n = 3 are:

Expr	True at
bare 3	{3}
more than 3	{4, 5}
fewer than 3	{0, 1, 2}
at least 3	{3, 4, 5}
at most 3	{0, 1, 2, 3}

Asserting "at least 3": bare 3 ⊊ at least 3 and more than 3 ⊊ at least 3 — both asymmetrically stronger. The upper-direction alternatives fewer than 3 and at most 3 are not subsets (the former is disjoint, the latter overlaps but extends below). So 2 primary implicatures fire.

Asserting "more than 3": bare 3 is disjoint (rules out subset relation in either direction); at least 3 is a weaker alternative (superset, not subset); at most 3 and fewer than 3 are also not subsets. So 0 primary implicatures fire — exactly Kennedy's Class A prediction.

The alternative set is Finset.univ : Finset KUtt (all 5 KUtt constructors); the world domain is Finset.univ : Finset KCard (Fin 6 via Fintype).

theorem Kennedy2015.classB_atLeast3_two_primary : {u : KUtt | Entailment.asymStrongerOn Finset.univ (kMean u) (kMean KUtt.atLeast3)}.card = 2

Class B (lower-bound) triggers two primary implicatures. Asserting "at least 3" makes both "bare 3" and "more than 3" asymmetrically stronger over the six-world domain; the upper-direction alternatives are not.

theorem Kennedy2015.classA_moreThan3_no_primary : {u : KUtt | Entailment.asymStrongerOn Finset.univ (kMean u) (kMean KUtt.moreThan3)}.card = 0

Class A (lower-bound) triggers no primary implicatures. Asserting "more than 3" makes no alternative in Kennedy's full set — neither bare-direction nor cross-direction — asymmetrically stronger.

theorem Kennedy2015.classB_atMost3_two_primary : {u : KUtt | Entailment.asymStrongerOn Finset.univ (kMean u) (kMean KUtt.atMost3)}.card = 2

Mirror image: Class B (upper-bound) triggers two primary implicatures.

theorem Kennedy2015.classA_fewerThan3_no_primary : {u : KUtt | Entailment.asymStrongerOn Finset.univ (kMean u) (kMean KUtt.fewerThan3)}.card = 0

Mirror image: Class A (upper-bound) triggers no primary implicatures.