Longobardi (2001): How Comparative Is Semantics?

This file formalizes the parametric theory of bare nouns and proper names of [Lon01]. A nominal argument is either referential, a constant denoting through the lexical reference of its head, or quantificational, a variable bound by an existential or a generic operator (ArgumentType). A quantificational bare noun has the existential reading where the predicate is stage-level and the generic reading where the environment is characterizing, habitual aspect, an adverb of generality, or an eventive individual-level predicate, the tables (11) and (32), and nothing with a stative individual-level or a kind-level predicate (Environment, quantReadings); a referential bare noun is a kind name and generic everywhere (44). Romance bare nouns are only quantificational, English bare nouns may also be referential (44), which reduces to whether D carries strong referential features (DPParameter, bnReadings): Romance bare nouns read exactly as overt indefinites (romance_eq_indefinite, (5a)), are generic only in characterizing environments (romance_gen_iff, (5c)), and are existential exactly with stage-level predicates (ex_iff_stageLevel, (14a)), while English bare nouns are generic everywhere and the two languages differ exactly in the non-characterizing environments (english_gen, contrast_iff, (48)). Kind anaphora requires a kind-referring antecedent, so only English bare nouns and Romance definites license the species reading (species_iff, (22), (24), (37)). The syntax of proper names and the semantics of bare nouns are one parameter: object-referring nouns occur without a filled D exactly when kind-referring nouns can (typological_generalization, (56)), and a strong D whose adjectives are opaque to N-raising forces an article on every proper name, the Greek prediction (61), (65) (pnRequiresArticle_greek). The rows of Data/Examples/Longobardi2001 are the paper's paradigms, and the readings they record are the ones the parameter predicts (readings_predicted, definite_generic, species_rows, greek_names); the parameter also fixes the nominal mapping [Chi98] gives Romance and English (toNominalMapping, chierchia_mappings).

Implementation notes

The two parameters are Boolean coordinates of the paper's table (61), the Celtic setting of fn. 35 being the fourth cell. The Greek definite of (64b), ungrammatical on its generic reading in an episodic sentence, is recorded but not predicted, the paper's claim (40a) about definite generics in episodic sentences being made for Romance. Reading availability counts the paper's marginal readings as available.

References

• [Lon01]
• [Chi98]
• [Car77a]
• [GK87]

inductive Longobardi2001.ArgumentType : Type

The semantic type of a nominal argument: a constant denoting through the lexical reference of its head, or a variable bound by an existential or generic operator.

• referential : ArgumentType
• quantificational : ArgumentType

@[instance_reducible]

instance Longobardi2001.instDecidableEqArgumentType : DecidableEq ArgumentType

Equations

• Longobardi2001.instDecidableEqArgumentType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Longobardi2001.instReprArgumentType : Repr ArgumentType

Equations

• Longobardi2001.instReprArgumentType = { reprPrec := Longobardi2001.instReprArgumentType.repr }

def Longobardi2001.instReprArgumentType.repr : ArgumentType → ℕ → Std.Format

Equations

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

structure Longobardi2001.DPParameter : Type

The parameters of table (61): whether D carries strong referential features, and whether the constituent between D and N is transparent to N-raising.

• strongD : Bool
• transparentAlpha : Bool

@[instance_reducible]

instance Longobardi2001.instDecidableEqDPParameter : DecidableEq DPParameter

Equations

• Longobardi2001.instDecidableEqDPParameter = Longobardi2001.instDecidableEqDPParameter.decEq

def Longobardi2001.instDecidableEqDPParameter.decEq (x✝ x✝¹ : DPParameter) : Decidable (x✝ = x✝¹)

Equations

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

def Longobardi2001.instReprDPParameter.repr : DPParameter → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Longobardi2001.instReprDPParameter : Repr DPParameter

Equations

• Longobardi2001.instReprDPParameter = { reprPrec := Longobardi2001.instReprDPParameter.repr }

def Longobardi2001.romance : DPParameter

