Numeral Embedding Test Cases

@cite{bylinina-nouwen-2020} @cite{coppock-beaver-2014} @cite{gajewski-2007} @cite{horn-1972} @cite{kaufmann-2012} @cite{kennedy-2015} @cite{kiparsky-kiparsky-1970} @cite{meier-2003} @cite{musolino-2004} @cite{nouwen-2006} @cite{penka-2006} @cite{solt-waldon-2019}

Theory-neutral empirical test cases for bare numerals in embedding environments (negation, modals, attitudes, conditionals, DE contexts). These environments are where lower-bound and bilateral numeral theories diverge most sharply.

Key Diagnostic Environments

1. Negation: "John doesn't have three children" — LB predicts <3, BL predicts ≠3
2. Modals: "You must read three books" — □(≥3) vs □(=3)
3. "Exactly" redundancy: informative under LB, redundant under BL
4. Conditionals: "If you have three children..." — ≥3 vs =3 as trigger condition
5. Existential scope: embedded EXH blocked under existential quantifier

inductive Phenomena.Numerals.Embedding.EmbeddingType : Type

Type of embedding environment for numeral test cases.

• negation : EmbeddingType
• modal_possibility : EmbeddingType
• modal_necessity : EmbeddingType
• attitude : EmbeddingType
• conditional : EmbeddingType
• restrictor : EmbeddingType
• question : EmbeddingType
• existential_scope : EmbeddingType
• exactly_modification : EmbeddingType
• collective : EmbeddingType
• focus_only : EmbeddingType
• factive : EmbeddingType
• imperative : EmbeddingType
• neg_raising : EmbeddingType
• approximator : EmbeddingType
• degree : EmbeddingType
• convexity_test : EmbeddingType
• acquisition : EmbeddingType

def Phenomena.Numerals.Embedding.instReprEmbeddingType.repr : EmbeddingType → Nat → Std.Format

Equations

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

instance Phenomena.Numerals.Embedding.instReprEmbeddingType : Repr EmbeddingType

Equations

• Phenomena.Numerals.Embedding.instReprEmbeddingType = { reprPrec := Phenomena.Numerals.Embedding.instReprEmbeddingType.repr }

instance Phenomena.Numerals.Embedding.instDecidableEqEmbeddingType : DecidableEq EmbeddingType

Equations

• Phenomena.Numerals.Embedding.instDecidableEqEmbeddingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Numerals.Embedding.instBEqEmbeddingType : BEq EmbeddingType

Equations

• Phenomena.Numerals.Embedding.instBEqEmbeddingType = { beq := Phenomena.Numerals.Embedding.instBEqEmbeddingType.beq }

def Phenomena.Numerals.Embedding.instBEqEmbeddingType.beq : EmbeddingType → EmbeddingType → Bool

Equations

• Phenomena.Numerals.Embedding.instBEqEmbeddingType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Numerals.Embedding.NumeralEmbeddingDatum : Type

A theory-neutral test case for a numeral in an embedding environment.

Each datum records the sentence, what reading each theory predicts, and (when clear) which reading speakers prefer.

• sentence : String
• embedding : EmbeddingType
• numeral : Nat
• lowerBoundReading : String
• bilateralReading : String
• preferredReading : Option String
• source : String

def Phenomena.Numerals.Embedding.instReprNumeralEmbeddingDatum.repr : NumeralEmbeddingDatum → Nat → Std.Format

Equations

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

instance Phenomena.Numerals.Embedding.instReprNumeralEmbeddingDatum : Repr NumeralEmbeddingDatum

Equations

• Phenomena.Numerals.Embedding.instReprNumeralEmbeddingDatum = { reprPrec := Phenomena.Numerals.Embedding.instReprNumeralEmbeddingDatum.repr }

instance Phenomena.Numerals.Embedding.instBEqNumeralEmbeddingDatum : BEq NumeralEmbeddingDatum

Equations

