Schwarz (2009): Two Types of Definites in Natural Language

[Sch09b] [Sch13] [Haw78] [CB15] [PGG17]

The central thesis of [Sch09b] is that the surface category "definite article" decomposes into two structurally distinct articles with different presupposition profiles:

• weak article — uniqueness presupposition (Russell/Frege/Strawson; the Coppock–Beaver Uniqueness projector)
• strong article — familiarity presupposition (Heim/Kamp; an antecedent in prior discourse)

Crucially, this is not a stipulation about meaning: it is read off the morphology in languages whose article paradigm overtly distinguishes the two — most prominently German (weak im, vom, zum vs strong in dem, von dem, zu dem), but also Fering, Lakhota, Akan, Hausa, and others ([Sch13]). English collapses both into syncretic the, masking the distinction at the surface.

What this file tests

The split is operationalized in the Core layer by:

• Semantics.Definiteness.Description — distinct .unique (weak) and .anaphoric (strong) constructors, with different argument shapes (.unique carries a situation index for resource-situation binding; .anaphoric carries a discourse index for antecedent lookup).
• Semantics.Definiteness.Description.expectedPresupType — projects each kind to the [Sch09b] presupposition type it expresses.
• Semantics.Definiteness.Determiner — the declared determiner set records the morphological inventory; Determiner.IsSyncretic is the predicate that distinguishes English-style syncretism from German-style bipartition.

We verify:

1. Two distinct presupposition types — .uniqueness and .familiarity are not collapsible in DefPresupType.
2. Constructor split — .unique and .anaphoric project to different presupposition types (uniqueness vs familiarity).
3. Different argument shapes — .unique consults the situation assignment via interpSitPronoun; .anaphoric consults the entity assignment via the discourse index. The interpreter realizes this difference structurally.
4. Morphological correlate — German (bipartite) marks the two types with distinct articles; English (generallyMarked) syncretizes them. The inventory bool uniqueAnaphoricSyncretism is the discriminator.
5. Donkey anaphora patterns with strong — .donkey use type maps to .familiarity, predicting that languages with the contrast use the strong article for donkey pronouns (German von dem, not vom).
6. Bridging split — part-whole bridging maps to uniqueness (weak article), relational/producer bridging to familiarity (strong article). This is [Sch13] §3.2 generalized via bridgingPresupType.

theorem Schwarz2009.two_presup_types_distinct : Features.Definiteness.DefPresupType.uniqueness ≠ Features.Definiteness.DefPresupType.familiarity

The two Schwarz presupposition types are distinct constructors of DefPresupType. The whole architectural claim of [Sch09b] rests on this: if the types were the same, there would be no contrast to expose morphologically.

theorem Schwarz2009.presup_types_exhaustive (p : Features.Definiteness.DefPresupType) : p = Features.Definiteness.DefPresupType.uniqueness ∨ p = Features.Definiteness.DefPresupType.familiarity

DefPresupType has exactly the two Schwarz types — no third article-presupposition type. (The donkey/bridging cells in DefiniteUseType collapse into these two via useTypeToPresupType / bridgingPresupType.)

theorem Schwarz2009.unique_is_uniqueness {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx : ℕ) : (Semantics.Definiteness.Description.unique R sIdx).expectedPresupType = some Features.Definiteness.DefPresupType.uniqueness

The weak article (.unique in the Core sum type) projects to the uniqueness presupposition.

