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

@cite{schwarz-2009} @cite{schwarz-2013} @cite{hawkins-1978} @cite{coppock-beaver-2015} @cite{patel-grosz-grosz-2017}

The central thesis of @cite{schwarz-2009} 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 (@cite{schwarz-2013}). 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:

• Core.Nominal.NominalKind — 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).
• Core.Nominal.NominalKind.expectedPresupType — projects each kind to the @cite{schwarz-2009} presupposition type it expresses.
• Core.Nominal.ArticleInventory — records the morphological inventory; uniqueAnaphoricSyncretism is the bool 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 @cite{schwarz-2013} §3.2 generalized via bridgingPresupType.

theorem Phenomena.Definiteness.Studies.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 @cite{schwarz-2009} rests on this: if the types were the same, there would be no contrast to expose morphologically.

theorem Phenomena.Definiteness.Studies.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 Phenomena.Definiteness.Studies.Schwarz2009.unique_is_uniqueness {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (sIdx : ℕ) : (Core.Nominal.NominalKind.unique R sIdx).expectedPresupType = some Features.Definiteness.DefPresupType.uniqueness

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

theorem Phenomena.Definiteness.Studies.Schwarz2009.anaphoric_is_familiarity {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (d : ℕ) : (Core.Nominal.NominalKind.anaphoric R d).expectedPresupType = some Features.Definiteness.DefPresupType.familiarity

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

theorem Phenomena.Definiteness.Studies.Schwarz2009.unique_anaphoric_presup_distinct {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (sIdx d : ℕ) : (Core.Nominal.NominalKind.unique R sIdx).expectedPresupType ≠ (Core.Nominal.NominalKind.anaphoric R d).expectedPresupType

The two articles project to distinct presupposition types — the central @cite{schwarz-2009} 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 Phenomena.Definiteness.Studies.Schwarz2009.weak_article_consults_situation_assignment {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (sIdx : ℕ) (g : Core.Assignment F.Entity) (gs : Core.Logic.Intensional.Variables.SitAssignment F) : Core.Nominal.interpret (Core.Nominal.NominalKind.unique R sIdx) g gs = Core.Nominal.russellIota fun (x : F.Denot Core.Logic.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 Phenomena.Definiteness.Studies.Schwarz2009.strong_article_consults_entity_assignment {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (d : ℕ) (g : Core.Assignment F.Entity) (gs : Core.Logic.Intensional.Variables.SitAssignment F) : Core.Nominal.interpret (Core.Nominal.NominalKind.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 Phenomena.Definiteness.Studies.Schwarz2009.situation_binding_classifies_articles {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (sIdx d : ℕ) : (Core.Nominal.NominalKind.unique R sIdx).usesSituationPronoun = true ∧ (Core.Nominal.NominalKind.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 @cite{schwarz-2009} claim that uniqueness is situational and familiarity is anaphoric.

@cite{schwarz-2009} reads the two-article distinction off German morphology. English collapses both into the; the contrast is masked at the surface but recoverable via the inventory's uniqueAnaphoricSyncretism bool.

theorem Phenomena.Definiteness.Studies.Schwarz2009.german_two_articles : Fragments.German.Definiteness.articleInventory.hasUniqueArticle ∧ Fragments.German.Definiteness.articleInventory.hasAnaphoricArticle ∧ ¬Fragments.German.Definiteness.articleInventory.uniqueAnaphoricSyncretism

German has both articles overtly, with no syncretism — the structural @cite{schwarz-2009} contrast is morphologically visible.

theorem Phenomena.Definiteness.Studies.Schwarz2009.english_syncretic_articles : Fragments.English.Definiteness.articleInventory.hasUniqueArticle ∧ Fragments.English.Definiteness.articleInventory.hasAnaphoricArticle ∧ Fragments.English.Definiteness.articleInventory.uniqueAnaphoricSyncretism

English has both articles, but they are syncretic — the covers both. The @cite{schwarz-2009} contrast is real but morphologically invisible.

theorem Phenomena.Definiteness.Studies.Schwarz2009.strategy_split : Fragments.German.Definiteness.articleInventory.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.bipartite ∧ Fragments.English.Definiteness.articleInventory.toMarkingStrategy = 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 Phenomena.Definiteness.Studies.Schwarz2009.morphological_distinction_count : (Features.Definiteness.articleTypeToDistinguishedPresup Fragments.German.Definiteness.articleInventory.toArticleType).length = 2 ∧ (Features.Definiteness.articleTypeToDistinguishedPresup Fragments.English.Definiteness.articleInventory.toArticleType).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 @cite{patel-grosz-grosz-2017} D-layer count read off the article system.

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

@cite{schwarz-2013} §3.1: anaphoric uses pattern with the strong article — i.e., they project the familiarity presupposition.

theorem Phenomena.Definiteness.Studies.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 Phenomena.Definiteness.Studies.Schwarz2009.donkey_use_is_familiarity : Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.donkey = Features.Definiteness.DefPresupType.familiarity

@cite{schwarz-2009} §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 Phenomena.Definiteness.Studies.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.

theorem Phenomena.Definiteness.Studies.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

@cite{schwarz-2013} §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 Phenomena.Definiteness.Studies.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 @cite{schwarz-2009} 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 Phenomena.Definiteness.Studies.Schwarz2009.Student : Type

Two students.

• alice : Student
• bob : Student

@[implicit_reducible]

instance Phenomena.Definiteness.Studies.Schwarz2009.instDecidableEqStudent : DecidableEq Student

Equations

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

def Phenomena.Definiteness.Studies.Schwarz2009.instReprStudent.repr : Student → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Definiteness.Studies.Schwarz2009.instReprStudent : Repr Student

Equations

• Phenomena.Definiteness.Studies.Schwarz2009.instReprStudent = { reprPrec := Phenomena.Definiteness.Studies.Schwarz2009.instReprStudent.repr }

def Phenomena.Definiteness.Studies.Schwarz2009.F0 : Core.Logic.Intensional.Frame

Equations

• Phenomena.Definiteness.Studies.Schwarz2009.F0 = { Entity := Phenomena.Definiteness.Studies.Schwarz2009.Student, Index := Unit }

def Phenomena.Definiteness.Studies.Schwarz2009.studentRestr : Core.Logic.Intensional.Variables.DenotGS F0 Core.Logic.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

• Phenomena.Definiteness.Studies.Schwarz2009.studentRestr _g _gs _x = True

def Phenomena.Definiteness.Studies.Schwarz2009.gAlice : Core.Assignment F0.Entity

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

Equations

• Phenomena.Definiteness.Studies.Schwarz2009.gAlice x✝ = Phenomena.Definiteness.Studies.Schwarz2009.Student.alice

def Phenomena.Definiteness.Studies.Schwarz2009.gs0 : Core.Logic.Intensional.Variables.SitAssignment F0

Equations

• Phenomena.Definiteness.Studies.Schwarz2009.gs0 x✝ = ()

theorem Phenomena.Definiteness.Studies.Schwarz2009.weak_article_fails_on_multi : Core.Nominal.interpret (Core.Nominal.NominalKind.unique studentRestr 0) gAlice gs0 = none

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

theorem Phenomena.Definiteness.Studies.Schwarz2009.strong_article_picks_indexed_antecedent : Core.Nominal.interpret (Core.Nominal.NominalKind.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 Phenomena.Definiteness.Studies.Schwarz2009.two_articles_can_disagree : Core.Nominal.interpret (Core.Nominal.NominalKind.unique studentRestr 0) gAlice gs0 ≠ Core.Nominal.interpret (Core.Nominal.NominalKind.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.