• Phenomena.Numerals.Embedding.instBEqNumeralEmbeddingDatum = { beq := Phenomena.Numerals.Embedding.instBEqNumeralEmbeddingDatum.beq }

def Phenomena.Numerals.Embedding.instBEqNumeralEmbeddingDatum.beq : NumeralEmbeddingDatum → NumeralEmbeddingDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Numerals.Embedding.instBEqNumeralEmbeddingDatum.beq x✝¹ x✝ = false

def Phenomena.Numerals.Embedding.neg_plain : NumeralEmbeddingDatum

"John doesn't have three children" — the classic divergence case. LB: has fewer than 3. BL: doesn't have exactly 3 (could have more).

Equations

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

def Phenomena.Numerals.Embedding.neg_sentential : NumeralEmbeddingDatum

Sentential negation — same divergence, more formal register.

Equations

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

def Phenomena.Numerals.Embedding.neg_metalinguistic : NumeralEmbeddingDatum

Metalinguistic negation — supports only ≠3, not <3. "He doesn't have THREE children — he has four" is felicitous.

Equations

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

def Phenomena.Numerals.Embedding.modal_possibility_biscuit : NumeralEmbeddingDatum

"You are allowed to eat two biscuits" — modal possibility. Key interaction: EXH scope relative to modal.

Equations

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

def Phenomena.Numerals.Embedding.modal_necessity_books : NumeralEmbeddingDatum

"You must read three books" — modal necessity. Necessity quantifies universally over accessible worlds.

Equations

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

def Phenomena.Numerals.Embedding.exactly_children : NumeralEmbeddingDatum

"John has exactly three children" — redundancy test. Informative under LB (restricts ≥3 to =3), redundant under BL (=3 already).

Equations

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

def Phenomena.Numerals.Embedding.attitude_believe : NumeralEmbeddingDatum

"John believes there are three solutions" — attitude embedding.

Equations

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

def Phenomena.Numerals.Embedding.conditional_qualify : NumeralEmbeddingDatum

"If you have three children, you qualify for the tax credit" — numeral in conditional antecedent (downward-entailing context).

Equations

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

def Phenomena.Numerals.Embedding.restrictor_universal : NumeralEmbeddingDatum

"Every student who read three books passed" — numeral in restrictor of universal (downward-entailing).

Equations

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

def Phenomena.Numerals.Embedding.question_books : NumeralEmbeddingDatum

"Did John read three books?" — numeral in polar question.

Equations

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

def Phenomena.Numerals.Embedding.existential_some : NumeralEmbeddingDatum

"Some students answered three questions correctly" — numeral embedded under existential (@cite{bylinina-nouwen-2020} (38)–(39)). Embedded EXH is blocked in this environment under LB.

Equations

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

def Phenomena.Numerals.Embedding.collective_dots : NumeralEmbeddingDatum

"Twelve dots surround the square" — collective predicate. Collective reading requires the group to be exactly 12.

Equations

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

def Phenomena.Numerals.Embedding.almost_passed : NumeralEmbeddingDatum

"Almost three students passed" — the polar orientation diagnostic. "Almost" has a proximal component (close to p) and a polar component (¬p) (@cite{nouwen-2006}). Under LB, the polar component ¬(≥3) restricts to <3 (below only). Under BL, ¬(=3) admits values above AND below (2 or 4). The empirical asymmetry (below only) is argued by @cite{penka-2006} to favor LB. @cite{nouwen-2006} shows that polar orientation is in general context-dependent (e.g., "almost that warm" vs "almost that cold" orient in opposite directions).

Equations

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

def Phenomena.Numerals.Embedding.only_passed : NumeralEmbeddingDatum

"Only three students passed" — focus particle + numeral. Under LB, "only" is truth-conditionally informative (adds upper bound ≥3 → =3). Under BL, "only" is truth-conditionally redundant (=3 already exact) but contributes an evaluative scalar presupposition ("3 is low").

