@cite{bylinina-nouwen-2020}: Lower-Bound Bare Numerals + RSA Derive Exact Readings

@cite{bylinina-nouwen-2020} @cite{horn-1972}

@cite{bylinina-nouwen-2020} survey the two camps on bare-numeral semantics: the lower-bound view (bare n = ≥n; @cite{horn-1972}) and the exact view (bare n = =n). Under the lower-bound camp, the exact reading must arise pragmatically. This study formalises that derivation: a standard L0→S1→L1 RSA cascade with bare numerals over a 0–3 cardinality domain strengthens "two" from ≥2 to peak at w=2, and analogously for "one".

The construction reuses atLeastMeaning from Theories/Semantics/Numerals/Basic.lean via a small finite domain wrapper (NCard, NUtt) suited to rsa_predict reification. The lbNuttMeaning_eq_atLeastMeaning grounding theorem witnesses that the inlined meaning is the same one defined there.

inductive BylininaNouwen2020.NCard : Type

Cardinality worlds 0–3 as a finite enum (suits rsa_predict).

• c0 : NCard
• c1 : NCard
• c2 : NCard
• c3 : NCard

@[implicit_reducible]

instance BylininaNouwen2020.instDecidableEqNCard : DecidableEq NCard

Equations

• BylininaNouwen2020.instDecidableEqNCard x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BylininaNouwen2020.instReprNCard : Repr NCard

Equations

• BylininaNouwen2020.instReprNCard = { reprPrec := BylininaNouwen2020.instReprNCard.repr }

def BylininaNouwen2020.instReprNCard.repr : NCard → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BylininaNouwen2020.instFintypeNCard : Fintype NCard

Equations

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

def BylininaNouwen2020.NCard.toNat : NCard → ℕ

Equations

• BylininaNouwen2020.NCard.c0.toNat = 0
• BylininaNouwen2020.NCard.c1.toNat = 1
• BylininaNouwen2020.NCard.c2.toNat = 2
• BylininaNouwen2020.NCard.c3.toNat = 3

inductive BylininaNouwen2020.NUtt : Type

Bare-numeral utterances under consideration.

• one : NUtt
• two : NUtt
• three : NUtt

@[implicit_reducible]

instance BylininaNouwen2020.instDecidableEqNUtt : DecidableEq NUtt

Equations

• BylininaNouwen2020.instDecidableEqNUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BylininaNouwen2020.instReprNUtt.repr : NUtt → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BylininaNouwen2020.instReprNUtt : Repr NUtt

Equations

• BylininaNouwen2020.instReprNUtt = { reprPrec := BylininaNouwen2020.instReprNUtt.repr }

@[implicit_reducible]

instance BylininaNouwen2020.instFintypeNUtt : Fintype NUtt

Equations

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

def BylininaNouwen2020.NUtt.toBareNumeral : NUtt → Semantics.Numerals.BareNumeral

Equations

• BylininaNouwen2020.NUtt.one.toBareNumeral = Semantics.Numerals.BareNumeral.one
• BylininaNouwen2020.NUtt.two.toBareNumeral = Semantics.Numerals.BareNumeral.two
• BylininaNouwen2020.NUtt.three.toBareNumeral = Semantics.Numerals.BareNumeral.three

def BylininaNouwen2020.lbNuttMeaning : NUtt → NCard → Bool

Lower-bound meaning inlined for reification: n ≥ k. Avoids the atLeastMeaning indirection that would defeat rsa_predict's definitional unfolder. The grounding theorem below shows it agrees with atLeastMeaning.

Equations

• BylininaNouwen2020.lbNuttMeaning BylininaNouwen2020.NUtt.one x✝ = decide (x✝.toNat ≥ 1)
• BylininaNouwen2020.lbNuttMeaning BylininaNouwen2020.NUtt.two x✝ = decide (x✝.toNat ≥ 2)
• BylininaNouwen2020.lbNuttMeaning BylininaNouwen2020.NUtt.three x✝ = decide (x✝.toNat ≥ 3)

theorem BylininaNouwen2020.lbNuttMeaning_eq_atLeastMeaning (u : NUtt) (w : NCard) : lbNuttMeaning u w = true ↔ Semantics.Numerals.atLeastMeaning u.toBareNumeral.toNat w.toNat

The inlined meaning agrees with atLeastMeaning from Numerals.Basic.

noncomputable def BylininaNouwen2020.lbNumeralCfg : RSA.RSAConfig NUtt NCard

Standard belief-based RSA over bare numerals with ≥ semantics: S1 rates worlds by L0^α (here α = 1). The cascade is what @cite{bylinina-nouwen-2020} call "scalar implicature in the lower-bound camp".

Equations

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

theorem BylininaNouwen2020.lb_rsa_strengthens_two : lbNumeralCfg.L1 NUtt.two NCard.c2 > lbNumeralCfg.L1 NUtt.two NCard.c3

Under lower-bound semantics, RSA strengthens "two" from ≥2 to the exact reading: L1 assigns more probability to w = 2 than w = 3.

theorem BylininaNouwen2020.lb_rsa_strengthens_one : lbNumeralCfg.L1 NUtt.one NCard.c1 > lbNumeralCfg.L1 NUtt.one NCard.c2

Same effect for "one": L1("one", w = 1) > L1("one", w = 2).

theorem BylininaNouwen2020.lb_three_peaked : lbNumeralCfg.L1 NUtt.three NCard.c3 > lbNumeralCfg.L1 NUtt.three NCard.c2

"Three" trivially peaks at w = 3 (the only ≥3-compatible world in the 0–3 range).