Gasparri (2025): Bare Singular Names and Genericity

This file formalizes [Gas25]'s reply to the argument that bare singular names, unlike the definite singulars predicativism equates them with ([Mat08b], [Far15]), never take generic readings ([Del24]). The paper's data show that they do, in simple generics as well as under quantificational adverbs, though more grudgingly than common-noun definites: out of the blue a bare name resists the generic reading, and a naming-convention context, a locative, a modifier or binding recovers it. Kind-level generics are the one case that stays closed to bare names and open to quoted ones, a gap common nouns share.

The rows are the paper's judgments and the theorems the generalizations it draws from them: recalcitrance against parity with definite singulars, bareName_simple_generic against the categorical ban. The paper's theoretical point, that a generic use calls for predicative content, is referentialist_generic_is_token: a referential name shifted to its identity property ([Par87]) and fed to the generic operator yields nothing but the token reading, so the shift a referentialist needs must introduce the naming predicate itself.

Implementation notes

• The generic operator is most over the restrictor, the proportional reading the paper's genericity diagnostics presuppose; the paper itself stays neutral on the semantics of Gen.
• A sentence the paper marks ?? without listing a reading is recorded with a questionable generic reading, the reading at issue; a reading the paper does not list is absent.

References

• [Gas25]
• [Par87]
• [Mat08b]
• [Far15]
• [Del24]

theorem Gasparri2025.referentialist_generic_is_token {E : Type} [Fintype E] [DecidableEq E] (j : E) (VP : E → Prop) : Quantifier.GQ.most (Quantifier.NP.ident j) VP ↔ VP j

A referential name shifted to its identity property and fed to the generic operator returns the token reading, so a generic use of a bare name needs the naming predicate.

The paper's judgments

inductive Gasparri2025.Subject : Type

The subject of a sentence, as the paper classifies it.

• bareName : Subject
• modifiedName : Subject
• pluralName : Subject
• quotedName : Subject
• definiteName : Subject
• definiteCommon : Subject
• modifiedCommon : Subject
• bareCommonPlural : Subject

@[instance_reducible]

instance Gasparri2025.instDecidableEqSubject : DecidableEq Subject

Equations

• Gasparri2025.instDecidableEqSubject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gasparri2025.instReprSubject : Repr Subject

Equations

• Gasparri2025.instReprSubject = { reprPrec := Gasparri2025.instReprSubject.repr }

def Gasparri2025.instReprSubject.repr : Subject → ℕ → Std.Format

Equations

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

inductive Gasparri2025.Context : Type

What the sentence is embedded in: nothing, a locative adjunct, a discourse about naming conventions, a binding quantifier, a discourse with kinds in focus, or a contrastive adjunct.

• outOfTheBlue : Context
• locative : Context
• naming : Context
• binding : Context
• focusedKinds : Context
• contrast : Context

@[instance_reducible]

instance Gasparri2025.instDecidableEqContext : DecidableEq Context

Equations

• Gasparri2025.instDecidableEqContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gasparri2025.instReprContext : Repr Context

Equations

• Gasparri2025.instReprContext = { reprPrec := Gasparri2025.instReprContext.repr }

def Gasparri2025.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

inductive Gasparri2025.Level : Type

Whether the predicate is characterizing or kind-level.

• characterizing : Level
• kindLevel : Level

@[instance_reducible]

instance Gasparri2025.instDecidableEqLevel : DecidableEq Level

Equations

• Gasparri2025.instDecidableEqLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gasparri2025.instReprLevel.repr : Level → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gasparri2025.instReprLevel : Repr Level

Equations

• Gasparri2025.instReprLevel = { reprPrec := Gasparri2025.instReprLevel.repr }

structure Gasparri2025.Row : Type

A sentence of the paper with the judgment of its generic reading, if the paper lists one.

• subject : Subject
• context : Context
• qadv : Bool
• level : Level
• generic : Option Judgment

@[instance_reducible]

instance Gasparri2025.instDecidableEqRow : DecidableEq Row

Equations

• Gasparri2025.instDecidableEqRow = Gasparri2025.instDecidableEqRow.decEq

def Gasparri2025.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def Gasparri2025.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gasparri2025.instReprRow : Repr Row

Equations

• Gasparri2025.instReprRow = { reprPrec := Gasparri2025.instReprRow.repr }

def Gasparri2025.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Gasparri2025.rows : List Row

Equations

• Gasparri2025.rows = List.filterMap Gasparri2025.Row.ofDatum Gasparri2025.Examples.all

theorem Gasparri2025.recalcitrance (r : Row) : r ∈ rows → r.subject = Subject.bareName → r.context = Context.outOfTheBlue → r.generic ≠ some Judgment.acceptable

Out of the blue, a bare name has no acceptable generic reading.

theorem Gasparri2025.definiteCommon_simple_generic : ∃ r ∈ rows, r.subject = Subject.definiteCommon ∧ r.context = Context.outOfTheBlue ∧ r.qadv = false ∧ r.generic = some Judgment.acceptable

The recalcitrance is specific to names: a common definite takes a simple generic reading out of the blue.

theorem Gasparri2025.bareName_simple_generic : ∃ r ∈ rows, r.subject = Subject.bareName ∧ r.qadv = false ∧ r.generic = some Judgment.acceptable

Against the ban on its narrow reading: a bare name in a simple generic.

theorem Gasparri2025.bareName_quantificational_generic : ∃ r ∈ rows, r.subject = Subject.bareName ∧ r.qadv = true ∧ r.generic = some Judgment.acceptable

Against the ban on its wide reading: a bare name under a quantificational adverb.

theorem Gasparri2025.bareName_kindLevel (r : Row) : r ∈ rows → r.subject = Subject.bareName → r.level = Level.kindLevel → r.generic ≠ some Judgment.acceptable

Kind-level generics stay closed to bare names.

theorem Gasparri2025.quotedName_kindLevel (r : Row) : r ∈ rows → r.subject = Subject.quotedName → r.level = Level.kindLevel → r.generic = some Judgment.acceptable

Kind-level generics are open to quoted names.

theorem Gasparri2025.definiteCommon_kindLevel_both : (∃ r ∈ rows, r.subject = Subject.definiteCommon ∧ r.level = Level.kindLevel ∧ r.generic = some Judgment.acceptable) ∧ ∃ r ∈ rows, r.subject = Subject.definiteCommon ∧ r.level = Level.kindLevel ∧ r.generic ≠ some Judgment.acceptable

Common definites go both ways in kind-level generics, so the gap is no discrepancy peculiar to names.