Romance: strong D, transparent α.

Equations

• Longobardi2001.romance = { strongD := true, transparentAlpha := true }

def Longobardi2001.english : DPParameter

English: weak D, opaque α.

Equations

• Longobardi2001.english = { strongD := false, transparentAlpha := false }

def Longobardi2001.greek : DPParameter

Greek: strong D, opaque α, the intermediate case of (61).

Equations

• Longobardi2001.greek = { strongD := true, transparentAlpha := false }

def Longobardi2001.celtic : DPParameter

Celtic: weak D, transparent α, the other intermediate case (fn. 35).

Equations

• Longobardi2001.celtic = { strongD := false, transparentAlpha := true }

def Longobardi2001.BnCanBeReferential (dp : DPParameter) : Prop

Bare nouns may be referential, kind names, exactly when D is weak (44).

Equations

• Longobardi2001.BnCanBeReferential dp = (dp.strongD = false)

def Longobardi2001.PnRequiresOvertD (dp : DPParameter) : Prop

Proper names need a phonetically filled D, by raising or an expletive article, exactly when D is strong (55).

Equations

• Longobardi2001.PnRequiresOvertD dp = (dp.strongD = true)

def Longobardi2001.PnRequiresArticle (dp : DPParameter) : Prop

Proper names need an overt article when D is strong and N cannot raise to it.

Equations

• Longobardi2001.PnRequiresArticle dp = (dp.strongD = true ∧ dp.transparentAlpha = false)

@[instance_reducible]

instance Longobardi2001.instDecidablePredDPParameterBnCanBeReferential : DecidablePred BnCanBeReferential

Equations

• Longobardi2001.instDecidablePredDPParameterBnCanBeReferential x✝ = Longobardi2001.instDecidablePredDPParameterBnCanBeReferential._aux_1 x✝

@[instance_reducible]

instance Longobardi2001.instDecidablePredDPParameterPnRequiresOvertD : DecidablePred PnRequiresOvertD

Equations

• Longobardi2001.instDecidablePredDPParameterPnRequiresOvertD x✝ = Longobardi2001.instDecidablePredDPParameterPnRequiresOvertD._aux_1 x✝

@[instance_reducible]

instance Longobardi2001.instDecidablePredDPParameterPnRequiresArticle : DecidablePred PnRequiresArticle

Equations

• Longobardi2001.instDecidablePredDPParameterPnRequiresArticle x✝ = { decide := decide (x✝.strongD = true) && decide (x✝.transparentAlpha = false), reflects_decide := ⋯ }

def Longobardi2001.bnArgumentTypes (dp : DPParameter) : Finset ArgumentType

The argument types available to a bare noun.

Equations

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

theorem Longobardi2001.typological_generalization (dp : DPParameter) : ¬PnRequiresOvertD dp ↔ BnCanBeReferential dp

The typological generalization (56): object-referring nouns occur without a filled D exactly when kind-referring nouns can.

theorem Longobardi2001.pnRequiresArticle_greek : PnRequiresArticle greek ∧ ¬PnRequiresArticle romance ∧ ¬PnRequiresArticle english

The Greek prediction (65): strong D with opaque adjectives forces an article on proper names, which neither Romance, where the name raises, nor English, where D is weak, does.

Environments and readings

inductive Longobardi2001.Environment : Type

The environments of the paper's paradigms: an episodic stage-level predicate, habitual aspect, an adverb of generality, an eventive (class A) or a stative (class B) individual-level predicate, and a kind-level predicate.

• episodic : Environment
• habitual : Environment
• adverbial : Environment
• iLevelA : Environment
• iLevelB : Environment
• kindLevel : Environment

@[instance_reducible]

instance Longobardi2001.instDecidableEqEnvironment : DecidableEq Environment

Equations

• Longobardi2001.instDecidableEqEnvironment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Longobardi2001.instReprEnvironment : Repr Environment

Equations

