Pronoun Typology: PER/DEM Classification + Gradient Measures

@cite{cardinaletti-starke-1999} @cite{elbourne-2005} @cite{patel-grosz-grosz-2017} @cite{postal-1966} @cite{schwarz-2009} @cite{schwarz-2013} @cite{levshina-stoynova-2023}

@cite{patel-grosz-grosz-2017} "Revisiting Pronominal Typology" (LI 48(2)) argue that 3rd-person pronouns split into two structural types:

• PER (personal): D_det + NP (weak article only)
• DEM (demonstrative): D_deix + D_det + NP (strong article)

Minimize DP! makes PER the default; DEM requires pragmatic licensing (emotivity, disambiguation, register).

Key Claims

1. If a language has DEM pronouns, it also has PER pronouns (DEM ⊂ PER)
2. DEM use requires pragmatic licensing (Minimize DP!)
3. Article system predicts D-layer structure

Gradient Component

Following @cite{levshina-stoynova-2023} / WordOrder/Gradience.lean, we encode continuous measures of pronoun system complexity: inventory sizes, licensing context counts, and strength-level counts.

inductive Phenomena.Anaphora.Typology.PronounClass : Type

@cite{patel-grosz-grosz-2017}: structural classification of 3rd-person pronouns.

PER pronouns project only D_det (weak article layer). DEM pronouns project D_deix + D_det (strong article layer).

• per : PronounClass
• dem : PronounClass

instance Phenomena.Anaphora.Typology.instDecidableEqPronounClass : DecidableEq PronounClass

Equations

• Phenomena.Anaphora.Typology.instDecidableEqPronounClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Anaphora.Typology.instBEqPronounClass.beq : PronounClass → PronounClass → Bool

Equations

• Phenomena.Anaphora.Typology.instBEqPronounClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Typology.instBEqPronounClass : BEq PronounClass

Equations

• Phenomena.Anaphora.Typology.instBEqPronounClass = { beq := Phenomena.Anaphora.Typology.instBEqPronounClass.beq }

instance Phenomena.Anaphora.Typology.instReprPronounClass : Repr PronounClass

Equations

• Phenomena.Anaphora.Typology.instReprPronounClass = { reprPrec := Phenomena.Anaphora.Typology.instReprPronounClass.repr }

def Phenomena.Anaphora.Typology.instReprPronounClass.repr : PronounClass → Nat → Std.Format

Equations

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

inductive Phenomena.Anaphora.Typology.PronounStrength : Type

@cite{cardinaletti-starke-1999}: pronoun strength.

Three-way typology based on phonological/syntactic deficiency:

• Strong: full, stressed (can be coordinated, modified, focused)
• Weak: reduced, unstressed (cannot be coordinated/focused)
• Clitic: phonologically deficient, must attach to host

• strong : PronounStrength
• weak : PronounStrength
• clitic : PronounStrength

instance Phenomena.Anaphora.Typology.instDecidableEqPronounStrength : DecidableEq PronounStrength

Equations

• Phenomena.Anaphora.Typology.instDecidableEqPronounStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Anaphora.Typology.instBEqPronounStrength : BEq PronounStrength

Equations

• Phenomena.Anaphora.Typology.instBEqPronounStrength = { beq := Phenomena.Anaphora.Typology.instBEqPronounStrength.beq }

def Phenomena.Anaphora.Typology.instBEqPronounStrength.beq : PronounStrength → PronounStrength → Bool

Equations

• Phenomena.Anaphora.Typology.instBEqPronounStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Anaphora.Typology.instReprPronounStrength.repr : PronounStrength → Nat → Std.Format

Equations

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

instance Phenomena.Anaphora.Typology.instReprPronounStrength : Repr PronounStrength

Equations

• Phenomena.Anaphora.Typology.instReprPronounStrength = { reprPrec := Phenomena.Anaphora.Typology.instReprPronounStrength.repr }

inductive Phenomena.Anaphora.Typology.DEMLicensingContext : Type

Pragmatic contexts that license DEM pronoun use (@cite{patel-grosz-grosz-2017} §3).

Minimize DP! requires DEM to be pragmatically licensed. These are the five licensing contexts identified by PG&G.

