Documentation

Linglib.Theories.Semantics.Lexical.Numeral.Polysemy

Number Word Polysemy #

@cite{mendia-2020} @cite{snyder-2026}

Three polymorphic analyses of number words and their type-shifting maps.

Key Idea #

Polymorphic Contextualism: the lexical meaning of 'two' is an atomic predicate λx_a. two(x), applicable to different countable entities in different contexts. Kinds whose instantiations are numeral tokens. All other meanings derive via Partee type-shifting.

The Type-Shifting Map (Contextualism) #

  (numeral, kind-ref, token-ref)
        ↑ IOTA
  λx_a. two(x) ——CARD——→ (predicative) ——PM——→ (attributive)
                                   |                      |
                                  NOM A
                                   ↓ ↓
                           (specificational) (quantificational)

inductive Semantics.Lexical.Numeral.Polysemy.PolymorphicAnalysis :

The three polymorphic analyses of number words (Snyder §2, §5).

substantivalism : PolymorphicAnalysis
adjectivalism : PolymorphicAnalysis
contextualism : PolymorphicAnalysis

Instances For

instance Semantics.Lexical.Numeral.Polysemy.instDecidableEqPolymorphicAnalysis :

DecidableEq PolymorphicAnalysis

Equations

Semantics.Lexical.Numeral.Polysemy.instDecidableEqPolymorphicAnalysis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Numeral.Polysemy.instBEqPolymorphicAnalysis.beq :

PolymorphicAnalysis → PolymorphicAnalysis → Bool

Equations

Semantics.Lexical.Numeral.Polysemy.instBEqPolymorphicAnalysis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Lexical.Numeral.Polysemy.instBEqPolymorphicAnalysis :

BEq PolymorphicAnalysis

Equations

Semantics.Lexical.Numeral.Polysemy.instBEqPolymorphicAnalysis = { beq := Semantics.Lexical.Numeral.Polysemy.instBEqPolymorphicAnalysis.beq }

instance Semantics.Lexical.Numeral.Polysemy.instReprPolymorphicAnalysis :

Repr PolymorphicAnalysis

Equations

Semantics.Lexical.Numeral.Polysemy.instReprPolymorphicAnalysis = { reprPrec := Semantics.Lexical.Numeral.Polysemy.instReprPolymorphicAnalysis.repr }

def Semantics.Lexical.Numeral.Polysemy.instReprPolymorphicAnalysis.repr :

PolymorphicAnalysis → ℕ → Std.Format

Equations

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

Instances For

inductive Semantics.Lexical.Numeral.Polysemy.SemanticFunction :

Semantic functions of number words (Snyder (1a-f) + (76g-j)).

predicative : SemanticFunction
attributive : SemanticFunction
quantificational : SemanticFunction
specificational : SemanticFunction
numeral : SemanticFunction
closeAppositive : SemanticFunction
taxonomic : SemanticFunction
tokenRef : SemanticFunction
kindRef : SemanticFunction

Instances For

instance Semantics.Lexical.Numeral.Polysemy.instDecidableEqSemanticFunction :

DecidableEq SemanticFunction

Equations

Semantics.Lexical.Numeral.Polysemy.instDecidableEqSemanticFunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Numeral.Polysemy.instBEqSemanticFunction.beq :

SemanticFunction → SemanticFunction → Bool

Equations

Semantics.Lexical.Numeral.Polysemy.instBEqSemanticFunction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Lexical.Numeral.Polysemy.instBEqSemanticFunction :

BEq SemanticFunction

Equations

Semantics.Lexical.Numeral.Polysemy.instBEqSemanticFunction = { beq := Semantics.Lexical.Numeral.Polysemy.instBEqSemanticFunction.beq }

instance Semantics.Lexical.Numeral.Polysemy.instReprSemanticFunction :

Repr SemanticFunction

Equations

Semantics.Lexical.Numeral.Polysemy.instReprSemanticFunction = { reprPrec := Semantics.Lexical.Numeral.Polysemy.instReprSemanticFunction.repr }

