Documentation

Studies.Longobardi2005

Longobardi (2005): Toward a Unified Grammar of Reference #

This file formalizes [Lon05], which unifies the syntax of proper names and the semantics of bare nouns under one mapping theory. Access to N-to-D raising, the derivational route to object reference, is not bipolar but scalar: pronouns are always in D, proper names raise whenever D holds no lexical determiner, the names of days and casa and the kinship terms raise only under deixis or a genitive modifier, and ordinary common nouns never raise (25). Three tests rank the four classes of table (28): object reference in D, use as a predicative restriction outside D, and kind reference under the definite article, which no proper name has, la Maria being as rigid as Maria while il cane names a kind (26). Individuals are denoted in D and arguments denote individuals (52), (53), as constants, with one fixed referential value, or as variables ranging over a set (54), so an argument is a constant exactly when D holds a lexically referential expression, a raised noun, a pronoun, a demonstrative or an expletive article chained to the noun, and is otherwise a variable (55), (56), bound by the operator in D or unselectively when D is empty (59). A variable must range over a set and objects are not sets, so only a kind-naming noun restricts one: common nouns need not raise (57a), and by Last Resort (63) may not, while proper names, object-naming, must raise or take an expletive article, which answers (57b) and (57c). The article of a name is then obligatorily an expletive, whence the absence of a kind reading in (26b).

Implementation notes #

The scale of properness is the linear order of the four classes of (28), and each test is a map into the three-valued scale of access, never, under marked conditions, or always, so that the paper's "conditioned" cells are values rather than lost. N-to-D raising is the choice of referential content for an empty D, and Last Resort licenses it exactly when the nominal would otherwise fail to denote. The solo diagnostic of raising, the mass and plural morphology of kind naming (62), and the type-shifting of names under restrictive modification are not formalized.

References #

The properness hierarchy #

inductive Longobardi2005.HeadClass :

The four classes of nominal head of table (28), from the most prototypically proper-like: pronouns; proper names, the names of persons and places; the special common nouns, the names of days and casa and the kinship terms, which raise to D only under deixis or a genitive modifier; and ordinary common nouns.

pronoun : HeadClass
properName : HeadClass
specialCommon : HeadClass
commonNoun : HeadClass

Instances For

@[instance_reducible]

instance Longobardi2005.instDecidableEqHeadClass :

DecidableEq HeadClass

Equations

Longobardi2005.instDecidableEqHeadClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Longobardi2005.instReprHeadClass.repr :

HeadClass → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Longobardi2005.instReprHeadClass :

Equations

Longobardi2005.instReprHeadClass = { reprPrec := Longobardi2005.instReprHeadClass.repr }

def Longobardi2005.HeadClass.rank :

HeadClass → ℕ

Position on the scale of properness.

Equations

Instances For

theorem Longobardi2005.HeadClass.rank_injective :

Function.Injective rank

@[instance_reducible]

instance Longobardi2005.HeadClass.instLinearOrder :

LinearOrder HeadClass

The scale of properness, the two prototypes at its ends.

Equations

Longobardi2005.HeadClass.instLinearOrder = LinearOrder.lift' Longobardi2005.HeadClass.rank Longobardi2005.HeadClass.rank_injective

inductive Longobardi2005.Access :

How a class passes one of the three tests of (28), which is not at all, only under marked conditions, or freely.

never : Access
conditioned : Access
always : Access

Instances For

@[instance_reducible]

instance Longobardi2005.instDecidableEqAccess :

DecidableEq Access

Equations

Longobardi2005.instDecidableEqAccess x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Longobardi2005.instReprAccess.repr :

Access → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Longobardi2005.instReprAccess :

Equations

Longobardi2005.instReprAccess = { reprPrec := Longobardi2005.instReprAccess.repr }

def Longobardi2005.Access.rank :

Access → ℕ

Position on the scale of access.

Equations

Instances For

theorem Longobardi2005.Access.rank_injective :

Function.Injective rank

@[instance_reducible]

instance Longobardi2005.Access.instLinearOrder :

LinearOrder Access

Equations

Longobardi2005.Access.instLinearOrder = LinearOrder.lift' Longobardi2005.Access.rank Longobardi2005.Access.rank_injective

def Longobardi2005.HeadClass.objectReference :

HeadClass → Access

Object reference in D, the first column of (28), which the special common nouns achieve only with the identifying context of deixis or a genitive restriction and common nouns never do.