• emotivity : DEMLicensingContext
• disambiguation : DEMLicensingContext
• register : DEMLicensingContext
• deixis : DEMLicensingContext
• contrast : DEMLicensingContext

instance Phenomena.Anaphora.Typology.instDecidableEqDEMLicensingContext : DecidableEq DEMLicensingContext

Equations

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

instance Phenomena.Anaphora.Typology.instBEqDEMLicensingContext : BEq DEMLicensingContext

Equations

• Phenomena.Anaphora.Typology.instBEqDEMLicensingContext = { beq := Phenomena.Anaphora.Typology.instBEqDEMLicensingContext.beq }

def Phenomena.Anaphora.Typology.instBEqDEMLicensingContext.beq : DEMLicensingContext → DEMLicensingContext → Bool

Equations

• Phenomena.Anaphora.Typology.instBEqDEMLicensingContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Anaphora.Typology.instReprDEMLicensingContext.repr : DEMLicensingContext → Nat → Std.Format

Equations

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

instance Phenomena.Anaphora.Typology.instReprDEMLicensingContext : Repr DEMLicensingContext

Equations

• Phenomena.Anaphora.Typology.instReprDEMLicensingContext = { reprPrec := Phenomena.Anaphora.Typology.instReprDEMLicensingContext.repr }

structure Phenomena.Anaphora.Typology.PronounForm : Type

A 3rd-person pronoun form in a language's inventory.

• form : String
• pronClass : PronounClass
• gender : Option String
• number : Option Number
• strengths : List PronounStrength

def Phenomena.Anaphora.Typology.instReprPronounForm.repr : PronounForm → Nat → Std.Format

Equations

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

instance Phenomena.Anaphora.Typology.instReprPronounForm : Repr PronounForm

Equations

• Phenomena.Anaphora.Typology.instReprPronounForm = { reprPrec := Phenomena.Anaphora.Typology.instReprPronounForm.repr }

def Phenomena.Anaphora.Typology.instBEqPronounForm.beq : PronounForm → PronounForm → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Anaphora.Typology.instBEqPronounForm.beq x✝¹ x✝ = false

instance Phenomena.Anaphora.Typology.instBEqPronounForm : BEq PronounForm

Equations

• Phenomena.Anaphora.Typology.instBEqPronounForm = { beq := Phenomena.Anaphora.Typology.instBEqPronounForm.beq }

structure Phenomena.Anaphora.Typology.PronounSystemDatum : Type

Per-language pronoun system datum (@cite{patel-grosz-grosz-2017} + @cite{cardinaletti-starke-1999}).

Each datum records the full 3rd-person pronoun inventory, article system, D-layer count, DEM licensing contexts, and DEM productivity.

• language : String
• isoCode : String
• forms : List PronounForm

  Available 3rd-person pronoun forms

• articleType : Core.Definiteness.ArticleType

  Article system type

• dLayers : Nat

  Number of D-layers: 1 = D_det only (PER), 2 = D_deix + D_det (PER+DEM)

• demLicensing : List DEMLicensingContext

  Pragmatic contexts licensing DEM use (empty for PER-only languages)

• demProductive : Bool

  Whether DEM pronouns are productive (freely usable) as 3rd-person reference

instance Phenomena.Anaphora.Typology.instReprPronounSystemDatum : Repr PronounSystemDatum

Equations

• Phenomena.Anaphora.Typology.instReprPronounSystemDatum = { reprPrec := Phenomena.Anaphora.Typology.instReprPronounSystemDatum.repr }

def Phenomena.Anaphora.Typology.instReprPronounSystemDatum.repr : PronounSystemDatum → Nat → Std.Format

Equations

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

instance Phenomena.Anaphora.Typology.instBEqPronounSystemDatum : BEq PronounSystemDatum

Equations

• Phenomena.Anaphora.Typology.instBEqPronounSystemDatum = { beq := Phenomena.Anaphora.Typology.instBEqPronounSystemDatum.beq }

def Phenomena.Anaphora.Typology.instBEqPronounSystemDatum.beq : PronounSystemDatum → PronounSystemDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Anaphora.Typology.instBEqPronounSystemDatum.beq x✝¹ x✝ = false