theorem Schwarz2009.anaphoric_is_familiarity {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (d : ℕ) : (Semantics.Definiteness.Description.anaphoric R d).expectedPresupType = some Features.Definiteness.DefPresupType.familiarity

The strong article (.anaphoric in the Core sum type) projects to the familiarity presupposition.

theorem Schwarz2009.unique_anaphoric_presup_distinct {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx d : ℕ) : (Semantics.Definiteness.Description.unique R sIdx).expectedPresupType ≠ (Semantics.Definiteness.Description.anaphoric R d).expectedPresupType

The two articles project to distinct presupposition types — the central [Sch09b] contrast at the type level.

The two articles do not just project different presupposition types — they consult different parts of the bi-assignment. The weak article binds a structural situation pronoun (its restrictor is evaluated at interpSitPronoun sIdx gs); the strong article looks up a discourse referent in the entity assignment (g d).

theorem Schwarz2009.weak_article_consults_situation_assignment {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique R sIdx) g gs = Semantics.Definiteness.russellIota fun (x : Intensional.Denot E W Intensional.Ty.e) => R g gs x

The weak article's restrictor sees the entire situation assignment gs (the unique constructor passes gs to R). The situation index sIdx is structurally recorded but does not affect the interpretation directly — the restrictor itself is what calls interpSitPronoun sIdx to fetch the resource situation.

theorem Schwarz2009.strong_article_consults_entity_assignment {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (d : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric R d) g gs = if R g gs (g d) then some (g d) else none

The strong article's referent is the entity at the discourse index g d, accepted iff the restrictor holds of it. The situation assignment is consulted only through the restrictor R — the constructor itself reads the entity slot.

theorem Schwarz2009.situation_binding_classifies_articles {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx d : ℕ) : (Semantics.Definiteness.Description.unique R sIdx).usesSituationPronoun = true ∧ (Semantics.Definiteness.Description.anaphoric R d).usesSituationPronoun = false

The classifier usesSituationPronoun correctly flags the weak article as a structural binder of the resource situation; the strong article is not. This is the structural correlate of the [Sch09b] claim that uniqueness is situational and familiarity is anaphoric.

[Sch09b] reads the two-article distinction off German morphology. English collapses both into the; the contrast is masked at the surface but recoverable via Determiner.IsSyncretic.

theorem Schwarz2009.german_two_articles : Determiner.MarksPresup German.Definiteness.determiners Features.Definiteness.DefPresupType.uniqueness ∧ Determiner.MarksPresup German.Definiteness.determiners Features.Definiteness.DefPresupType.familiarity ∧ ¬Determiner.IsSyncretic German.Definiteness.determiners

German has both articles overtly, with no syncretism — the structural [Sch09b] contrast is morphologically visible.

theorem Schwarz2009.english_syncretic_articles : Determiner.MarksPresup English.Definiteness.determiners Features.Definiteness.DefPresupType.uniqueness ∧ Determiner.MarksPresup English.Definiteness.determiners Features.Definiteness.DefPresupType.familiarity ∧ Determiner.IsSyncretic English.Definiteness.determiners

English has both articles, but they are syncretic — the covers both. The [Sch09b] contrast is real but morphologically invisible.

theorem Schwarz2009.strategy_split : Determiner.markingStrategy German.Definiteness.determiners = Features.Definiteness.DefMarkingStrategy.bipartite ∧ Determiner.markingStrategy English.Definiteness.determiners = Features.Definiteness.DefMarkingStrategy.generallyMarked

The morphological discriminator: German is .bipartite (two distinct forms), English is .generallyMarked (one syncretic form). Both distinguish the same semantic types — the surface morphology differs.

theorem Schwarz2009.morphological_distinction_count : (Features.Definiteness.articleTypeToDistinguishedPresup (Determiner.articleType German.Definiteness.determiners)).length = 2 ∧ (Features.Definiteness.articleTypeToDistinguishedPresup (Determiner.articleType English.Definiteness.determiners)).length = 1

The number of morphologically distinguished presupposition types differs across the two languages, even though the underlying inventory of semantic distinctions is the same.

German marks 2 (bipartite); English marks 1 (the single the form). This is the [PGG17] D-layer count read off the article system.

theorem Schwarz2009.anaphoric_use_is_familiarity : Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.anaphoric = Features.Definiteness.DefPresupType.familiarity

[Sch13] §3.1: anaphoric uses pattern with the strong article — i.e., they project the familiarity presupposition.

theorem Schwarz2009.situational_uses_are_uniqueness : Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.immediateSituation = Features.Definiteness.DefPresupType.uniqueness ∧ Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.largerSituation = Features.Definiteness.DefPresupType.uniqueness

Immediate-situation and larger-situation uses pattern with the weak article — uniqueness presupposition.

theorem Schwarz2009.donkey_use_is_familiarity : Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.donkey = Features.Definiteness.DefPresupType.familiarity

[Sch09b] §3: donkey pronouns require the strong article in German (von dem, not vom). At the use-type level, this follows from useTypeToPresupType .donkey = .familiarity — the same presupposition type the strong article carries.

This is a non-trivial empirical prediction: a quantifier-bound pronoun in a syntactically inaccessible position is treated by the morphology as a familiarity phenomenon rather than a uniqueness phenomenon.

theorem Schwarz2009.donkey_patterns_with_anaphoric : Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.donkey = Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.anaphoric

Donkey anaphora and discourse anaphora project the same presupposition type — they pattern together morphologically.

Cross-linguistic realization of donkey anaphora

The cross-linguistic pattern ([Sch09b] §3; cf. [Mor21] Table 4.4 for the parallel pattern with anaphoric definites):

• German: strong article (von dem) — the two-article system distinguishes the donkey use overtly
• Thai/Mandarin: demonstrative — demonstratives fill the strong-article role
• Shan: bare noun — no articles, so no morphological signal

structure Schwarz2009.DonkeyArticleDatum : Type

Cross-linguistic datum on how donkey anaphora is expressed morphologically, connecting DefiniteUseType.donkey to concrete article forms.

The article system (articleSystem) is derived from the language's fragment-level determiners, not stipulated independently — the declared Determiner.Entry list is the single source of truth.

• language : String
• isoCode : String
• form : String

  Morphological form used for donkey pronouns

• determiners : List Determiner.Entry

  Declared determiner set (single source of truth from which articleSystem is derived).

def Schwarz2009.DonkeyArticleDatum.articleSystem (d : DonkeyArticleDatum) : Features.Definiteness.ArticleType

Schwarz ArticleType classification, derived from determiners.

Equations

• d.articleSystem = Determiner.articleType d.determiners

def Schwarz2009.germanDonkey : DonkeyArticleDatum

Equations

• Schwarz2009.germanDonkey = { language := "German", isoCode := "deu", form := "strong article (von dem)", determiners := German.Definiteness.determiners }

def Schwarz2009.thaiDonkey : DonkeyArticleDatum

Equations

• Schwarz2009.thaiDonkey = { language := "Thai", isoCode := "tha", form := "demonstrative", determiners := Thai.Definiteness.determiners }

def Schwarz2009.mandarinDonkey : DonkeyArticleDatum

Equations

• Schwarz2009.mandarinDonkey = { language := "Mandarin", isoCode := "cmn", form := "demonstrative", determiners := Mandarin.Definiteness.determiners }

def Schwarz2009.shanDonkey : DonkeyArticleDatum

Equations

• Schwarz2009.shanDonkey = { language := "Shan", isoCode := "shn", form := "bare noun", determiners := Shan.Definiteness.determiners }

def Schwarz2009.donkeyArticleData : List DonkeyArticleDatum

All cross-linguistic donkey article data.

Equations

• Schwarz2009.donkeyArticleData = [Schwarz2009.germanDonkey, Schwarz2009.thaiDonkey, Schwarz2009.mandarinDonkey, Schwarz2009.shanDonkey]

theorem Schwarz2009.weakAndStrong_uses_strong : ((List.filter (fun (x : DonkeyArticleDatum) => x.articleSystem == Features.Definiteness.ArticleType.weakAndStrong) donkeyArticleData).all fun (x : DonkeyArticleDatum) => x.form == "strong article (von dem)") = true

In languages with a weak/strong article distinction, donkey anaphora uses the strong form — never the weak form. This is predicted by donkey_use_is_familiarity: strong articles encode familiarity, and donkey anaphora requires familiarity.

theorem Schwarz2009.bridging_split_at_presup_layer : Features.Definiteness.bridgingPresupType Features.Definiteness.BridgingSubtype.partWhole = Features.Definiteness.DefPresupType.uniqueness ∧ Features.Definiteness.bridgingPresupType Features.Definiteness.BridgingSubtype.relational = Features.Definiteness.DefPresupType.familiarity

[Sch13] §3.2: bridging splits across the two articles. Part-whole bridging (the village ... the church) takes the weak article — situational uniqueness. Relational/producer bridging (the play ... the author) takes the strong article — anaphoric familiarity.

theorem Schwarz2009.bridging_subtypes_realize_both_presup_types : Features.Definiteness.bridgingPresupType Features.Definiteness.BridgingSubtype.partWhole ≠ Features.Definiteness.bridgingPresupType Features.Definiteness.BridgingSubtype.relational

The two bridging subtypes are exactly the two Schwarz presupposition types — bridging is a microcosm of the [Sch09b] contrast. This is the empirical core of why the bridging split argument motivates a structural rather than purely lexical theory of definiteness.

The semantic distinction is not just a presupposition-type label — the two articles can pick different referents in the same context. We build a tiny scenario where the unique satisfier of a restrictor is one entity, and the discourse-indexed entity is a different one (which also satisfies the restrictor). The weak article picks the indexed-by- uniqueness referent (none, because there are two satisfiers); the strong article picks the discourse-indexed antecedent.

inductive Schwarz2009.Student : Type

Two students.

• alice : Student
• bob : Student

@[implicit_reducible]

instance Schwarz2009.instDecidableEqStudent : DecidableEq Student

Equations

• Schwarz2009.instDecidableEqStudent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Schwarz2009.instReprStudent.repr : Student → ℕ → Std.Format

Equations

• Schwarz2009.instReprStudent.repr Schwarz2009.Student.alice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Schwarz2009.Student.alice")).group prec✝
• Schwarz2009.instReprStudent.repr Schwarz2009.Student.bob prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Schwarz2009.Student.bob")).group prec✝

@[implicit_reducible]

instance Schwarz2009.instReprStudent : Repr Student

Equations

• Schwarz2009.instReprStudent = { reprPrec := Schwarz2009.instReprStudent.repr }

def Schwarz2009.studentRestr : Intensional.Variables.DenotGS Student Unit Intensional.Ty.et

Both students count as students. The restrictor has two satisfiers, so the weak (uniqueness) article fails — there is no unique satisfier.

Equations

• Schwarz2009.studentRestr _g _gs _x = True

def Schwarz2009.gAlice : Core.Assignment Student

Discourse referent at index 0 is Alice. The strong article (.anaphoric) reads off this slot.

Equations

• Schwarz2009.gAlice x✝ = Schwarz2009.Student.alice

def Schwarz2009.gs0 : Intensional.Variables.SitAssignment Unit

Equations

• Schwarz2009.gs0 x✝ = ()

theorem Schwarz2009.weak_article_fails_on_multi : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique studentRestr 0) gAlice gs0 = none

The weak article fails on a multi-satisfier restrictor — uniqueness presupposition violation.

theorem Schwarz2009.strong_article_picks_indexed_antecedent : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric studentRestr 0) gAlice gs0 = some Student.alice

The strong article succeeds — it returns the discourse-indexed referent (Alice) regardless of how many entities satisfy the restrictor. The familiarity presupposition does its work via the discourse index, not via uniqueness.

theorem Schwarz2009.two_articles_can_disagree : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique studentRestr 0) gAlice gs0 ≠ Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric studentRestr 0) gAlice gs0

The empirical payoff at the Core API: the two articles, given the same restrictor and bi-assignment, can disagree on what they return. This is the semantic counterpart of the German morphological split.