Equations

Instances For

def Longobardi2005.HeadClass.predicative :

HeadClass → Access

Use as a predicative restriction outside D, the second column of (28), which pronouns never have and proper names only under the marked conditions of restrictive modification.

Equations

Instances For

def Longobardi2005.HeadClass.kindReference :

HeadClass → Access

Kind reference under the definite article, the third column of (28) and the test of (26) and (27): no pronoun or proper name has it.

Equations

Instances For

theorem Longobardi2005.objectReference_antitone :

Antitone HeadClass.objectReference

Access to the raising strategy decreases along the scale of properness.

theorem Longobardi2005.predicative_monotone :

Monotone HeadClass.predicative

Predicative use increases along the scale.

theorem Longobardi2005.kindReference_monotone :

Monotone HeadClass.kindReference

Kind reference increases along the scale.

theorem Longobardi2005.kindReference_ne_never_iff (c : HeadClass) :

c.kindReference ≠ Access.never ↔ HeadClass.specialCommon ≤ c

The major divide runs between the proper names and the special common nouns: kind reference is available from the special common nouns down the scale and to nothing above them.

theorem Longobardi2005.objectReference_and_kindReference_iff (c : HeadClass) :

c.objectReference ≠ Access.never ∧ c.kindReference ≠ Access.never ↔ c = HeadClass.specialCommon

The special common nouns alone have both object and kind reference, the former only under marked conditions.

The topological mapping theory #

inductive Longobardi2005.Naming :

What a noun names, an object, learned by applying the name to one term of experience, or a kind, a potentially open set of objects recognizable as such. Proper names are object-naming, common nouns kind-naming.

object : Naming
kind : Naming

Instances For

@[instance_reducible]

instance Longobardi2005.instDecidableEqNaming :

DecidableEq Naming

Equations

Longobardi2005.instDecidableEqNaming x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Longobardi2005.instReprNaming.repr :

Naming → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Longobardi2005.instReprNaming :

Equations

Longobardi2005.instReprNaming = { reprPrec := Longobardi2005.instReprNaming.repr }

inductive Longobardi2005.DContent :

The content of D, which is empty, a lexically referential expression, a noun raised to D, a pronoun, a demonstrative or an expletive article chained to the noun (56a), or an overt operator, a lexical determiner or quantifier (58).

empty : DContent
referential : DContent
operator : DContent

Instances For

@[instance_reducible]

instance Longobardi2005.instDecidableEqDContent :

DecidableEq DContent

Equations

Longobardi2005.instDecidableEqDContent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Longobardi2005.instReprDContent :

Equations

Longobardi2005.instReprDContent = { reprPrec := Longobardi2005.instReprDContent.repr }

def Longobardi2005.instReprDContent.repr :

DContent → ℕ → Std.Format

Equations

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

Instances For

structure Longobardi2005.Nominal :

A nominal, by what its head names and what its D contains.

head : Naming
d : DContent

Instances For

@[instance_reducible]

instance Longobardi2005.instDecidableEqNominal :

DecidableEq Nominal

Equations

Longobardi2005.instDecidableEqNominal = Longobardi2005.instDecidableEqNominal.decEq

def Longobardi2005.instDecidableEqNominal.decEq (x✝ x✝¹ : Nominal) :

Decidable (x✝ = x✝¹)

Equations

