inductive NeoGricean.ImplicatureOperation : Type

Operations on scalar implicatures.

Following @cite{horn-1972}, speakers can:

• Assert/reinforce the implicature ("just two", "only two")
• Contradict/cancel the implicature ("not just two, but three")
• Suspend the implicature ("at least two", "two if not more")

• assert : ImplicatureOperation

  Assert the upper-bound implicature: "just/only n"

• contradict : ImplicatureOperation

  Contradict the implicature: "not just n, but more"

• suspend : ImplicatureOperation

  Suspend the implicature: "at least n", "n if not more"

instance NeoGricean.instDecidableEqImplicatureOperation : DecidableEq ImplicatureOperation

Equations

• NeoGricean.instDecidableEqImplicatureOperation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.instReprImplicatureOperation.repr : ImplicatureOperation → ℕ → Std.Format

Equations

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

instance NeoGricean.instReprImplicatureOperation : Repr ImplicatureOperation

Equations

• NeoGricean.instReprImplicatureOperation = { reprPrec := NeoGricean.instReprImplicatureOperation.repr }

instance NeoGricean.instToStringImplicatureOperation : ToString ImplicatureOperation

Equations

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

def NeoGricean.operationFelicitous (T : Semantics.Lexical.Numeral.NumeralTheory) (w : Semantics.Lexical.Numeral.BareNumeral) (_op : ImplicatureOperation) : Bool

An implicature operation is felicitous iff there IS an implicature to operate on.

For numerals, this means:

• The utterance must be ambiguous (compatible with multiple worlds)
• There must be a stronger alternative on the scale

Lower-bound semantics: Operations are felicitous (ambiguity exists) Exact semantics: Operations are infelicitous (no ambiguity)

Equations

• One or more equations did not get rendered due to their size.
• NeoGricean.operationFelicitous T Semantics.Lexical.Numeral.BareNumeral.five _op = (T.hasAmbiguity Semantics.Lexical.Numeral.BareNumeral.five && false)

def NeoGricean.hasImplicatureTarget (T : Semantics.Lexical.Numeral.NumeralTheory) (w : Semantics.Lexical.Numeral.BareNumeral) : Bool

Simplified check: is there an implicature to operate on?

Equations

• NeoGricean.hasImplicatureTarget T w = T.hasAmbiguity w

structure NeoGricean.OperationExamples : Type

Example sentences demonstrating the three operations on "two".

These follow Horn's pattern from (1.73):

• Assert: "just two" / "only two" / "two, not three"
• Contradict: "not just two, three" / "not two but three"
• Suspend: "at least two" / "two if not three" / "two or more"

• numeral : Semantics.Lexical.Numeral.BareNumeral
• assertExamples : List String
• contradictExamples : List String
• suspendExamples : List String

def NeoGricean.twoExamples : OperationExamples

Examples for "two" following @cite{horn-1972}

Equations

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

theorem NeoGricean.lowerBound_operations_felicitous : operationFelicitous Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.assert = true ∧ operationFelicitous Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.contradict = true ∧ operationFelicitous Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.suspend = true

Lower-bound predicts felicitous operations

Since "two" means ≥2, it's compatible with both 2 and 3. This ambiguity licenses implicature operations.

theorem NeoGricean.exact_operations_infelicitous : operationFelicitous Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.assert = false ∧ operationFelicitous Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.contradict = false ∧ operationFelicitous Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.suspend = false

Exact predicts infelicitous operations

Since "two" means =2, it's only compatible with world 2. No ambiguity → no implicature → nothing to operate on.

theorem NeoGricean.operation_felicity_differs : hasImplicatureTarget Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two = true ∧ hasImplicatureTarget Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two = false

The decisive contrast

The two theories make opposite predictions about whether "at least two" and "just two" are felicitous modifications.

Empirically, these ARE felicitous → supports Lower-bound.

def NeoGricean.suspensionNonRedundant (T : Semantics.Lexical.Numeral.NumeralTheory) (w : Semantics.Lexical.Numeral.BareNumeral) : Bool

Lower-bound suspension is non-redundant

"At least two" is informative because "two" alone means ≥2 but IMPLICATES =2. "At least" suspends the implicature.

In exact semantics, "at least two" would be contradictory or meaningless since "two" already means exactly 2.

Equations

• NeoGricean.suspensionNonRedundant T w = decide (T.compatibleCount w > 1)

