inductive Phenomena.Generics.BareNames.ReadingStatus : Type

Reading availability judgment.

• ok : ReadingStatus
• marginal : ReadingStatus
• degraded : ReadingStatus

instance Phenomena.Generics.BareNames.instReprReadingStatus : Repr ReadingStatus

Equations

• Phenomena.Generics.BareNames.instReprReadingStatus = { reprPrec := Phenomena.Generics.BareNames.instReprReadingStatus.repr }

def Phenomena.Generics.BareNames.instReprReadingStatus.repr : ReadingStatus → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.BareNames.instDecidableEqReadingStatus : DecidableEq ReadingStatus

Equations

• Phenomena.Generics.BareNames.instDecidableEqReadingStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.BareNames.instBEqReadingStatus.beq : ReadingStatus → ReadingStatus → Bool

Equations

• Phenomena.Generics.BareNames.instBEqReadingStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.BareNames.instBEqReadingStatus : BEq ReadingStatus

Equations

• Phenomena.Generics.BareNames.instBEqReadingStatus = { beq := Phenomena.Generics.BareNames.instBEqReadingStatus.beq }

structure Phenomena.Generics.BareNames.ReadingDatum : Type

A datum recording whether token and generic readings are available.

• sentence : String
• tokenReading : ReadingStatus
• genericReading : ReadingStatus
• notes : String

def Phenomena.Generics.BareNames.instReprReadingDatum.repr : ReadingDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.BareNames.instReprReadingDatum : Repr ReadingDatum

Equations

• Phenomena.Generics.BareNames.instReprReadingDatum = { reprPrec := Phenomena.Generics.BareNames.instReprReadingDatum.repr }

inductive Phenomena.Generics.BareNames.SubjectType : Type

What kind of DP is the subject?

• bareName : SubjectType
• definiteCommon : SubjectType
• modifiedName : SubjectType
• barePlural : SubjectType
• quotedName : SubjectType

def Phenomena.Generics.BareNames.instReprSubjectType.repr : SubjectType → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.BareNames.instReprSubjectType : Repr SubjectType

Equations

• Phenomena.Generics.BareNames.instReprSubjectType = { reprPrec := Phenomena.Generics.BareNames.instReprSubjectType.repr }

instance Phenomena.Generics.BareNames.instDecidableEqSubjectType : DecidableEq SubjectType

Equations

• Phenomena.Generics.BareNames.instDecidableEqSubjectType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.BareNames.instBEqSubjectType.beq : SubjectType → SubjectType → Bool

Equations

• Phenomena.Generics.BareNames.instBEqSubjectType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.BareNames.instBEqSubjectType : BEq SubjectType

Equations

• Phenomena.Generics.BareNames.instBEqSubjectType = { beq := Phenomena.Generics.BareNames.instBEqSubjectType.beq }

inductive Phenomena.Generics.BareNames.GenericLicensor : Type

What licensing factor (if any) enables the generic reading?

• none : GenericLicensor
• qAdv : GenericLicensor
• locativeAdjunct : GenericLicensor
• adjectivalMod : GenericLicensor
• genericContext : GenericLicensor
• kindLevelPred : GenericLicensor

def Phenomena.Generics.BareNames.instReprGenericLicensor.repr : GenericLicensor → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.BareNames.instReprGenericLicensor : Repr GenericLicensor

Equations

• Phenomena.Generics.BareNames.instReprGenericLicensor = { reprPrec := Phenomena.Generics.BareNames.instReprGenericLicensor.repr }

instance Phenomena.Generics.BareNames.instDecidableEqGenericLicensor : DecidableEq GenericLicensor

Equations

• Phenomena.Generics.BareNames.instDecidableEqGenericLicensor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Generics.BareNames.instBEqGenericLicensor : BEq GenericLicensor

Equations

• Phenomena.Generics.BareNames.instBEqGenericLicensor = { beq := Phenomena.Generics.BareNames.instBEqGenericLicensor.beq }

def Phenomena.Generics.BareNames.instBEqGenericLicensor.beq : GenericLicensor → GenericLicensor → Bool

Equations

• Phenomena.Generics.BareNames.instBEqGenericLicensor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Generics.BareNames.BSNDatum : Type

Full datum with DP type and licensing information.

• sentence : String
• subjectType : SubjectType
• tokenReading : ReadingStatus
• genericReading : ReadingStatus
• licensor : GenericLicensor

instance Phenomena.Generics.BareNames.instReprBSNDatum : Repr BSNDatum

