Demonstrative pronouns — the genuinely deictic carrier

[PGG17] [Mor21]

The deictic demonstrative pronoun (this/that, German dieser, Japanese kore/sore/are): DemonstrativePronoun extends the general Pronoun with a Features.Deixis.Feature — the spatial contrast (proximal/medial/distal) that makes it a demonstrative. One carrier of the word-class-neutral Demonstrative capability; an adnominal demonstrative determiner (this book) or pro-adverb (here) would be sibling carriers.

The membership criterion is the deictic feature, not the morphological label. This is the point of [PGG17]: German der/die/das, traditionally called "demonstrative pronouns", are strong-article personal pronouns with no deixis (their footnote 1) — they are PersonalPronouns, not DemonstrativePronouns (see Studies/PatelGroszGrosz2017.lean). The genuine German demonstrative is dieser. So the PER/DEM(German) distinction is article strength (a Schwarz semantic axis), orthogonal to demonstrativehood (a deictic axis); the type assignment keeps them apart by construction.

Main declarations

• DemonstrativePronoun — the deictic demonstrative pronoun (extends Pronoun + deixis).
• instance : Demonstrative DemonstrativePronoun — its deictic-contrast capability.
• Proform / Bound instances routing it through the Pronoun API.

structure DemonstrativePronounextends Pronoun : Type

A deictic demonstrative pronoun: the general Pronoun (form + φ) plus the Features.Deixis.Feature it encodes — its proximal/medial/distal contrast (or unspecified for a distance-neutral demonstrative like German dieser). Carries no separate denotation here; its meaning is the deictic Semantics.Definiteness.Description.demonstrative over its restrictor.

• form : String
• person : Option Person
• number : Option Number
• case_ : Option Case
• gender : Option Gender
• script : Option String
• pronType : Option UD.PronType
• bindingClass : Option Features.BindingClass
• strength : Option Strength
• deixis : Features.Deixis.Feature

  The deictic feature (proximal/medial/distal, or unspecified).

@[implicit_reducible]

instance instReprDemonstrativePronoun : Repr DemonstrativePronoun

Equations

• instReprDemonstrativePronoun = { reprPrec := instReprDemonstrativePronoun.repr }

def instReprDemonstrativePronoun.repr : DemonstrativePronoun → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instDecidableEqDemonstrativePronoun : DecidableEq DemonstrativePronoun

Equations

• instDecidableEqDemonstrativePronoun = instDecidableEqDemonstrativePronoun.decEq

def instDecidableEqDemonstrativePronoun.decEq (x✝ x✝¹ : DemonstrativePronoun) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instProformDemonstrativePronoun : Proform DemonstrativePronoun

A demonstrative pronoun is a Proform (form + φ via its Pronoun core).

Equations

• instProformDemonstrativePronoun = { form := fun (d : DemonstrativePronoun) => d.form, phi := fun (d : DemonstrativePronoun) => d.toWord.phi }

@[implicit_reducible]

instance instBoundDemonstrativePronoun : Bound DemonstrativePronoun

Its binding class is the Pronoun core's, defaulting an undeclared shell to .pronoun.

Equations

• instBoundDemonstrativePronoun = { bindingClass := fun (d : DemonstrativePronoun) => d.bindingClass.getD Features.BindingClass.pronoun }

@[implicit_reducible]

instance instDemonstrativeDemonstrativePronoun : Demonstrative DemonstrativePronoun

The demonstrative pronoun is a carrier of the Demonstrative (deictic-contrast) capability.

Equations

• instDemonstrativeDemonstrativePronoun = { deixis := DemonstrativePronoun.deixis }