@cite{snyder-2026}: Number Word Polysemy Data

@cite{snyder-2026}

Key example sentences from @cite{snyder-2026} illustrating the nine semantic functions of number words. These examples motivate Polymorphic Contextualism: any adequate theory of number words must derive all nine uses from a single lexical entry.

The Core Data Pattern

Number words appear in at least nine syntactic/semantic configurations. The challenge is that no single semantic type (e, ⟨e,t⟩, or ⟨⟨e,t⟩,t⟩) directly generates all nine. Any theory must explain how the others arise.

structure Phenomena.Numerals.Snyder2026.NumberWordExample : Type

An example sentence exhibiting a semantic function of a number word.

• exNum : String

  Example number from the paper

• sentence : String

  The example sentence

• function : Semantics.Lexical.Numeral.Polysemy.SemanticFunction

  Which semantic function it exhibits

• acceptable : Bool

  Acceptability judgment

def Phenomena.Numerals.Snyder2026.instReprNumberWordExample.repr : NumberWordExample → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Snyder2026.instReprNumberWordExample : Repr NumberWordExample

Equations

• Phenomena.Numerals.Snyder2026.instReprNumberWordExample = { reprPrec := Phenomena.Numerals.Snyder2026.instReprNumberWordExample.repr }

def Phenomena.Numerals.Snyder2026.ex1a : NumberWordExample

(1a) Predicative: "Mars's moons are two (in number)."

Equations

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

def Phenomena.Numerals.Snyder2026.ex1b : NumberWordExample

(1b) Attributive: "Mars has two moons."

Equations

• Phenomena.Numerals.Snyder2026.ex1b = { exNum := "1b", sentence := "Mars has two moons", function := Semantics.Lexical.Numeral.Polysemy.SemanticFunction.attributive, acceptable := true }

def Phenomena.Numerals.Snyder2026.ex1c : NumberWordExample

(1c) Quantificational: "Two moons orbit Mars."

Equations

• Phenomena.Numerals.Snyder2026.ex1c = { exNum := "1c", sentence := "Two moons orbit Mars", function := Semantics.Lexical.Numeral.Polysemy.SemanticFunction.quantificational, acceptable := true }

def Phenomena.Numerals.Snyder2026.ex1d : NumberWordExample

(1d) Specificational: "The number of Mars's moons is two."

Equations

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

def Phenomena.Numerals.Snyder2026.ex1e : NumberWordExample

(1e) Numeral: "Two is a prime number."

Equations

• Phenomena.Numerals.Snyder2026.ex1e = { exNum := "1e", sentence := "Two is a prime number", function := Semantics.Lexical.Numeral.Polysemy.SemanticFunction.numeral, acceptable := true }

def Phenomena.Numerals.Snyder2026.ex1f : NumberWordExample

(1f) Close appositive: "The number two is even."

Equations

• Phenomena.Numerals.Snyder2026.ex1f = { exNum := "1f", sentence := "The number two is even", function := Semantics.Lexical.Numeral.Polysemy.SemanticFunction.closeAppositive, acceptable := true }

def Phenomena.Numerals.Snyder2026.coreExamples : List NumberWordExample

All six core examples from (1).

Equations

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

theorem Phenomena.Numerals.Snyder2026.core_examples_acceptable : (coreExamples.all fun (x : NumberWordExample) => x.acceptable) = true

All core examples are acceptable.

structure Phenomena.Numerals.Snyder2026.IdentificationDatum : Type

A truth-value judgment on a close appositive with a specific number system.

• exNum : String
• sentence : String
• truthValue : Bool

def Phenomena.Numerals.Snyder2026.instReprIdentificationDatum.repr : IdentificationDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Snyder2026.instReprIdentificationDatum : Repr IdentificationDatum

Equations

• Phenomena.Numerals.Snyder2026.instReprIdentificationDatum = { reprPrec := Phenomena.Numerals.Snyder2026.instReprIdentificationDatum.repr }

def Phenomena.Numerals.Snyder2026.ex20a : IdentificationDatum

(20a) "The von Neumann ordinal two is two-membered." — TRUE (von Neumann 2 = {∅, {∅}}, which has two members)

Equations

• Phenomena.Numerals.Snyder2026.ex20a = { exNum := "20a", sentence := "The von Neumann ordinal two is two-membered", truthValue := true }

def Phenomena.Numerals.Snyder2026.ex20b : IdentificationDatum

(20b) "The Zermelo ordinal two is two-membered." — FALSE (Zermelo 2 = {{∅}}, which has one member)

Equations

• Phenomena.Numerals.Snyder2026.ex20b = { exNum := "20b", sentence := "The Zermelo ordinal two is two-membered", truthValue := false }

theorem Phenomena.Numerals.Snyder2026.identification_jointly_coherent : ex20a.truthValue = true ∧ ex20b.truthValue = false

(20a) and (20b) are jointly coherent: speakers accept both without sensing contradiction. This is the Identification Problem — any theory treating 'two' as a rigid designator wrongly predicts incoherence.

def Phenomena.Numerals.Snyder2026.ex47d : NumberWordExample

(47d) "Two comes in several varieties." — acceptable. This requires 'two' to denote a kind with subkinds.

Equations

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

def Phenomena.Numerals.Snyder2026.ex47e : NumberWordExample

(47e) "Each kind of two belongs to a different number system." — acceptable.

Equations

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

def Phenomena.Numerals.Snyder2026.ex76g : NumberWordExample

(76g) "Two is next to a five on the board." — acceptable (token reference).

Equations

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

def Phenomena.Numerals.Snyder2026.ex76i : NumberWordExample

(76i) "Two comes in several varieties." — acceptable (kind reference).

Equations

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

def Phenomena.Numerals.Snyder2026.allExamples : List NumberWordExample

All nine semantic functions are attested in acceptable sentences.

Equations

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

theorem Phenomena.Numerals.Snyder2026.all_examples_acceptable : (allExamples.all fun (x : NumberWordExample) => x.acceptable) = true

theorem Phenomena.Numerals.Snyder2026.nine_functions_attested : allExamples.length = 9