def Phenomena.Anaphora.Typology.germanData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.bavarianData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.portugueseData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.hebrewData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.czechData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.frenchData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.italianData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.spanishData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.catalanData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.kutchiGujaratiData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.englishData : PronounSystemDatum

Equations

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

def Phenomena.Anaphora.Typology.allData : List PronounSystemDatum

All 11 languages from @cite{patel-grosz-grosz-2017} survey.

Equations

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

theorem Phenomena.Anaphora.Typology.allData_count : allData.length = 11

def Phenomena.Anaphora.Typology.finnishData : PronounSystemDatum

Finnish: "hän" (3sg human, PER, no gender), "he" (3pl human, PER), "se" (3sg non-human / DEM), "tämä" (proximal DEM), "tuo" (distal DEM). No articles. "se" is productively used as 3rd-person reference in colloquial Finnish. Not part of @cite{patel-grosz-grosz-2017} sample — a counterexample to the article-DEM productivity correlation (2 D-layers, productive DEM, but no articles).

Equations

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

structure Phenomena.Anaphora.Typology.PronounComplexityProfile : Type

Gradient pronoun system profile, analogous to GradientWOProfile.

Captures continuous variation in pronoun system complexity across languages.

• name : String
• isoCode : String
• perInventory : Nat

  Number of distinct PER pronoun forms

• demInventory : Nat

  Number of distinct DEM pronoun forms usable as pronouns

• demLicensingCount : Nat

  Number of pragmatic contexts licensing DEM use (0–5 scale)

• strengthLevels : Nat

  Pronoun strength levels available: 1=strong only, 2=strong+weak, 3=strong+weak+clitic

def Phenomena.Anaphora.Typology.instReprPronounComplexityProfile.repr : PronounComplexityProfile → Nat → Std.Format

Equations

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

instance Phenomena.Anaphora.Typology.instReprPronounComplexityProfile : Repr PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.instReprPronounComplexityProfile = { reprPrec := Phenomena.Anaphora.Typology.instReprPronounComplexityProfile.repr }

instance Phenomena.Anaphora.Typology.instDecidableEqPronounComplexityProfile : DecidableEq PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.instDecidableEqPronounComplexityProfile = Phenomena.Anaphora.Typology.instDecidableEqPronounComplexityProfile.decEq