theorem NeoGricean.lowerBound_suspension_nonRedundant : suspensionNonRedundant Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two = true

theorem NeoGricean.exact_suspension_redundant : suspensionNonRedundant Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two = false

def NeoGricean.reinforcementNonRedundant (T : Semantics.Lexical.Numeral.NumeralTheory) (w : Semantics.Lexical.Numeral.BareNumeral) : Bool

Reinforcement is ALWAYS non-redundant

"Just two" asserts what "two" only implicates. This is non-redundant precisely because the upper bound is implicated, not asserted.

Contrast with contradiction:

• "I have two children and I don't have all the children" (odd - "all" not implicated)
• "I have two children and I don't have three" (fine - "three" IS implicated)

Equations

• NeoGricean.reinforcementNonRedundant T w = T.hasAmbiguity w

theorem NeoGricean.lowerBound_reinforcement_nonRedundant : reinforcementNonRedundant Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two = true

theorem NeoGricean.exact_reinforcement_redundant : reinforcementNonRedundant Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two = false

structure NeoGricean.ConjunctionTest : Type

Conjunction Test for Implicature

Horn uses conjunction redundancy to distinguish implicature from assertion:

• "P and Q" is non-redundant if Q is merely implicated by P
• "P and Q" is redundant if Q is entailed by P

For numerals:

• "I have two children, in fact three" (fine - "not three" was implicated)
• "*I have two children, in fact one" (odd - "at least one" was asserted)

• base : Semantics.Lexical.Numeral.BareNumeral

  The base numeral

• continuation : Semantics.Lexical.Numeral.BareNumeral

  The continuation numeral

• felicitous : Bool

  Is "base, in fact continuation" felicitous?

def NeoGricean.upwardContinuation (T : Semantics.Lexical.Numeral.NumeralTheory) (base stronger : Semantics.Lexical.Numeral.BareNumeral) : Bool

Upward continuation is felicitous (cancels implicature).

Equations

• NeoGricean.upwardContinuation T base stronger = (T.meaning base stronger.toNat && T.isStrongerThan stronger base)

def NeoGricean.downwardContinuation (T : Semantics.Lexical.Numeral.NumeralTheory) (base weaker : Semantics.Lexical.Numeral.BareNumeral) : Bool

Downward continuation is infelicitous (contradicts assertion).

Equations

• NeoGricean.downwardContinuation T base weaker = (T.meaning base weaker.toNat && !T.isStrongerThan base weaker)

theorem NeoGricean.lowerBound_continuation_asymmetry : upwardContinuation Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two Semantics.Lexical.Numeral.BareNumeral.three = true ∧ downwardContinuation Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two Semantics.Lexical.Numeral.BareNumeral.one = false

Lower-bound predicts asymmetry

Upward continuation OK (cancels implicature). Downward continuation bad (contradicts lower bound).

theorem NeoGricean.operations_support_rsa_with_lowerBound : Semantics.Lexical.Numeral.LowerBound.hasAmbiguity Semantics.Lexical.Numeral.BareNumeral.two = true ∧ operationFelicitous Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.suspend = true ∧ Semantics.Lexical.Numeral.Exact.hasAmbiguity Semantics.Lexical.Numeral.BareNumeral.two = false ∧ operationFelicitous Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.suspend = false

Why Operations Matter for RSA

The felicity of implicature operations is evidence that:

1. The literal meaning is weak (compatible with multiple worlds)
2. RSA derives a stronger pragmatic meaning
3. Speakers can manipulate this pragmatic inference

This supports using Lower-bound semantics as the literal meaning in RSA models of numeral interpretation.

theorem NeoGricean.operations_summary : (operationFelicitous Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.assert = true ∧ operationFelicitous Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.contradict = true ∧ operationFelicitous Semantics.Lexical.Numeral.LowerBound Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.suspend = true) ∧ operationFelicitous Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.assert = false ∧ operationFelicitous Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.contradict = false ∧ operationFelicitous Semantics.Lexical.Numeral.Exact Semantics.Lexical.Numeral.BareNumeral.two ImplicatureOperation.suspend = false

Summary: Implicature Operations Distinguish the Theories

Operation	Lower-bound	Exact
Assert	Felicitous	Anomalous
Contradict	Felicitous	Anomalous
Suspend	Felicitous	Anomalous

The empirical fact that "just two", "at least two", and "not just two" are all felicitous supports the lower-bound analysis.