Patel-Grosz & Grosz (2017): Revisiting Pronominal Typology

[PGG17] [Sch09b] [Sch13] [Elb05] [CS99a]

[PGG17] (LI 48(2)) argue, for German, that personal pronouns (PER: er/sie/es) and demonstrative pronouns (DEM: der/die/das) have the same core makeup — both a null NP plus a definite determiner — and differ only in that DEM adds an anaphoric index: DEM is the [Sch09b] strong article, PER the weak article ("the latter are anaphoric in a way that the former are not"). The extra layer is that index, not spatial deixis — their footnote 1 stresses "it is far from clear that there is anything truly 'demonstrative' about" German DEMs. So here der/die/das are strong-article PersonalPronouns, not a separate demonstrative type. The genuinely deictic objects are a different matter: the Description.demonstrative denotation, and the deictic demonstrative pronoun DemonstrativePronoun (German dieser, English this), which carries a Features.Deixis.Feature — der does not, so it is no Demonstrative (Syntax/Pronoun/Demonstrative.lean). PER/DEM (article strength) is thus orthogonal to demonstrativehood (deixis). The PER/DEM distribution then follows from structural economy (Minimize DP!): PER, being less structured, is the default; DEM is licensed only by an added pragmatic effect (emotivity §5.1, disambiguation §5.2, register §5.3).

The contributions are made true by construction on shared substrate:

• DEM = PER + anaphoric index is the [Sch09b] weak/strong refinement Semantics.Definiteness.interpret_anaphoric_eq_unique_of_existsUnique: the strong description (DEM, .anaphoric) and the weak description (PER, .unique) over one restrictor pick the same referent exactly when the indexed entity is the unique satisfier — off that, DEM is anaphoric in a way PER is not. Both denote via Description.ofPresupType, with the strength round-tripping through expectedPresupType (Description.expectedPresupType_ofPresupType); the off-uniqueness divergence — DEM and PER picking different referents — is der_er_can_diverge, reusing [Sch09b] §8's two-satisfier scenario.
• The two-series ↔ two-article correlation (§4) is read off the determiner inventory (Determiner.articleType) and the lexicalized strong series, not stipulated.

Implementation notes

The paper is German-focused (Bavarian in §5.3, passing Portuguese/French/Hebrew). The earlier ~11-language table, a five-context licensing inventory, and a Finnish "counterexample" had no basis in the text and were removed. Minimize DP! as a genuine node-count order (over Pareto.lean/PullbackPreorder) is left as a Todo. The §3 corpus finding — that gender mismatches (e.g. neuter Mädchen/Ehepaar with a non-neuter pronoun) are equally available for PER and DEM, PG&G's argument against a [±NP] split — is recorded in prose, as formalizing it needs antecedent modeling absent here.

inductive PatelGroszGrosz2017.DEMLicensingContext : Type

The three pragmatic contexts that license the strong-article ("DEM") series in German ([PGG17] §5): a positive pragmatic effect must override the Minimize DP! preference for the less-structured PER.

• emotivity : DEMLicensingContext

  §5.1 Emotivity — the speaker expresses emotional engagement with the referent.

• disambiguation : DEMLicensingContext

  §5.2 Disambiguation — DEM avoids the most prominent antecedent (anti-topicality).

• register : DEMLicensingContext

  §5.3 Register — colloquial/dialectal register.

@[implicit_reducible]

instance PatelGroszGrosz2017.instDecidableEqDEMLicensingContext : DecidableEq DEMLicensingContext

Equations

• PatelGroszGrosz2017.instDecidableEqDEMLicensingContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance PatelGroszGrosz2017.instReprDEMLicensingContext : Repr DEMLicensingContext

Equations

• PatelGroszGrosz2017.instReprDEMLicensingContext = { reprPrec := PatelGroszGrosz2017.instReprDEMLicensingContext.repr }

def PatelGroszGrosz2017.instReprDEMLicensingContext.repr : DEMLicensingContext → ℕ → Std.Format

Equations

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

German 3rd-person pronoun inventory

[PGG17] footnote 1: German der/die/das are not truly demonstrative — they are the strong-article counterpart of the personal-pronoun series. So both series are PersonalPronoun, differing only in [Sch09b] article strength; which series a form belongs to is recorded here (the weak/strong split of PronounSystem), not in the theory-neutral PersonalPronoun schema.

def PatelGroszGrosz2017.er : PersonalPronoun

Equations

• PatelGroszGrosz2017.er = { form := "er", person := some Person.third, number := some Number.singular, gender := some Gender.masculine }

def PatelGroszGrosz2017.sie : PersonalPronoun

Equations

• PatelGroszGrosz2017.sie = { form := "sie", person := some Person.third, number := some Number.singular, gender := some Gender.feminine }

def PatelGroszGrosz2017.es : PersonalPronoun

Equations

• PatelGroszGrosz2017.es = { form := "es", person := some Person.third, number := some Number.singular, gender := some Gender.neuter }

def PatelGroszGrosz2017.der : PersonalPronoun

Equations

• PatelGroszGrosz2017.der = { form := "der", person := some Person.third, number := some Number.singular, gender := some Gender.masculine }

def PatelGroszGrosz2017.die : PersonalPronoun

Equations

• PatelGroszGrosz2017.die = { form := "die", person := some Person.third, number := some Number.singular, gender := some Gender.feminine }

def PatelGroszGrosz2017.das : PersonalPronoun

Equations

• PatelGroszGrosz2017.das = { form := "das", person := some Person.third, number := some Number.singular, gender := some Gender.neuter }

structure PatelGroszGrosz2017.PronounSystem : Type

A language's 3rd-person pronoun system as PG&G analyze it: the weak (PER) and strong ("DEM") article series, the article inventory (source of articleType), and the pragmatic contexts licensing the strong series.