Longobardi2005.instDecidableEqNominal.decEq { head := a, d := a_1 } { head := b, d := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

def Longobardi2005.instReprNominal.repr :

Nominal → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Longobardi2005.instReprNominal :

Equations

Longobardi2005.instReprNominal = { reprPrec := Longobardi2005.instReprNominal.repr }

def Longobardi2005.Nominal.IsConstant (n : Nominal) :

A constant has one fixed referential value (54a), which requires referential content in D, by raising or by an expletive article chained to the noun (56a).

Equations

n.IsConstant = (n.d = Longobardi2005.DContent.referential)

Instances For

def Longobardi2005.Nominal.IsVariable (n : Nominal) :

A variable is bound by the operator in D or unselectively when D is empty and ranges over a set (54b), the objects of the kind the noun names (59); objects are not sets, so only a kind-naming noun restricts one.

Equations

n.IsVariable = (n.d ≠ Longobardi2005.DContent.referential ∧ n.head = Longobardi2005.Naming.kind)

Instances For

def Longobardi2005.Nominal.Denotes (n : Nominal) :

Individuals are denoted in D and arguments denote individuals (52), (53), as constants or as variables.

Equations

n.Denotes = (n.IsConstant ∨ n.IsVariable)

Instances For

@[instance_reducible]

instance Longobardi2005.Nominal.instDecidableIsConstant (n : Nominal) :

Decidable n.IsConstant

Equations

n.instDecidableIsConstant = Longobardi2005.Nominal.instDecidableIsConstant._aux_1 n

@[instance_reducible]

instance Longobardi2005.Nominal.instDecidableIsVariable (n : Nominal) :

Decidable n.IsVariable

Equations

n.instDecidableIsVariable = { decide := decide (n.d ≠ Longobardi2005.DContent.referential) && decide (n.head = Longobardi2005.Naming.kind), reflects_decide := ⋯ }

@[instance_reducible]

instance Longobardi2005.Nominal.instDecidableDenotes (n : Nominal) :

Decidable n.Denotes

Equations

n.instDecidableDenotes = { decide := decide n.IsConstant || decide n.IsVariable, reflects_decide := ⋯ }

theorem Longobardi2005.Nominal.isVariable_of_empty {n : Nominal} (h : n.Denotes) (hd : n.d = DContent.empty) :

(55): an argument with an empty D is a variable.

theorem Longobardi2005.Nominal.isVariable_of_not_isConstant {n : Nominal} (h : n.Denotes) (hc : ¬n.IsConstant) :

(56b): an argument that is not a constant is a variable.

theorem Longobardi2005.Nominal.isVariable_of_operator {n : Nominal} (h : n.Denotes) (hd : n.d = DContent.operator) :

A D occupied by a lexical determiner or quantifier is translated into a variable.

theorem Longobardi2005.Nominal.denotes_of_kind {n : Nominal} (h : n.head = Naming.kind) :

(57a): a kind-naming noun denotes with any content of D, so a common noun need not raise.

theorem Longobardi2005.Nominal.denotes_iff_of_object {n : Nominal} (h : n.head = Naming.object) :

n.Denotes ↔ n.IsConstant

(57c): an object-naming noun denotes only as a constant, so a proper name in argument position must fill D, by raising or by an expletive article.

Last Resort #

def Longobardi2005.MayRaise (h : Naming) :

N-to-D raising fills an empty D with referential content, and by Last Resort (63) it is licensed exactly when the nominal would otherwise fail to denote.

Equations

Longobardi2005.MayRaise h = ¬{ head := h, d := Longobardi2005.DContent.empty }.Denotes

Instances For

@[instance_reducible]

instance Longobardi2005.instDecidableMayRaise (h : Naming) :

Decidable (MayRaise h)

Equations

Longobardi2005.instDecidableMayRaise h = { decide := !decide { head := h, d := Longobardi2005.DContent.empty }.Denotes, reflects_decide := ⋯ }

theorem Longobardi2005.mayRaise_iff (h : Naming) :

MayRaise h ↔ h = Naming.object

The answer to (57b) and (57c): a common noun may not raise, since it denotes without, and a proper name may raise, since it must.

Expletive articles #

inductive Longobardi2005.Article :

An article in D is an operator, binding a variable over the kind the noun names, or an expletive, chained to the noun and contributing no operator.

operator : Article
expletive : Article

Instances For

@[instance_reducible]

instance Longobardi2005.instDecidableEqArticle :

DecidableEq Article

Equations

Longobardi2005.instDecidableEqArticle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Longobardi2005.instReprArticle.repr :

Article → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Longobardi2005.instReprArticle :

Equations

Longobardi2005.instReprArticle = { reprPrec := Longobardi2005.instReprArticle.repr }

def Longobardi2005.Article.dContent :

Article → DContent

The content an article gives D.

Equations

Instances For

theorem Longobardi2005.denotes_iff_expletive (a : Article) :

{ head := Naming.object, d := a.dContent }.Denotes ↔ a = Article.expletive

The article of la Maria is obligatorily an expletive: with an object-naming head the nominal denotes only if the article is chained to the name, so it contributes no operator and no kind reading arises (26b).

theorem Longobardi2005.denotes_of_kind_article (a : Article) :

{ head := Naming.kind, d := a.dContent }.Denotes

With a kind-naming head either article yields a denoting argument: the operator binds a variable over the kind (59), and the expletive makes the argument a constant naming the kind, the singular generic of (26a).