• Longobardi2001.instReprEnvironment = { reprPrec := Longobardi2001.instReprEnvironment.repr }

def Longobardi2001.instReprEnvironment.repr : Environment → ℕ → Std.Format

Equations

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

def Longobardi2001.Environment.StageLevel : Environment → Prop

Whether the predicate is stage-level.

Equations

• Longobardi2001.Environment.episodic.StageLevel = True
• Longobardi2001.Environment.habitual.StageLevel = True
• Longobardi2001.Environment.adverbial.StageLevel = True
• x✝.StageLevel = False

def Longobardi2001.Environment.Characterizing : Environment → Prop

Whether the environment is characterizing, (32): habitual aspect, an adverb of generality, or an eventive individual-level predicate.

Equations

• Longobardi2001.Environment.habitual.Characterizing = True
• Longobardi2001.Environment.adverbial.Characterizing = True
• Longobardi2001.Environment.iLevelA.Characterizing = True
• x✝.Characterizing = False

@[instance_reducible]

instance Longobardi2001.instDecidablePredEnvironmentStageLevel : DecidablePred Environment.StageLevel

Equations

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

@[instance_reducible]

instance Longobardi2001.instDecidablePredEnvironmentCharacterizing : DecidablePred Environment.Characterizing

Equations

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

inductive Longobardi2001.Reading : Type

The existential and generic readings.

• ex : Reading
• gen : Reading

@[instance_reducible]

instance Longobardi2001.instDecidableEqReading : DecidableEq Reading

Equations

• Longobardi2001.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Longobardi2001.instReprReading : Repr Reading

Equations

• Longobardi2001.instReprReading = { reprPrec := Longobardi2001.instReprReading.repr }

def Longobardi2001.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

def Longobardi2001.quantReadings (e : Environment) : Finset Reading

The readings of a quantificational nominal, (11), (14) and (46): existential with a stage-level predicate, generic in a characterizing environment.

Equations

• Longobardi2001.quantReadings e = (if e.StageLevel then {Longobardi2001.Reading.ex} else ∅) ∪ if e.Characterizing then {Longobardi2001.Reading.gen} else ∅

def Longobardi2001.bnReadings (dp : DPParameter) (e : Environment) : Finset Reading

The readings of a bare noun under a parameter, (45) and (46): those of a variable, and the generic reading of a kind name wherever the noun may be referential.

Equations

• Longobardi2001.bnReadings dp e = Longobardi2001.quantReadings e ∪ if Longobardi2001.BnCanBeReferential dp then {Longobardi2001.Reading.gen} else ∅

theorem Longobardi2001.romance_eq_indefinite (e : Environment) : bnReadings romance e = quantReadings e

(5a): Romance bare nouns read exactly as overt indefinites in every environment.

theorem Longobardi2001.ex_iff_stageLevel (dp : DPParameter) (e : Environment) : Reading.ex ∈ bnReadings dp e ↔ e.StageLevel

(14a): a bare noun is existential exactly with a stage-level predicate, whatever the parameter.

theorem Longobardi2001.romance_gen_iff (e : Environment) : Reading.gen ∈ bnReadings romance e ↔ e.Characterizing

(5c): Romance bare nouns are generic only in characterizing environments.

theorem Longobardi2001.english_gen (e : Environment) : Reading.gen ∈ bnReadings english e

(48): English bare nouns are generic in every environment.

theorem Longobardi2001.contrast_iff (e : Environment) : bnReadings romance e ≠ bnReadings english e ↔ ¬e.Characterizing

The two languages' bare nouns differ exactly in the non-characterizing environments, the episodic, stative, and kind-level predicates of (48).

theorem Longobardi2001.greek_eq_romance (e : Environment) : bnReadings greek e = bnReadings romance e

Greek bare nouns read as Romance ones, (63).

def Longobardi2001.SpeciesReading (dp : DPParameter) : ArgumentType → Prop

The species reading of an anaphor, (22), (24), (37): available to a bare-noun antecedent exactly when the noun may be a kind name, and always to a definite.