• language : String
• weak : List PersonalPronoun
• strong : List PersonalPronoun
• determiners : List Determiner.Entry
• licensing : List DEMLicensingContext

def PatelGroszGrosz2017.PronounSystem.LexicalizesStrong (s : PronounSystem) : Prop

The language lexicalizes a distinct strong-article series (PG&G's added D-layer): at least one strong form is present. Derived, not stipulated.

Equations

• s.LexicalizesStrong = (0 < s.strong.length)

@[implicit_reducible]

instance PatelGroszGrosz2017.PronounSystem.instDecidablePredLexicalizesStrong : DecidablePred LexicalizesStrong

Equations

• s.instDecidablePredLexicalizesStrong = PatelGroszGrosz2017.PronounSystem.instDecidablePredLexicalizesStrong._aux_1 s

def PatelGroszGrosz2017.german : PronounSystem

German: weak PER er/sie/es, strong "DEM" der/die/das, weak/strong articles, all three licensing contexts attested ([PGG17] §5).

Equations

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

The contributions, derived

theorem PatelGroszGrosz2017.german_lexicalizes_strong : german.LexicalizesStrong

German lexicalizes a distinct strong-article pronoun series — derived from the presence of der/die/das, not stipulated.

theorem PatelGroszGrosz2017.german_weakAndStrong : Determiner.articleType german.determiners = Features.Definiteness.ArticleType.weakAndStrong

German's article system is .weakAndStrong (two distinct article forms) — derived from the determiner inventory, matching its weak/strong pronoun series ([PGG17] §4).

theorem PatelGroszGrosz2017.schwarz_pgg_german_consistent : Determiner.markingStrategy German.Definiteness.determiners = Features.Definiteness.DefMarkingStrategy.bipartite ∧ german.LexicalizesStrong ∧ Determiner.articleType german.determiners = Features.Definiteness.ArticleType.weakAndStrong

The [Sch09b]/[Sch13] weak/strong typology meets PG&G's two-series claim: German's two distinct article forms (deriving .bipartite) correspond to its lexicalized strong series and the .weakAndStrong article type — all derived from the determiner inventory + the strong forms.

The empirical payoff: the two series can diverge

theorem PatelGroszGrosz2017.der_er_can_diverge : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.ofPresupType Features.Definiteness.DefPresupType.uniqueness Schwarz2009.studentRestr 0) Schwarz2009.gAlice Schwarz2009.gs0 ≠ Semantics.Definiteness.interpret (Semantics.Definiteness.Description.ofPresupType Features.Definiteness.DefPresupType.familiarity Schwarz2009.studentRestr 0) Schwarz2009.gAlice Schwarz2009.gs0

[PGG17]'s actual claim — DEM "is anaphoric in a way" PER "is not" — made concrete: the strong-article "DEM" reading (der, ofPresupType .familiarity) and the weak-article PER reading (er, ofPresupType .uniqueness), over one restrictor and bi-assignment, pick different referents. Reusing [Sch09b] §8's two-satisfier scenario: the weak PER fails uniqueness (two satisfiers → none) while the strong DEM reads off the discourse index. This is the divergence direction the convergence theorem (Semantics.Definiteness.interpret_anaphoric_eq_unique_of_existsUnique) rules out only under uniqueness.

Grounding the Pronoun API: PersonalPronoun denotes via a φ-restricted definite description

A personal pronoun is a definite description over a null NP whose φ-features are presuppositions ([Elb05] pronouns-as-definites; gender = null-NP concord à la Sauerland; the partial-identity view of φ in Semantics/Presupposition/PhiFeatures, after Cooper/Heim & Kratzer). The PER series is the weak article (uniqueness); the marked DEM series the strong (familiarity, der_er_can_diverge above) — article-strength is per-series, not a per-element slot (like deficiency, unlike the demonstrative's deixis). The load-bearing parallel to the demonstrative grounding (Studies/Hanink2021): there deixis filled Description.demonstrative's slot; here the Proform.phi gender supplies the restrictor's presupposition.

theorem PatelGroszGrosz2017.feminine_per_restrictor_is_femSem {E W : Type} (isFemale : E → Prop) (sIdx : ℕ) : Semantics.Definiteness.Description.ofPresupType Features.Definiteness.DefPresupType.uniqueness (fun (x : Core.Assignment E) (x_1 : Intensional.Variables.SitAssignment W) (x_2 : Intensional.Denot E W Intensional.Ty.e) => (Semantics.Presupposition.PhiFeatures.femSem isFemale).presup x_2) sIdx = Semantics.Definiteness.Description.unique (fun (x : Core.Assignment E) (x_1 : Intensional.Variables.SitAssignment W) (x_2 : Intensional.Denot E W Intensional.Ty.e) => isFemale x_2) sIdx

⟦sie⟧ made concrete: the feminine PER's weak-article restrictor is the femSem presupposition — true by construction ((femSem isFemale).presup = isFemale), so the gender feature drives the definite description's restrictor rather than re-stipulating it.

theorem PatelGroszGrosz2017.feminine_per_picks_unique_female {E W : Type} (isFemale : E → Prop) (sIdx : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.ofPresupType Features.Definiteness.DefPresupType.uniqueness (fun (x : Core.Assignment E) (x_1 : Intensional.Variables.SitAssignment W) (x_2 : Intensional.Denot E W Intensional.Ty.e) => (Semantics.Presupposition.PhiFeatures.femSem isFemale).presup x_2) sIdx) g gs = Semantics.Definiteness.russellIota fun (x : E) => isFemale x

Consequently a feminine PER picks the unique female — the gender presupposition is the restrictor of the weak-article definite (ιx[isFemale x]).