def Semantics.Lexical.Numeral.Polysemy.instReprSemanticFunction.repr :

SemanticFunction → ℕ → Std.Format

Equations

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

Instances For

inductive Semantics.Lexical.Numeral.Polysemy.DerivationPath :

Which type-shifting path derives each semantic function under Contextualism. The lexical predicate λx_a.two(x) is the source for all.

cardFromPred : DerivationPath
pmFromCard : DerivationPath
aFromCard : DerivationPath
nomFromCard : DerivationPath
iotaFromPred : DerivationPath
iotaToken : DerivationPath
closeAppos : DerivationPath

Instances For

instance Semantics.Lexical.Numeral.Polysemy.instDecidableEqDerivationPath :

DecidableEq DerivationPath

Equations

Semantics.Lexical.Numeral.Polysemy.instDecidableEqDerivationPath x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Numeral.Polysemy.instBEqDerivationPath.beq :

DerivationPath → DerivationPath → Bool

Equations

Semantics.Lexical.Numeral.Polysemy.instBEqDerivationPath.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Lexical.Numeral.Polysemy.instBEqDerivationPath :

BEq DerivationPath

Equations

Semantics.Lexical.Numeral.Polysemy.instBEqDerivationPath = { beq := Semantics.Lexical.Numeral.Polysemy.instBEqDerivationPath.beq }

instance Semantics.Lexical.Numeral.Polysemy.instReprDerivationPath :

Repr DerivationPath

Equations

Semantics.Lexical.Numeral.Polysemy.instReprDerivationPath = { reprPrec := Semantics.Lexical.Numeral.Polysemy.instReprDerivationPath.repr }

def Semantics.Lexical.Numeral.Polysemy.instReprDerivationPath.repr :

DerivationPath → ℕ → Std.Format

Equations

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

Instances For

def Semantics.Lexical.Numeral.Polysemy.contextualistPath :

SemanticFunction → DerivationPath

Map from semantic function to derivation path under Contextualism.

Equations

Instances For

def Semantics.Lexical.Numeral.Polysemy.closeAppositive {m : Montague.Model} (domain : List m.Entity) (n1 n2 : m.interpTy Montague.Ty.et) :

Option (m.interpTy Montague.Ty.e)

Close appositive semantics: ⟦the N₁ N₂⟧ = ιx[N₁(x) ∧ N₂(x)] (Snyder §5.2, (16b)). N₁ functions as intersective modifier via IDENT, N₂ is the numeral predicate.

Equations

Semantics.Lexical.Numeral.Polysemy.closeAppositive domain n1 n2 = Semantics.Composition.TypeShifting.iota domain fun (x : m.interpTy Semantics.Montague.Ty.e) => n1 x && n2 x

Instances For

theorem Semantics.Lexical.Numeral.Polysemy.identification_problem_resolved (sys₁ sys₂ : Noun.Kind.Chierchia1998.MathSystem) :

sys₁ ≠ sys₂ → Noun.Kind.Chierchia1998.twoSubkinds sys₁ sys₂

The Identification Problem is resolved: close appositives are context-sensitive. "The von Neumann ordinal two" and "the Zermelo ordinal two" refer to different subkinds of TWO, so both can be true without contradiction (Snyder §5.2).

theorem Semantics.Lexical.Numeral.Polysemy.contextualism_total (sf : SemanticFunction) :

∃ (dp : DerivationPath), contextualistPath sf = dp

The contextualist derivation map is total: every semantic function has a derivation path. (This is trivially true because contextualistPath is a total function, but stating it explicitly documents the claim.)

All nine semantic functions are covered by Contextualism.

theorem Semantics.Lexical.Numeral.Polysemy.taxonomic_supported :

contextualistPath SemanticFunction.taxonomic = DerivationPath.iotaFromPred ∧ Noun.Kind.Chierchia1998.MathSystem.all.length ≥ 2

The taxonomic function is supported: MathSystem has multiple subkinds, so "two comes in several varieties" is predicted to be felicitous.