Equations

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

def Phenomena.Numerals.Embedding.factive_surprised : NumeralEmbeddingDatum

"I'm surprised that three students passed" — emotive factive. The numeral is under a factive presupposition trigger: LB presupposes ≥3 passed, BL presupposes =3 passed. If 5 passed, LB presupposition is satisfied but BL is violated.

Equations

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

def Phenomena.Numerals.Embedding.imperative_read : NumeralEmbeddingDatum

"Read three books!" — imperative compliance condition. Does reading 5 books comply with the command? Under LB: yes (5 ≥ 3). Under BL: no (5 ≠ 3).

Equations

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

def Phenomena.Numerals.Embedding.doubt_passed : NumeralEmbeddingDatum

"I doubt that three students passed" — neg-raising verb. "Doubt" ≈ "believe not" (neg-raising). Under LB: think ¬(≥3) = think <3 passed. Under BL: think ¬(=3) = think ≠3 (could think 5 passed).

Equations

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

def Phenomena.Numerals.Embedding.convexity_sheep : NumeralEmbeddingDatum

"She doesn't have 40 sheep" — QUD-convexity diagnostic. Infelicitous in neutral "how many?" context. Under LB: ¬(≥40) = {0.39}, a convex set → predicts felicitous (wrong). Under BL: ¬(=40) = {0.39, 41, 42,...}, non-convex → predicts infelicitous (correct).

Equations

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

def Phenomena.Numerals.Embedding.acquisition_horses : NumeralEmbeddingDatum

"Two of the horses jumped over the fence" — child interpretation. When 3 horses jumped, 5-year-olds reject "two horses jumped." Under LB: 3 ≥ 2, so should be accepted (children don't compute SI). Under BL: 3 ≠ 2, so should be rejected (exact reading is semantic). Children reject → supports BL.

Equations

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

def Phenomena.Numerals.Embedding.degree_too_many : NumeralEmbeddingDatum

"Three students is too many" — degree construction monotonicity. Under LB: ≥3 is too many → 4 is also too many (upward monotone). Under BL: =3 is too many → 4 being too many is NOT entailed.

Equations

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

def Phenomena.Numerals.Embedding.allData : List NumeralEmbeddingDatum

All embedding test cases.

Equations

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

theorem Phenomena.Numerals.Embedding.data_count : allData.length = 20

20 test cases covering 18 embedding types.

structure Phenomena.Numerals.Embedding.EmbeddingGeneralization : Type

A generalization about numeral behavior across embedding environments.

• name : String
• description : String

def Phenomena.Numerals.Embedding.instReprEmbeddingGeneralization.repr : EmbeddingGeneralization → Nat → Std.Format

Equations

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

instance Phenomena.Numerals.Embedding.instReprEmbeddingGeneralization : Repr EmbeddingGeneralization

Equations

• Phenomena.Numerals.Embedding.instReprEmbeddingGeneralization = { reprPrec := Phenomena.Numerals.Embedding.instReprEmbeddingGeneralization.repr }

instance Phenomena.Numerals.Embedding.instBEqEmbeddingGeneralization : BEq EmbeddingGeneralization

Equations

• Phenomena.Numerals.Embedding.instBEqEmbeddingGeneralization = { beq := Phenomena.Numerals.Embedding.instBEqEmbeddingGeneralization.beq }

def Phenomena.Numerals.Embedding.instBEqEmbeddingGeneralization.beq : EmbeddingGeneralization → EmbeddingGeneralization → Bool

Equations

• Phenomena.Numerals.Embedding.instBEqEmbeddingGeneralization.beq { name := a, description := a_1 } { name := b, description := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Numerals.Embedding.instBEqEmbeddingGeneralization.beq x✝¹ x✝ = false

def Phenomena.Numerals.Embedding.generalizations : List EmbeddingGeneralization

Key cross-cutting generalizations from the literature.

Equations

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