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

This file formalizes [Sch09b]'s thesis that the definite article decomposes into two articles with distinct presuppositions, the weak article of uniqueness and the strong article of familiarity, read off the German paradigm of contracted against full preposition-article forms and masked in English by the syncretic the. Both articles are evaluated at a resource situation; the strong article additionally takes an anaphoric index, so the weak article's referent is the unique satisfier at the situation and covaries with it (weak_article_referent_iff, weak_article_covaries), while the strong article's referent is the antecedent wherever it is defined and does not (strong_article_referent_iff, strong_article_rigid). The German inventory marks the two strengths with distinct forms and the English one with a single form (german_two_articles, english_syncretic_articles, strategy_split). The two articles can disagree on a referent in one context: over a restrictor with two satisfiers the weak article fails uniqueness and the strong article returns its antecedent (weak_article_fails_on_multi, strong_article_picks_indexed_antecedent, two_articles_can_disagree).

References

• [Sch09b]
• [Sch13]
• [CB15]
• [PGG17]

The two articles take different arguments

theorem Schwarz2009.weak_article_referent_iff {E W : Type} (R : Reference.Restrictor E W) (g : Assignment E) (s : W) (x : E) : Semantics.Denotes.denote (Reference.Description.unique R) g s = some x ↔ R g s x ∧ ∀ (y : E), R g s y → y = x

The weak article denotes x at a situation iff x is the unique satisfier of the restrictor there: the situation fixes the referent.

theorem Schwarz2009.strong_article_referent_iff {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) (g : Assignment E) (s : W) (x : E) : Semantics.Denotes.denote (Reference.Description.anaphoric R d) g s = some x ↔ R g s (g d) ∧ x = g d

The strong article denotes x at a situation iff x is its antecedent g d and the restrictor holds of the antecedent there: the index fixes the referent.

theorem Schwarz2009.strong_article_rigid {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) (g : Assignment E) {s s' : W} {x x' : E} (h : Semantics.Denotes.denote (Reference.Description.anaphoric R d) g s = some x) (h' : Semantics.Denotes.denote (Reference.Description.anaphoric R d) g s' = some x') : x = x'

The strong article's referent does not covary with the resource situation.

The morphological correlate

theorem Schwarz2009.german_two_articles : German.Determiners.inventory.Marks Reference.Description.Strength.uniqueness ∧ German.Determiners.inventory.Marks Reference.Description.Strength.familiarity ∧ ¬German.Determiners.inventory.IsSyncretic

German marks both strengths, with distinct forms.

theorem Schwarz2009.english_syncretic_articles : English.Determiners.inventory.Marks Reference.Description.Strength.uniqueness ∧ English.Determiners.inventory.Marks Reference.Description.Strength.familiarity ∧ English.Determiners.inventory.IsSyncretic

English marks both strengths with the one syncretic form the.

theorem Schwarz2009.strategy_split : German.Determiners.inventory.markingStrategy = Reference.MarkingStrategy.bipartite ∧ English.Determiners.inventory.markingStrategy = Reference.MarkingStrategy.generallyMarked

German is bipartite and English generally marked: the same two strengths, distinguished at the surface in one language and not the other.

The two articles pick different referents

inductive Schwarz2009.Student : Type

Two students.

• alice : Student
• bob : Student

@[instance_reducible]

instance Schwarz2009.instDecidableEqStudent : DecidableEq Student

Equations

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

@[instance_reducible]

instance Schwarz2009.instReprStudent : Repr Student

Equations

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

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✝

def Schwarz2009.studentRestr : Reference.Restrictor Student Bool

Both students count as students at every situation, so the restrictor has two satisfiers and the weak article fails uniqueness.

Equations

• Schwarz2009.studentRestr x✝² x✝¹ x✝ = True

def Schwarz2009.gAlice : Assignment Student

The discourse referent at index 0 is Alice.

Equations

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

theorem Schwarz2009.weak_article_fails_on_multi (s : Bool) : Semantics.Denotes.denote (Reference.Description.unique studentRestr) gAlice s = none

The weak article fails on a restrictor with two satisfiers.

theorem Schwarz2009.strong_article_picks_indexed_antecedent (s : Bool) : Semantics.Denotes.denote (Reference.Description.anaphoric studentRestr 0) gAlice s = some Student.alice

The strong article returns its antecedent however many entities satisfy the restrictor.

theorem Schwarz2009.two_articles_can_disagree (s : Bool) : Semantics.Denotes.denote (Reference.Description.unique studentRestr) gAlice s ≠ Semantics.Denotes.denote (Reference.Description.anaphoric studentRestr 0) gAlice s

The two articles disagree on a referent in the same context: the semantic counterpart of the German morphological split.

def Schwarz2009.mayorRestr : Reference.Restrictor Student Bool

A restrictor whose unique satisfier differs between two situations, the mayor across towns.

Equations

• Schwarz2009.mayorRestr x✝ s x = (x = if s = true then Schwarz2009.Student.alice else Schwarz2009.Student.bob)

theorem Schwarz2009.weak_article_covaries : Semantics.Denotes.denote (Reference.Description.unique mayorRestr) gAlice true = some Student.alice ∧ Semantics.Denotes.denote (Reference.Description.unique mayorRestr) gAlice false = some Student.bob

The weak article covaries with the resource situation: over mayorRestr it picks Alice in one situation and Bob in the other, the covarying larger-situation uses that the strong article lacks (strong_article_rigid).