def Phenomena.Anaphora.Typology.instDecidableEqPronounComplexityProfile.decEq (x✝ x✝¹ : PronounComplexityProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Anaphora.Typology.instBEqPronounComplexityProfile : BEq PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.instBEqPronounComplexityProfile = { beq := Phenomena.Anaphora.Typology.instBEqPronounComplexityProfile.beq }

def Phenomena.Anaphora.Typology.instBEqPronounComplexityProfile.beq : PronounComplexityProfile → PronounComplexityProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Anaphora.Typology.instBEqPronounComplexityProfile.beq x✝¹ x✝ = false

def Phenomena.Anaphora.Typology.PronounSystemDatum.toProfile (d : PronounSystemDatum) : PronounComplexityProfile

Compute gradient profile from a PronounSystemDatum.

Equations

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

def Phenomena.Anaphora.Typology.germanProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.germanProfile = Phenomena.Anaphora.Typology.germanData.toProfile

def Phenomena.Anaphora.Typology.bavarianProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.bavarianProfile = Phenomena.Anaphora.Typology.bavarianData.toProfile

def Phenomena.Anaphora.Typology.portugueseProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.portugueseProfile = Phenomena.Anaphora.Typology.portugueseData.toProfile

def Phenomena.Anaphora.Typology.hebrewProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.hebrewProfile = Phenomena.Anaphora.Typology.hebrewData.toProfile

def Phenomena.Anaphora.Typology.czechProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.czechProfile = Phenomena.Anaphora.Typology.czechData.toProfile

def Phenomena.Anaphora.Typology.frenchProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.frenchProfile = Phenomena.Anaphora.Typology.frenchData.toProfile

def Phenomena.Anaphora.Typology.italianProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.italianProfile = Phenomena.Anaphora.Typology.italianData.toProfile

def Phenomena.Anaphora.Typology.spanishProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.spanishProfile = Phenomena.Anaphora.Typology.spanishData.toProfile

def Phenomena.Anaphora.Typology.catalanProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.catalanProfile = Phenomena.Anaphora.Typology.catalanData.toProfile

def Phenomena.Anaphora.Typology.kutchiGujaratiProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.kutchiGujaratiProfile = Phenomena.Anaphora.Typology.kutchiGujaratiData.toProfile

def Phenomena.Anaphora.Typology.englishProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.englishProfile = Phenomena.Anaphora.Typology.englishData.toProfile

def Phenomena.Anaphora.Typology.allProfiles : List PronounComplexityProfile

All 11 gradient pronoun system profiles.

Equations

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

theorem Phenomena.Anaphora.Typology.allProfiles_count : allProfiles.length = 11

def Phenomena.Anaphora.Typology.finnishProfile : PronounComplexityProfile

Equations

• Phenomena.Anaphora.Typology.finnishProfile = Phenomena.Anaphora.Typology.finnishData.toProfile

theorem Phenomena.Anaphora.Typology.finnish_counterexample_to_article_dem : (finnishData.dLayers == 2) = true ∧ finnishData.demProductive = true ∧ (finnishData.articleType == Core.Definiteness.ArticleType.none_) = true

Finnish has productive DEM with no articles — a counterexample to the PG&G sample's dem_productivity_from_article_system generalization.

PG&G Core Claims

theorem Phenomena.Anaphora.Typology.minimize_dp : ((List.filter (fun (x : PronounSystemDatum) => x.demProductive) allData).all fun (x : PronounSystemDatum) => decide (x.demLicensing.length > 0)) = true

Minimize DP! (@cite{patel-grosz-grosz-2017} §3): Languages where DEM is productive all require pragmatic licensing (demLicensing is non-empty).

DEM is the marked choice; PER is the default.

theorem Phenomena.Anaphora.Typology.dem_implies_per : (allData.all fun (d : PronounSystemDatum) => if (d.forms.any fun (x : PronounForm) => x.pronClass == PronounClass.dem) = true then d.forms.any fun (x : PronounForm) => x.pronClass == PronounClass.per else true) = true

Implicational universal: If DEM exists in a language's inventory, PER also exists. No language has DEM without PER.

This follows from PG&G's structural claim: DEM = D_deix + D_det + NP, where D_det is the PER layer. DEM presupposes PER structurally.

theorem Phenomena.Anaphora.Typology.strong_article_two_layers : ((List.filter (fun (x : PronounSystemDatum) => x.articleType == Core.Definiteness.ArticleType.weakAndStrong) allData).all fun (x : PronounSystemDatum) => x.dLayers == 2) = true

Article-D-layer correlation (@cite{schwarz-2009} → PG&G): Languages with both weak and strong articles have 2 D-layers.

theorem Phenomena.Anaphora.Typology.one_layer_no_strong_articles : ((List.filter (fun (x : PronounSystemDatum) => x.dLayers == 1) allData).all fun (x : PronounSystemDatum) => x.articleType != Core.Definiteness.ArticleType.weakAndStrong) = true

PER-only languages (1 D-layer) have only weak or no articles. The converse of strong_article_two_layers.

Gradient Claims

theorem Phenomena.Anaphora.Typology.per_inventory_range : kutchiGujaratiProfile.perInventory = 2 ∧ germanProfile.perInventory = 3 ∧ (allProfiles.all fun (x : PronounComplexityProfile) => decide (x.perInventory ≥ 2)) = true

PER inventory is continuous: ranges from 2 (Kutchi Gujarati) to 3 (most languages with m/f/n), not a binary split.

theorem Phenomena.Anaphora.Typology.strong_articles_have_dem_forms : ((List.filter (fun (x : PronounSystemDatum) => x.articleType == Core.Definiteness.ArticleType.weakAndStrong) allData).all fun (d : PronounSystemDatum) => decide ((List.filter (fun (x : PronounForm) => x.pronClass == PronounClass.dem) d.forms).length > 0)) = true

DEM inventory correlates with article system: languages with weakAndStrong articles have non-zero DEM inventory.

theorem Phenomena.Anaphora.Typology.romance_three_strength_levels : have romance := [frenchProfile, italianProfile, spanishProfile, catalanProfile]; (romance.all fun (x : PronounComplexityProfile) => x.strengthLevels == 3) = true

Strength levels vary: Romance languages (French, Italian, Spanish, Catalan) have 3 strength levels (strong+weak+clitic), while Germanic typically has 2.

theorem Phenomena.Anaphora.Typology.germanic_two_strength_levels : have germanic := [germanProfile, bavarianProfile]; (germanic.all fun (x : PronounComplexityProfile) => x.strengthLevels == 2) = true

Germanic languages with DEM (German, Bavarian) have 2 strength levels.

theorem Phenomena.Anaphora.Typology.dem_licensing_is_gradient : englishProfile.demLicensingCount = 0 ∧ germanProfile.demLicensingCount = 5 ∧ (allProfiles.any fun (x : PronounComplexityProfile) => x.demLicensingCount == 2) = true ∧ (allProfiles.any fun (x : PronounComplexityProfile) => x.demLicensingCount == 3) = true

DEM licensing count ranges from 0 to 5, forming a continuum rather than a binary productive/non-productive distinction.

Open Problem

theorem Phenomena.Anaphora.Typology.dem_productivity_from_article_system : ((List.filter (fun (d : PronounSystemDatum) => decide ((d.dLayers == 2) = true ∧ d.demProductive = true)) allData).all fun (x : PronounSystemDatum) => x.articleType == Core.Definiteness.ArticleType.weakAndStrong) = true

DEM productivity tracks overt strong articles (pattern in PG&G data):

Among 2-layer languages, only those with overt weak+strong article morphology (German, Bavarian) have productive DEM. Languages with 2 D-layers but no overt articles (Hebrew, Czech) or limited article systems restrict DEM.

@cite{schwarz-2013} §5.5 provides the theoretical link: the strong article conventionalizes the D_deix layer, making DEM pronouns (which also project D_deix) more accessible. Without overt strong articles, D_deix is available syntactically but not conventionalized for reference tracking.

Open question: why does article-system conventionalization affect pronoun productivity? PG&G suggest familiarity/frequency; @cite{schwarz-2013} suggests the strong article's anaphoric function naturally extends to pronominal use.

Definite use types (@cite{hawkins-1978}, @cite{schwarz-2013} §2.1)

Types and mappings are defined in Core/Definiteness.lean: DefiniteUseType, BridgingSubtype, useTypeToPresupType, bridgingPresupType.

@cite{schwarz-2013} cross-linguistic article paradigm data

structure Phenomena.Anaphora.Typology.SchwarzArticleDatum : Type

Per-language article paradigm from @cite{schwarz-2013}.

• language : String
• isoCode : String
• strongForm : Option String

  Morphological form of the strong article (if any)

• weakForm : Option String

  Morphological form of the weak article (if any)

• weakStrategy : Core.Definiteness.WeakArticleStrategy

  How weak definites are expressed

• strongForAnaphoric : Bool

  Strong article used for anaphoric definites

• weakForUniqueness : Bool

  Weak article/bare nominal used for uniqueness/situational

• bridgingSplit : Bool

  Bridging shows the split (part-whole = weak, producer = strong)

def Phenomena.Anaphora.Typology.instReprSchwarzArticleDatum.repr : SchwarzArticleDatum → Nat → Std.Format

Equations

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

instance Phenomena.Anaphora.Typology.instReprSchwarzArticleDatum : Repr SchwarzArticleDatum

Equations

• Phenomena.Anaphora.Typology.instReprSchwarzArticleDatum = { reprPrec := Phenomena.Anaphora.Typology.instReprSchwarzArticleDatum.repr }

instance Phenomena.Anaphora.Typology.instBEqSchwarzArticleDatum : BEq SchwarzArticleDatum

Equations

• Phenomena.Anaphora.Typology.instBEqSchwarzArticleDatum = { beq := Phenomena.Anaphora.Typology.instBEqSchwarzArticleDatum.beq }

def Phenomena.Anaphora.Typology.instBEqSchwarzArticleDatum.beq : SchwarzArticleDatum → SchwarzArticleDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Anaphora.Typology.instBEqSchwarzArticleDatum.beq x✝¹ x✝ = false

def Phenomena.Anaphora.Typology.schwarz_german : SchwarzArticleDatum

Equations

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

def Phenomena.Anaphora.Typology.schwarz_fering : SchwarzArticleDatum

Equations

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

def Phenomena.Anaphora.Typology.schwarz_akan : SchwarzArticleDatum

Equations

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

def Phenomena.Anaphora.Typology.schwarz_mauritianCreole : SchwarzArticleDatum

Equations

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

def Phenomena.Anaphora.Typology.schwarz_lakhota : SchwarzArticleDatum

Equations

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

def Phenomena.Anaphora.Typology.schwarz_hausa : SchwarzArticleDatum

Equations

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

def Phenomena.Anaphora.Typology.schwarz_haitianCreole : SchwarzArticleDatum

Equations

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

def Phenomena.Anaphora.Typology.allSchwarzData : List SchwarzArticleDatum

All 7 languages from @cite{schwarz-2013} survey.

Equations

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

theorem Phenomena.Anaphora.Typology.allSchwarzData_count : allSchwarzData.length = 7

@cite{schwarz-2013} verified generalizations

theorem Phenomena.Anaphora.Typology.strong_for_anaphoric : (allSchwarzData.all fun (x : SchwarzArticleDatum) => x.strongForAnaphoric) = true

Strong article → anaphoric use (@cite{schwarz-2013} §3.1.1): All surveyed languages use the strong article for anaphoric definites.

theorem Phenomena.Anaphora.Typology.weak_for_uniqueness : (allSchwarzData.all fun (x : SchwarzArticleDatum) => x.weakForUniqueness) = true

Weak form → uniqueness/situational use (@cite{schwarz-2013} §3.1.2): All surveyed languages use weak articles (or bare nominals) for uniqueness-based definites.

theorem Phenomena.Anaphora.Typology.bridging_split_is_majority : (List.filter (fun (x : SchwarzArticleDatum) => x.bridgingSplit) allSchwarzData).length = 5

Bridging split (@cite{schwarz-2013} §3.2): Most languages split bridging across article forms (part-whole = weak, producer = strong). 5 of 7 languages show this pattern; Hausa lacks data, and Haitian Creole uses a single form for everything.

theorem Phenomena.Anaphora.Typology.bare_nominal_languages : (List.filter (fun (x : SchwarzArticleDatum) => x.weakStrategy == Core.Definiteness.WeakArticleStrategy.bareNominal) allSchwarzData).length = 2

Bare-nominal strategy (@cite{schwarz-2013} §4.1): Languages with only one overt article form (Akan, Mauritian Creole) use bare nominals for weak-article definites.

theorem Phenomena.Anaphora.Typology.haitian_creole_no_split : (schwarz_haitianCreole.weakStrategy == Core.Definiteness.WeakArticleStrategy.sameAsStrong) = true

Haitian Creole is exceptional (@cite{schwarz-2013} §4.3): single determiner la for both anaphoric and uniqueness uses — no weak/strong split.

Bridge: Schwarz article types ↔ PG&G pronoun D-layers

@cite{schwarz-2013} §5.5 explicitly connects the article contrast to pronouns: "pronouns are definite articles without overt NP". German d-pronouns (der/die/das) are identical to strong articles. The pronominal domain shows parallel contrasts (/2007, /2011).

The structural mapping:

• Schwarz weak article = PG&G D_det layer = PER pronoun
• Schwarz strong article = PG&G D_deix + D_det = DEM pronoun

theorem Phenomena.Anaphora.Typology.schwarz_pgg_german_consistent : schwarz_german.strongForm.isSome = true ∧ schwarz_german.weakForm.isSome = true ∧ (germanData.dLayers == 2) = true ∧ (germanData.articleType == Core.Definiteness.ArticleType.weakAndStrong) = true

Languages with two overt article forms in @cite{schwarz-2013} correspond to 2-D-layer languages in @cite{patel-grosz-grosz-2017}. Verified for German, which appears in both datasets.

theorem Phenomena.Anaphora.Typology.semantic_mapping_parallel : Core.Definiteness.useTypeToPresupType Core.Definiteness.DefiniteUseType.anaphoric = Core.Definiteness.DefPresupType.familiarity ∧ Core.Definiteness.useTypeToPresupType Core.Definiteness.DefiniteUseType.immediateSituation = Core.Definiteness.DefPresupType.uniqueness ∧ Core.Definiteness.useTypeToPresupType Core.Definiteness.DefiniteUseType.largerSituation = Core.Definiteness.DefPresupType.uniqueness

The semantic mapping is compositional (@cite{schwarz-2013} §2.2):

• Weak article contributes uniqueness presupposition (ι-operator)
• Strong article contributes familiarity/anaphoricity (index variable) This parallels PG&G's D_det (weak/uniqueness) vs D_deix (strong/deixis).

Bridge 1: PronounClass ↔ AnaphorType (Coreference.lean)

def Phenomena.Anaphora.Typology.pronClassToAnaphorType : PronounClass → Coreference.AnaphorType

PER pronouns correspond to AnaphorType.pronoun in Coreference.lean. DEM pronouns have no direct AnaphorType counterpart — they are structurally richer than simple pronouns but not descriptions either.

Equations

• Phenomena.Anaphora.Typology.pronClassToAnaphorType Phenomena.Anaphora.Typology.PronounClass.per = Phenomena.Anaphora.Coreference.AnaphorType.pronoun
• Phenomena.Anaphora.Typology.pronClassToAnaphorType Phenomena.Anaphora.Typology.PronounClass.dem = Phenomena.Anaphora.Coreference.AnaphorType.pronoun

theorem Phenomena.Anaphora.Typology.per_is_pronoun_binding : pronClassToAnaphorType PronounClass.per = Coreference.AnaphorType.pronoun

All PER forms map to the pronoun binding pattern (Principle B domain).

Bridge 2: DEM pronouns ↔ Kaplan-style true demonstratives

DEM pronouns require D_deix — the same structural layer that hosts Kaplan's demonstration. True demonstratives in Demonstratives.lean have a Demonstration component; DEM pronouns require D_deix licensing.

The connection: D_deix is the syntactic home of the demonstration. PER pronouns lack D_deix, so they cannot be true demonstratives.

theorem Phenomena.Anaphora.Typology.dem_requires_deixis_layer : (allData.all fun (d : PronounSystemDatum) => if (d.forms.any fun (x : PronounForm) => x.pronClass == PronounClass.dem) = true then d.dLayers == 2 else true) = true

DEM pronouns require D_deix (dLayers = 2), which is the structural position for Kaplan's demonstration. PER-only languages (dLayers = 1) cannot have true demonstrative pronouns.

Bridge 3: PER pronouns ↔ Direct Reference

PER pronouns are directly referential in Kaplan's sense: they contribute their referent to the proposition, with no descriptive content (no D_deix, no demonstration, no descriptive component).

This connects to DirectReference.lean's modal argument: PER pronouns, like names, are rigid designators. DEM pronouns may involve a descriptive/deictic component (D_deix), making them potentially non-rigid under some analyses.

theorem Phenomena.Anaphora.Typology.per_only_directly_referential : ((List.filter (fun (x : PronounSystemDatum) => x.dLayers == 1) allData).all fun (d : PronounSystemDatum) => d.forms.all fun (x : PronounForm) => x.pronClass == PronounClass.per) = true

PER-only languages have no descriptive D-layer: all forms are directly referential (rigid designators).

Bridge 4: Article system ↔ D-layer count

@cite{schwarz-2009} establishes that the weak/strong article distinction is structurally real (D_det vs D_deix + D_det). PG&G build on this: languages with both article types have the structural space for DEM.

theorem Phenomena.Anaphora.Typology.covert_deixis_layer : (List.filter (fun (d : PronounSystemDatum) => decide ((d.articleType == Core.Definiteness.ArticleType.none_) = true ∧ (d.dLayers == 2) = true)) allData).length > 0

No-article languages with DEM (Hebrew, Czech) show that D-layers can exist without overt article morphology. The D_deix layer is present in the syntax even without morphological exponence.