Equations

• Longobardi2001.SpeciesReading dp Longobardi2001.ArgumentType.referential = True
• Longobardi2001.SpeciesReading dp Longobardi2001.ArgumentType.quantificational = Longobardi2001.BnCanBeReferential dp

@[instance_reducible]

instance Longobardi2001.instDecidablePredArgumentTypeSpeciesReading (dp : DPParameter) : DecidablePred (SpeciesReading dp)

Equations

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

theorem Longobardi2001.species_iff (dp : DPParameter) : (∃ t ∈ bnArgumentTypes dp, SpeciesReading dp t) ↔ BnCanBeReferential dp

A bare noun licenses the species reading exactly when it may be referential.

The paradigms

def Longobardi2001.paramOf (e : Datum) : Option DPParameter

The parameter of a row's language.

Equations

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

def Longobardi2001.environmentOf (e : Datum) : Option Environment

The environment a row records.

Equations

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

def Longobardi2001.Available (e : Datum) (name : String) : Prop

A reading the row records as available, the paper's marginal readings included.

Equations

• Longobardi2001.Available e name = ∃ r ∈ e.readings, r.1 = name ∧ (r.2 = Judgment.acceptable ∨ r.2 = Judgment.marginal)

@[instance_reducible]

instance Longobardi2001.instDecidableAvailable (e : Datum) (name : String) : Decidable (Available e name)

Equations

• Longobardi2001.instDecidableAvailable e name = List.decidableBEx (fun (r : String × Judgment) => r.1 = name ∧ (r.2 = Judgment.acceptable ∨ r.2 = Judgment.marginal)) e.readings

def Longobardi2001.predictedOf (e : Datum) : Option (Finset Reading)

The predicted readings of a bare-noun or overt-indefinite row.

Equations

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

theorem Longobardi2001.readings_predicted (e : Datum) : e ∈ Examples.all → ∀ p ∈ predictedOf e, (Available e "Ex" ↔ Reading.ex ∈ p) ∧ (Available e "Gen" ↔ Reading.gen ∈ p)

Every bare-noun and overt-indefinite row, Italian, English, and Greek, subject and object, records exactly the readings the parameter predicts.

theorem Longobardi2001.definite_generic (e : Datum) : e ∈ Examples.all → e.language = "ital1282" → e.feature? "nominal" = some "definite" → ∀ x ∈ environmentOf e, Available e "Gen"

(5d), (34) to (36): Italian definites are generic in every environment, kind-level and episodic included.

theorem Longobardi2001.species_rows (e : Datum) : e ∈ Examples.all → e.feature? "environment" = some "kindAnaphora" → ∀ dp ∈ paramOf e, Available e "species" ↔ e.feature? "nominal" = some "definite" ∨ e.feature? "nominal" = some "bareNoun" ∧ BnCanBeReferential dp

The anaphora rows (22), (24), (25) and (37): the species reading goes with a definite or with a bare noun of a weak-D language.

theorem Longobardi2001.greek_names (e : Datum) : e ∈ Examples.all → e.feature? "nominal" = some "properName" → e.feature? "article" = some "absent" → e.judgment = Judgment.ungrammatical

(65): a Greek proper name without its article is ungrammatical.

The nominal mapping

def Longobardi2001.toNominalMapping (dp : DPParameter) : Genericity.NominalMapping

The nominal mapping of [Chi98] the parameter determines: with strong D nouns are predicates needing D for argumenthood, with weak D they may be arguments on their own.

Equations

• Longobardi2001.toNominalMapping dp = if dp.strongD = true then Genericity.NominalMapping.predOnly else Genericity.NominalMapping.argAndPred

theorem Longobardi2001.chierchia_mappings : toNominalMapping romance = Chierchia1998.Language.italian.nominalMapping ∧ toNominalMapping english = Chierchia1998.Language.english.nominalMapping

The Romance and English parameters yield the mappings [Chi98] gives Italian and English.