Equations

• Phenomena.Generics.BareNames.instReprBSNDatum = { reprPrec := Phenomena.Generics.BareNames.instReprBSNDatum.repr }

def Phenomena.Generics.BareNames.instReprBSNDatum.repr : BSNDatum → ℕ → Std.Format

Equations

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

def Phenomena.Generics.BareNames.ruth_common : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.ruth_dancer : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.the_tiger_striped : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.the_tiger_widespread : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.ruth_40 : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.ruth_typically_40 : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.rutgers_prof_40 : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.rutgers_prof_generally_40 : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.coke_bottle_narrow : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.coke_bottle_generally_narrow : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.leslie_english_woman : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.italian_andrea_male : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.german_andrea_female : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.ruth_good_grades : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.paul_falls_in_love : BSNDatum

Equations

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

structure Phenomena.Generics.BareNames.NonEntailmentDatum : Type

Generic readings are not upward-entailing. "The kangaroo rat arrived" ⊭ "A rodent arrived" (on generic reading) "Ruth arrived" ⊭ "A person whose name starts with r arrived"

• premise : String
• wouldBeConclusion : String
• entails : Bool

def Phenomena.Generics.BareNames.instReprNonEntailmentDatum.repr : NonEntailmentDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.BareNames.instReprNonEntailmentDatum : Repr NonEntailmentDatum

Equations

• Phenomena.Generics.BareNames.instReprNonEntailmentDatum = { reprPrec := Phenomena.Generics.BareNames.instReprNonEntailmentDatum.repr }

def Phenomena.Generics.BareNames.kangaroo_rat_not_ue : NonEntailmentDatum

Equations

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

def Phenomena.Generics.BareNames.dodo_extinct : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.tristan_extinct : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.john_became_common : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.quoted_tristan_extinct : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.quoted_john_common : BSNDatum

Equations

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

def Phenomena.Generics.BareNames.recalcitrancePattern : List BSNDatum

Generic recalcitrance: BSNs are harder to interpret generically than ordinary definite singulars, but it IS possible with licensing.

Equations

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

theorem Phenomena.Generics.BareNames.recalcitrance_without_licensor : ruth_dancer.genericReading = ReadingStatus.degraded

BSNs without licensing resist generics; with licensing they improve.

theorem Phenomena.Generics.BareNames.recalcitrance_with_licensor : ruth_good_grades.genericReading = ReadingStatus.ok

theorem Phenomena.Generics.BareNames.def_singular_no_licensor_needed : the_tiger_striped.genericReading = ReadingStatus.ok ∧ the_tiger_striped.licensor = GenericLicensor.none

Definite singulars don't need licensing for generic readings.

theorem Phenomena.Generics.BareNames.quotation_rescues_kind_level : tristan_extinct.genericReading = ReadingStatus.degraded ∧ quoted_tristan_extinct.genericReading = ReadingStatus.ok

Quotation rescues kind-level predicates for names.

structure Phenomena.Generics.BareNames.PredicativistParallel : Type

The predicativist claim: BSNs and definite common NPs have parallel structure. ⟦∅ Ruth⟧ = ⟦the⟧ [λx.x is called Ruth] ⟦the tiger⟧ = ⟦the⟧ [λx.x is a tiger] If this is right, they should pattern alike for genericity. The data shows they mostly do, modulo recalcitrance.

• bsnDatum : BSNDatum
• defDatum : BSNDatum
• genericParallel : Bool

  Do both allow the same generic reading status?

def Phenomena.Generics.BareNames.striped_parallel : PredicativistParallel

Equations

• Phenomena.Generics.BareNames.striped_parallel = { bsnDatum := Phenomena.Generics.BareNames.ruth_dancer, defDatum := Phenomena.Generics.BareNames.the_tiger_striped }

theorem Phenomena.Generics.BareNames.recalcitrance_breaks_parallel : striped_parallel.genericParallel = false

Not all parallels hold — this is the recalcitrance phenomenon.

def Phenomena.Generics.BareNames.kind_level_parallel : PredicativistParallel

Equations

• Phenomena.Generics.BareNames.kind_level_parallel = { bsnDatum := Phenomena.Generics.BareNames.quoted_tristan_extinct, defDatum := Phenomena.Generics.BareNames.dodo_extinct }

theorem Phenomena.Generics.BareNames.quotation_restores_parallel : kind_level_parallel.genericParallel = true

Quotation restores the parallel for kind-level predicates.