Cooper (2023) Ch. 8 — Type-Based Underspecification

@cite{cooper-2023} @cite{chomsky-1981} @cite{kanazawa-1994} @cite{scontras-pearl-2021}

@cite{cooper-2023} Chapter 8 introduces content types that replace specific contents with types whose witnesses are fully specified readings.

This study formalises Ch. 8 directly. It was formerly substrate at Theories/Semantics/TypeTheoretic/Underspecification.lean but is genuinely a single-paper Cooper-textbook replication: only the sibling Phenomena/Anaphora/Studies/Cooper2023.lean (bridge theorems to anaphora data) consumed it externally. Companion to Cooper2023.lean in the same directory.

Simplified semantic interface (used by bridge theorems)

1. Scope ambiguity: QStore, store/retrieve, 𝔖 (underspecification closure)
2. Donkey anaphora: localization 𝔏/𝔏ʸ/𝔏ᶜ (= purification 𝔓/𝔓ʸ from Ch7)
3. Binding theory: reflexivization ℜ, anaphoric resolution @_{i,j}
4. Conditional localization: 𝔏ᶜ for the correct strong donkey reading

Full Ch8 context machinery (eqs 10→74→82→89)

5. Cntxt₈: full 7-field context (q, 𝔰, 𝔩, 𝔯, 𝔴, 𝔤, 𝔠)
6. B (eq 77): boundary operation removing locality at clause boundaries
7. 𝔄 (eq 85): anaphor-free filter via r-field checking
8. ℜ₈ (eq 84): full reflexivization on Cntxt₈
9. @_{i,j} with l-field (eq 76): locality-aware anaphoric combination
10. UnderspecClosure₈ (eq 89): generalized 𝔖 with 7 closure clauses
11. NQuantScope: N-quantifier scope generalization (N! readings)
12. Cross-sentential anaphora (eqs 37-44): discourse merge
13. Donkey + negation (eqs 46-55): path alignment, "no" quantifier

Bridge theorems

1. tagged_roundtrip — 𝔖 witnesses ↔ ScopeConfig
2. localize := purify (Ch8 ↔ Ch7) — true by abbreviation, not a theorem
3. reflexivize₈_agrees_with_simple — full ℜ₈ ↔ simplified ℜ
4. twoQuant_embeds_in_closure — TwoQuantScope.𝔖 embeds in UnderspecClosure₈
5. donkeyNeg_uses_localization — negation donkey uses 𝔏

Key connections

• QStore.isPlugged bridges to Parametric.trivial (no pending scope)
• Scope witnesses bridge to ParticularWC_Exist / existPQ (Ch7)
• TwoQuantScope.𝔖 bridges to ScopeConfig
• crossSententialResolve bridges discourse merge to pronoun resolution

Quantifier stores

A quantifier store holds quantifiers that have been "tucked away" during composition and await scope assignment via retrieval.

structure Studies.Anaphora.Cooper2023.Ch8.QStore (E : Type) : Type 1

A quantifier store: a list of quantifiers awaiting scope resolution. Ch8 §8.3: stored quantifiers are later retrieved at scope positions, and retrieval order determines scope.

• stored : List (Semantics.TypeTheoretic.Quant E)

  The stored quantifiers, ordered by storage time

def Studies.Anaphora.Cooper2023.Ch8.QStore.empty {E : Type} : QStore E

Empty quantifier store: no pending scope ambiguity.

Equations

• Studies.Anaphora.Cooper2023.Ch8.QStore.empty = { stored := [] }

def Studies.Anaphora.Cooper2023.Ch8.QStore.isPlugged {E : Type} (qs : QStore E) : Prop

A store is plugged when all quantifiers have taken scope. Ch8: plugged content is fully scope-resolved.

Equations

• qs.isPlugged = (qs.stored = [])

def Studies.Anaphora.Cooper2023.Ch8.QStore.isUnplugged {E : Type} (qs : QStore E) : Prop

A store is unplugged when quantifiers remain to be scoped.

Equations

• qs.isUnplugged = (qs.stored ≠ [])

theorem Studies.Anaphora.Cooper2023.Ch8.plugged_iff_not_unplugged {E : Type} (qs : QStore E) : qs.isPlugged ↔ ¬qs.isUnplugged

Plugged ↔ ¬ unplugged.

theorem Studies.Anaphora.Cooper2023.Ch8.empty_isPlugged {E : Type} : QStore.empty.isPlugged

The empty store is plugged by construction.

def Studies.Anaphora.Cooper2023.Ch8.pluggedToTrivial {E : Type} {C : Type u_1} (c : C) (qs : QStore E) (_h : qs.isPlugged) : Semantics.TypeTheoretic.Parametric C

Bridge: a plugged QStore corresponds to a trivial Parametric background. When the store is empty, the content has no scope presuppositions — just like Parametric.trivial has Bg = Unit.

Equations

• Studies.Anaphora.Cooper2023.Ch8.pluggedToTrivial c qs _h = Semantics.TypeTheoretic.Parametric.trivial c

Store

Store moves a quantifier from content into the qstore, leaving behind a variable (trace) in the content.

def Studies.Anaphora.Cooper2023.Ch8.QStore.store {E : Type} (qs : QStore E) (q : Semantics.TypeTheoretic.Quant E) : QStore E

Store a quantifier: push it onto the front of the store. Ch8 §8.3: store(Q) moves Q into the qstore.

Equations

• qs.store q = { stored := q :: qs.stored }

theorem Studies.Anaphora.Cooper2023.Ch8.store_unplugs {E : Type} (q : Semantics.TypeTheoretic.Quant E) : (QStore.empty.store q).isUnplugged

Storing into a plugged store makes it unplugged.

Retrieve

Retrieve pops a quantifier from the store and applies it at a scope position. The order of retrieval determines relative scope.

def Studies.Anaphora.Cooper2023.Ch8.QStore.retrieve {E : Type} (qs : QStore E) : Option (Semantics.TypeTheoretic.Quant E × QStore E)

Retrieve the first quantifier from the store. Ch8 §8.3: retrieve pops the outermost stored quantifier. Returns the quantifier and the remaining store, or none if plugged.

Equations

• qs.retrieve = match qs.stored with | [] => none | q :: rest => some (q, { stored := rest })

theorem Studies.Anaphora.Cooper2023.Ch8.retrieve_none_iff_plugged {E : Type} (qs : QStore E) : qs.retrieve = none ↔ qs.isPlugged

Retrieve returns none iff the store is plugged.

theorem Studies.Anaphora.Cooper2023.Ch8.store_then_retrieve {E : Type} (qs : QStore E) (q : Semantics.TypeTheoretic.Quant E) : (qs.store q).retrieve = some (q, qs)

Store then retrieve recovers the stored quantifier.

Two-quantifier scope

For sentences with two quantifiers and a binary relation, the two possible retrieval orders produce exactly two scope readings. Ch8: "every boy hugged a dog" has ∀>∃ and ∃>∀ readings.

structure Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope (E : Type) : Type 1

A two-quantifier scope configuration: two quantifiers and a relation. Ch8: the minimal underspecified content for a doubly-quantified sentence.

• rel : E → E → Type

  The binary relation (e.g., hug)

• q₁ : Semantics.TypeTheoretic.Quant E

  The subject quantifier (e.g., every boy)

• q₂ : Semantics.TypeTheoretic.Quant E

  The object quantifier (e.g., a dog)

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.surfaceScope {E : Type} (s : TwoQuantScope E) : Type

Surface scope reading: Q₁ scopes over Q₂. Ch8: retrieving Q₁ first = outermost scope. For "every boy hugged a dog": ∀x.boy(x) → ∃y.dog(y) ∧ hug(x,y).

Equations

• s.surfaceScope = s.q₁ fun (x : E) => s.q₂ fun (y : E) => s.rel x y

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.inverseScope {E : Type} (s : TwoQuantScope E) : Type

Inverse scope reading: Q₂ scopes over Q₁. For "every boy hugged a dog": ∃y.dog(y) ∧ ∀x.boy(x) → hug(x,y).

Equations

• s.inverseScope = s.q₂ fun (y : E) => s.q₁ fun (x : E) => s.rel x y

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.𝔖 {E : Type} (s : TwoQuantScope E) : Type

The underspecification closure 𝔖 for two quantifiers: the join of all possible scope readings. Ch8 §8.4: each witness of 𝔖(content) is one fully specified reading. With two quantifiers, |𝔖| = 2.

Equations

• s.𝔖 = Semantics.TypeTheoretic.JoinType s.surfaceScope s.inverseScope

theorem Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.𝔖_iff {E : Type} (s : TwoQuantScope E) : Semantics.TypeTheoretic.IsTrue s.𝔖 ↔ Semantics.TypeTheoretic.IsTrue s.surfaceScope ∨ Semantics.TypeTheoretic.IsTrue s.inverseScope

𝔖 is inhabited iff at least one scope reading is true.

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.surfaceToUnderspec {E : Type} (s : TwoQuantScope E) (w : s.surfaceScope) : s.𝔖

A surface scope witness embeds into 𝔖.

Equations

• s.surfaceToUnderspec w = Sum.inl w

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.inverseToUnderspec {E : Type} (s : TwoQuantScope E) (w : s.inverseScope) : s.𝔖

An inverse scope witness embeds into 𝔖.

Equations

• s.inverseToUnderspec w = Sum.inr w

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.readingAt {E : Type} (s : TwoQuantScope E) (sc : Semantics.Scope.ScopeConfig) : Type

Select a scope reading by ScopeConfig. Ch8 → @cite{scontras-pearl-2021} bridge: retrieval order corresponds to ScopeConfig.surface /.inverse.

Equations

• s.readingAt Semantics.Scope.ScopeConfig.surface = s.surfaceScope
• s.readingAt Semantics.Scope.ScopeConfig.inverse = s.inverseScope

Bridge: underspec witnesses match scope readings

The witnesses of 𝔖(content) are in bijection with the scope orderings predicted by retrieve. Each ScopeConfig selects one reading, and every witness of 𝔖 comes from exactly one reading.

This connects TTR's type-based underspecification to the ScopeConfig infrastructure used by @cite{scontras-pearl-2021} in the RSA implementation.

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.𝔖_to_tagged {E : Type} (s : TwoQuantScope E) (w : s.𝔖) : (sc : Semantics.Scope.ScopeConfig) × s.readingAt sc

Forward direction: every witness of 𝔖 is tagged by a ScopeConfig.

Equations

• s.𝔖_to_tagged (Sum.inl surf) = ⟨Semantics.Scope.ScopeConfig.surface, surf⟩
• s.𝔖_to_tagged (Sum.inr inv) = ⟨Semantics.Scope.ScopeConfig.inverse, inv⟩

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.tagged_to_𝔖 {E : Type} (s : TwoQuantScope E) (tagged : (sc : Semantics.Scope.ScopeConfig) × s.readingAt sc) : s.𝔖

Backward direction: a tagged reading embeds into 𝔖.

Equations

• s.tagged_to_𝔖 tagged = match tagged.fst, tagged.snd with | Semantics.Scope.ScopeConfig.surface, w => Sum.inl w | Semantics.Scope.ScopeConfig.inverse, w => Sum.inr w

theorem Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.tagged_roundtrip {E : Type} (s : TwoQuantScope E) (tagged : (sc : Semantics.Scope.ScopeConfig) × s.readingAt sc) : s.𝔖_to_tagged (s.tagged_to_𝔖 tagged) = tagged

Round-trip: tagged → 𝔖 → tagged is the identity. This is the bijection theorem connecting Ch8's 𝔖 to ScopeConfig.

Scope ambiguity in "every boy hugged a dog"

Ch8: the classic scope ambiguity example. Two boys, two dogs; each boy hugs a different dog. Surface scope is true but inverse scope is false.

inductive Studies.Anaphora.Cooper2023.Ch8.ScopeInd : Type

Individuals for the scope example.

• tom : ScopeInd
• bill : ScopeInd
• fido : ScopeInd
• rex : ScopeInd

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instDecidableEqScopeInd : DecidableEq ScopeInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instDecidableEqScopeInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instReprScopeInd : Repr ScopeInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instReprScopeInd = { reprPrec := Studies.Anaphora.Cooper2023.Ch8.instReprScopeInd.repr }

def Studies.Anaphora.Cooper2023.Ch8.instReprScopeInd.repr : ScopeInd → ℕ → Std.Format

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.isBoy : Semantics.TypeTheoretic.Ppty ScopeInd

Boy predicate: Tom and Bill are boys.

Equations

• Studies.Anaphora.Cooper2023.Ch8.isBoy Studies.Anaphora.Cooper2023.Ch8.ScopeInd.tom = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isBoy Studies.Anaphora.Cooper2023.Ch8.ScopeInd.bill = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isBoy x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.isDog₈ : Semantics.TypeTheoretic.Ppty ScopeInd

Dog predicate: Fido and Rex are dogs.

Equations

• Studies.Anaphora.Cooper2023.Ch8.isDog₈ Studies.Anaphora.Cooper2023.Ch8.ScopeInd.fido = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isDog₈ Studies.Anaphora.Cooper2023.Ch8.ScopeInd.rex = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isDog₈ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.hugs : ScopeInd → ScopeInd → Type

Hug predicate: Tom hugs Fido, Bill hugs Rex. This scenario makes surface scope true but inverse scope false: every boy hugged A dog (different dogs), but no single dog was hugged by every boy.

Equations

• Studies.Anaphora.Cooper2023.Ch8.hugs Studies.Anaphora.Cooper2023.Ch8.ScopeInd.tom Studies.Anaphora.Cooper2023.Ch8.ScopeInd.fido = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.hugs Studies.Anaphora.Cooper2023.Ch8.ScopeInd.bill Studies.Anaphora.Cooper2023.Ch8.ScopeInd.rex = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.hugs x✝¹ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.everyBoy : Semantics.TypeTheoretic.Quant ScopeInd

The universal quantifier for boys.

Equations

• Studies.Anaphora.Cooper2023.Ch8.everyBoy = Semantics.TypeTheoretic.semUniversal Studies.Anaphora.Cooper2023.Ch8.isBoy

def Studies.Anaphora.Cooper2023.Ch8.aDog : Semantics.TypeTheoretic.Quant ScopeInd

The existential quantifier for dogs.

Equations

• Studies.Anaphora.Cooper2023.Ch8.aDog = Semantics.TypeTheoretic.semIndefArt Studies.Anaphora.Cooper2023.Ch8.isDog₈

def Studies.Anaphora.Cooper2023.Ch8.everyBoyHuggedADog : TwoQuantScope ScopeInd

The two-quantifier scope configuration for "every boy hugged a dog".

Equations

• Studies.Anaphora.Cooper2023.Ch8.everyBoyHuggedADog = { rel := Studies.Anaphora.Cooper2023.Ch8.hugs, q₁ := Studies.Anaphora.Cooper2023.Ch8.everyBoy, q₂ := Studies.Anaphora.Cooper2023.Ch8.aDog }

def Studies.Anaphora.Cooper2023.Ch8.surfaceScopeWitness : everyBoyHuggedADog.surfaceScope

Surface scope witness: every boy hugged a (possibly different) dog. Tom→Fido, Bill→Rex.

Equations

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

theorem Studies.Anaphora.Cooper2023.Ch8.no_inverse_scope : Semantics.TypeTheoretic.IsFalse everyBoyHuggedADog.inverseScope

Inverse scope fails: no single dog was hugged by every boy.

def Studies.Anaphora.Cooper2023.Ch8.underspecInhabited : everyBoyHuggedADog.𝔖

𝔖 is inhabited (via the surface scope reading).

Equations

• Studies.Anaphora.Cooper2023.Ch8.underspecInhabited = Studies.Anaphora.Cooper2023.Ch8.everyBoyHuggedADog.surfaceToUnderspec Studies.Anaphora.Cooper2023.Ch8.surfaceScopeWitness

theorem Studies.Anaphora.Cooper2023.Ch8.only_surface_in_scenario : Semantics.TypeTheoretic.IsTrue everyBoyHuggedADog.𝔖 ∧ ¬Semantics.TypeTheoretic.IsTrue everyBoyHuggedADog.inverseScope

The surface reading is the only true reading in this scenario.

theorem Studies.Anaphora.Cooper2023.Ch8.underspec_tagged_is_surface : (everyBoyHuggedADog.𝔖_to_tagged underspecInhabited).fst = Semantics.Scope.ScopeConfig.surface

The scope reading is correctly identified as surface via tagging.

Bridge: scope readings → witness conditions

The connection between Ch8's scope readings and Ch7's witness conditions: a surface scope reading with a universal subject and existential object corresponds to per-element ParticularWC_Exist conditions, yielding REFSET anaphora for the object NP.

"Every boy hugged a dog. It was friendly." → "it" picks up one dog per boy (distributive anaphora, REFSET).

def Studies.Anaphora.Cooper2023.Ch8.surfaceScope_inner_witness {E : Type} (P Q : Semantics.TypeTheoretic.Ppty E) (R : E → E → Type) (w : Semantics.TypeTheoretic.semUniversal P fun (x : E) => Semantics.TypeTheoretic.ExistWitness E Q fun (y : E) => R x y) (x : E) (hP : P x) : Phenomena.Quantification.Studies.Cooper2023.ParticularWC_Exist Q fun (y : E) => R x y

Bridge: a surface scope witness (∀x.P(x) → ∃y.Q(y) ∧ R(x,y)) yields a ParticularWC_Exist for the inner existential at each fixed subject.

Cooper Ch8→Ch7: the inner quantifier's witness condition is exactly ParticularWC_Exist, predicting REFSET anaphora for the object.

Equations

• Studies.Anaphora.Cooper2023.Ch8.surfaceScope_inner_witness P Q R w x hP = { x := (w x hP).individual, pWit := (w x hP).restrWit, qWit := (w x hP).scopeWit }

def Studies.Anaphora.Cooper2023.Ch8.inverseScope_outer_witness {E : Type} (P Q : Semantics.TypeTheoretic.Ppty E) (R : E → E → Type) (w : Semantics.TypeTheoretic.ExistWitness E Q fun (y : E) => Semantics.TypeTheoretic.semUniversal P fun (x : E) => R x y) : Phenomena.Quantification.Studies.Cooper2023.ParticularWC_Exist Q fun (y : E) => Semantics.TypeTheoretic.semUniversal P fun (x : E) => R x y

Bridge: an inverse scope witness (∃y.Q(y) ∧ ∀x.P(x) → R(x,y)) yields a ParticularWC_Exist for the outer existential — there is ONE specific entity witnessing Q that the universal scopes under.

"A dog was hugged by every boy. It was large." → "it" picks up the specific dog (REFSET from outer scope).

Equations

• Studies.Anaphora.Cooper2023.Ch8.inverseScope_outer_witness P Q R w = { x := w.individual, pWit := w.restrWit, qWit := w.scopeWit }

theorem Studies.Anaphora.Cooper2023.Ch8.surface_scope_matches_existPQ {E : Type} (P Q : Semantics.TypeTheoretic.Ppty E) (R : E → E → Type) (w : Semantics.TypeTheoretic.semUniversal P fun (x : E) => Semantics.TypeTheoretic.ExistWitness E Q fun (y : E) => R x y) (x : E) : Nonempty (P x) → Semantics.TypeTheoretic.existPQ Q (R x)

Bridge: surface scope (semUniversal + ExistWitness) matches existPQ at each individual — the Ch7 existential predicate overlap.

Cooper Ch8→Ch7: scope retrieval order determines which witness conditions hold per quantifier position.

Localization

Ch8 §8.5: localization moves a stored quantifier's background into the domain of a property, absorbing the context dependency. This is the Ch8 mechanism for donkey anaphora:

"Every farmer who owns a donkey beats it" → "a donkey" is stored, then localized into the restrictor "farmer who owns a donkey", binding the donkey existentially (weak) or universally (strong) inside the property body.

The central insight: this is the same operation as Ch7's purification.

@[reducible, inline]

abbrev Studies.Anaphora.Cooper2023.Ch8.localize {E : Type} : Semantics.TypeTheoretic.PPpty E → Semantics.TypeTheoretic.Ppty E

Localization: absorb a parametric property's background into its body. Ch8 §8.5: 𝔏(P) moves context material into the property's domain type, enabling donkey anaphora. Before 𝔏: restrictor is parametric (depends on which donkey). After 𝔏: restrictor is pure (donkey existentially bound inside).

Cooper §8.5 identifies 𝔏 with the Ch. 7 purification operator 𝔓 (the same Σ-absorption of a parametric background into the property body). We encode the identification as abbrev so that Ch7 lemmas about purification automatically discharge Ch8 obligations about localization — the cross-chapter unification is true by construction, not a separate bridge theorem.

Equations

• Studies.Anaphora.Cooper2023.Ch8.localize = Phenomena.Quantification.Studies.Cooper2023.purify

@[reducible, inline]

abbrev Studies.Anaphora.Cooper2023.Ch8.localizeUniv {E : Type} : Semantics.TypeTheoretic.PPpty E → Semantics.TypeTheoretic.Ppty E

Universal localization: strong-donkey variant. Identical to Ch7's 𝔓ʸ.

Equations

• Studies.Anaphora.Cooper2023.Ch8.localizeUniv = Phenomena.Quantification.Studies.Cooper2023.purifyUniv

def Studies.Anaphora.Cooper2023.Ch8.term𝔏_ : Lean.ParserDescr

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.«term𝔏ʸ_» : Lean.ParserDescr

Equations

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

Localization lemmas (inherited from Ch7 purification)

Because localize := purify and localizeUniv := purifyUniv, all witness-existence lemmas about purification carry over via Iff.rfl-style aliases. Cooper's claim that "the Ch8 localization mechanism is the Ch7 purification mechanism" is now true by construction.

theorem Studies.Anaphora.Cooper2023.Ch8.localize_nonempty_iff {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (a : E) : Nonempty (localize P a) ↔ ∃ (c : P.Bg), Nonempty (P.fg c a)

Localization preserves truth: a localized property is witnessed iff the original is witnessable under some context.

theorem Studies.Anaphora.Cooper2023.Ch8.localizeUniv_nonempty_iff {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (a : E) : Nonempty (localizeUniv P a) ↔ ∀ (c : P.Bg), Nonempty (P.fg c a)

Universal localization: witnessed iff property holds under all contexts.

theorem Studies.Anaphora.Cooper2023.Ch8.localize_trivial {E : Type} (P : Semantics.TypeTheoretic.Ppty E) (a : E) : localize (Semantics.TypeTheoretic.Parametric.trivial P) a = ((_ : Unit) × P a)

Localizing a trivial parametric property adds only a Unit factor.

theorem Studies.Anaphora.Cooper2023.Ch8.localization_readings_agree_when_pure {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (hPure : Phenomena.Quantification.Studies.Cooper2023.PPpty.isPure P) (a : E) : Nonempty (localize P a) ↔ Nonempty (localizeUniv P a)

Bridge: weak and strong donkey readings agree when the parametric background is trivial. Corollary of donkey_readings_agree_when_pure.

"Every farmer who owns a donkey beats it"

The classic donkey anaphora example. Two farmers, two donkeys; each farmer owns and beats a different donkey. This demonstrates:

1. Localization absorbs "a donkey" into the restrictor
2. Weak donkey (𝔏 = 𝔓) is true — each farmer owns/beats some donkey
3. Strong donkey (𝔏ʸ = 𝔓ʸ) fails — no farmer owns/beats every donkey
4. The divergence witnesses the non-triviality of donkey_readings_agree_when_pure

inductive Studies.Anaphora.Cooper2023.Ch8.DonkeyInd : Type

Individuals for the donkey example.

• farmer1 : DonkeyInd
• farmer2 : DonkeyInd
• donkey1 : DonkeyInd
• donkey2 : DonkeyInd

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instDecidableEqDonkeyInd : DecidableEq DonkeyInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instDecidableEqDonkeyInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Studies.Anaphora.Cooper2023.Ch8.instReprDonkeyInd.repr : DonkeyInd → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instReprDonkeyInd : Repr DonkeyInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instReprDonkeyInd = { reprPrec := Studies.Anaphora.Cooper2023.Ch8.instReprDonkeyInd.repr }

def Studies.Anaphora.Cooper2023.Ch8.isFarmer : Semantics.TypeTheoretic.Ppty DonkeyInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.isFarmer Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.farmer1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isFarmer Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.farmer2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isFarmer x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.isDonkey₈ : Semantics.TypeTheoretic.Ppty DonkeyInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.isDonkey₈ Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.donkey1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isDonkey₈ Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.donkey2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isDonkey₈ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.owns : DonkeyInd → DonkeyInd → Type

Ownership: farmer1 owns donkey1, farmer2 owns donkey2.

Equations

• Studies.Anaphora.Cooper2023.Ch8.owns Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.farmer1 Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.donkey1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.owns Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.farmer2 Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.donkey2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.owns x✝¹ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.beats : DonkeyInd → DonkeyInd → Type

Beating: each farmer beats the donkey they own.

Equations

• Studies.Anaphora.Cooper2023.Ch8.beats Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.farmer1 Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.donkey1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.beats Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.farmer2 Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.donkey2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.beats x✝¹ x✝ = Empty

@[reducible, inline]

abbrev Studies.Anaphora.Cooper2023.Ch8.DonkeyBg : Type

Background type: a donkey that exists.

Equations

• Studies.Anaphora.Cooper2023.Ch8.DonkeyBg = ((d : Studies.Anaphora.Cooper2023.Ch8.DonkeyInd) × Studies.Anaphora.Cooper2023.Ch8.isDonkey₈ d)

def Studies.Anaphora.Cooper2023.Ch8.farmerOwnsBeatsDonkey : Semantics.TypeTheoretic.PPpty DonkeyInd

The parametric property "farmer who owns a donkey [and beats it]". Background: a specific donkey d. Foreground: given d, x is a farmer who owns d and beats d.

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.farmer1_weak_donkey : localize farmerOwnsBeatsDonkey DonkeyInd.farmer1

Farmer1 satisfies the weak donkey reading: owns and beats donkey1.

Equations

• Studies.Anaphora.Cooper2023.Ch8.farmer1_weak_donkey = ⟨⟨Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.donkey1, PUnit.unit⟩, (PUnit.unit, PUnit.unit, PUnit.unit)⟩

def Studies.Anaphora.Cooper2023.Ch8.farmer2_weak_donkey : localize farmerOwnsBeatsDonkey DonkeyInd.farmer2

Farmer2 satisfies the weak donkey reading: owns and beats donkey2.

Equations

• Studies.Anaphora.Cooper2023.Ch8.farmer2_weak_donkey = ⟨⟨Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.donkey2, PUnit.unit⟩, (PUnit.unit, PUnit.unit, PUnit.unit)⟩

theorem Studies.Anaphora.Cooper2023.Ch8.farmer1_fails_strong_donkey : IsEmpty (localizeUniv farmerOwnsBeatsDonkey DonkeyInd.farmer1)

Strong donkey FAILS for farmer1: farmer1 doesn't own donkey2. This is the ∀-reading: every donkey d, farmer1 owns d ∧ beats d. Fails because farmer1 doesn't own donkey2.

theorem Studies.Anaphora.Cooper2023.Ch8.donkey_readings_diverge : Nonempty (localize farmerOwnsBeatsDonkey DonkeyInd.farmer1) ∧ ¬Nonempty (localizeUniv farmerOwnsBeatsDonkey DonkeyInd.farmer1)

Weak and strong donkey readings DIVERGE: weak is true, strong is false. This demonstrates that donkey_readings_agree_when_pure has a real hypothesis: when Bg is non-trivial (multiple donkeys), the readings genuinely differ.

def Studies.Anaphora.Cooper2023.Ch8.everyFarmerBeatsDonkey_weak : Semantics.TypeTheoretic.semUniversal (localize farmerOwnsBeatsDonkey) fun (x : DonkeyInd) => PUnit.{1}

The full sentence "every farmer who owns a donkey beats it" is true under the weak donkey reading (via localization = purification).

Equations

• Studies.Anaphora.Cooper2023.Ch8.everyFarmerBeatsDonkey_weak Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.farmer1 x_2 = PUnit.unit
• Studies.Anaphora.Cooper2023.Ch8.everyFarmerBeatsDonkey_weak Studies.Anaphora.Cooper2023.Ch8.DonkeyInd.farmer2 x_2 = PUnit.unit

TODO: Cooper's correct strong-donkey reading via 𝔓^∀

The previous formalisation here (localizeConditional + beatsParam + ownsGate + strongDonkeyConditional + farmer{1,2}_strong_conditional) was a formaliser-invented "conditional gate" mechanism attributing @cite{kanazawa-1994}'s strong-donkey reading to a third operator beyond 𝔏 and 𝔏ʸ. Cooper's own §8.5 solution is 𝔓^∀ over a parametric property whose background contains the ownership constraint (not 𝔏 + a separate gate). The current farmerOwnsBeatsDonkey puts ownership in the foreground, so 𝔓^∀ over it misfires — but restructuring the property so that Bg carries the owning relation (a per-farmer indexed background) lets 𝔓^∀ produce the correct prediction directly.

Audit-verified gap (linguistics-domain-expert vs Cooper 2023 PDF, §8.5): the correct strong-donkey reconstruction is deferred until the indexed-background machinery for per-entity Bg is in place.

Reflexivization and anaphoric operations

Ch8 introduces two operations for binding:

1. ℜ(P) (eq 84): Reflexivization — removes the reflexive marking (r-field) from the context and binds the reflexive pronoun to the subject variable in the domain of the property. Semantic effect: R(x,y) → R(x,x).

2. @_{i,j} (eq 28): Anaphoric combination — identifies assignment path j with path i, creating the anaphoric link between a pronoun and its antecedent. General mechanism for pronoun resolution.

The interplay creates complementary distribution:

• ℜ provides the mechanism for reflexives → they MUST be locally bound
• @_{i,j} with a constant resolve function gives disjoint reference for pronouns
• B (eq 77, not yet formalized) removes locality at clause boundaries

Key connections

• reflexivize (ℜ) bridges to CoreferencePattern.reflexivePattern (Phenomena)
• anaphoricResolve captures @_{i,j} resolution → pronounPattern
• reflexive_predicts_binding: the main bridge theorem (bridge theorem 3)

def Studies.Anaphora.Cooper2023.Ch8.reflexivize {E : Type} (R : E → E → Type) : Semantics.TypeTheoretic.Ppty E

Reflexivization: identify the two arguments of a binary relation. Ch8, eq (84): ℜ(P) removes the reflexive marking (r-field) from the context and replaces the dependency on the assignment variable 𝔤.xᵢ with the domain variable r.x.

Semantic effect: a transitive verb R(x,y) becomes a reflexive VP R(x,x), forcing the object to corefer with the subject. "Sam likes himself" = ℜ(like)(Sam) = like(Sam, Sam).

Equations

• Studies.Anaphora.Cooper2023.Ch8.reflexivize R x = R x x

def Studies.Anaphora.Cooper2023.Ch8.termℜ_ : Lean.ParserDescr

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.anaphoricResolve {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (resolve : E → P.Bg) : Semantics.TypeTheoretic.Ppty E

Anaphoric resolution: resolve a parametric property's background using a function of the foreground argument. Captures the semantic effect of Cooper's @{i,j} (eq 28): @{i,j} identifies path 𝔤.xⱼ with 𝔤.xᵢ, creating the anaphoric link.

• Reflexives: resolve = id (subject IS the referent) → same as ℜ
• Pronouns: resolve = const(g(i)) (assignment provides referent)

Equations

• Studies.Anaphora.Cooper2023.Ch8.anaphoricResolve P resolve x = P.fg (resolve x) x

theorem Studies.Anaphora.Cooper2023.Ch8.reflexivize_forces_identity {E : Type} (R : E → E → Type) (x : E) : reflexivize R x = R x x

ℜ forces argument identity: any witness of ℜ(R)(x) IS R(x,x). Cooper Ch8: the reflexive marking ensures the object slot is filled by the same individual as the subject.

theorem Studies.Anaphora.Cooper2023.Ch8.reflexivize_eq_resolve_id {E : Type} (R : E → E → Type) : reflexivize R = anaphoricResolve { Bg := E, fg := fun (y x : E) => R x y } id

ℜ is anaphoric resolution with identity: reflexivization is the special case where the background (object referent) is resolved to equal the foreground argument (subject). ℜ(R) = anaphoricResolve(⟨E, λy x. R(x,y)⟩, id).

theorem Studies.Anaphora.Cooper2023.Ch8.resolve_const {E : Type} (R : E → E → Type) (y x : E) : anaphoricResolve { Bg := E, fg := fun (obj subj : E) => R subj obj } (fun (x : E) => y) x = R x y

Pronoun resolution with constant: resolves to a fixed referent y regardless of the subject x. Captures @_{i,j} when the assignment g(i) = y is fixed from discourse context. "Sam likes him(=Bill)" = anaphoricResolve(like_param, const Bill)(Sam) = like(Sam, Bill).

Binding in "Sam likes himself" / "Sam likes him"

Ch8, eqs (67)–(73): "Sam likes him" has two fields x and y for individuals (68a). When y=x, the fields are filled by the same individual (68b,c). Reflexivization ℜ forces this identification.

The complementary distribution:

• "Sam likes himself" = ℜ(like)(Sam) = like(Sam, Sam) — coreference forced
• "Sam likes him(=Bill)" = anaphoricResolve(like_param, const Bill)(Sam) = like(Sam, Bill) — disjoint reference

inductive Studies.Anaphora.Cooper2023.Ch8.BindInd : Type

Individuals for the binding example. Ch8: Sam is the subject; Bill is a potential non-local antecedent for "him".

• sam : BindInd
• bill : BindInd
• kim : BindInd

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instDecidableEqBindInd : DecidableEq BindInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instDecidableEqBindInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Studies.Anaphora.Cooper2023.Ch8.instReprBindInd.repr : BindInd → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instReprBindInd : Repr BindInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instReprBindInd = { reprPrec := Studies.Anaphora.Cooper2023.Ch8.instReprBindInd.repr }

def Studies.Anaphora.Cooper2023.Ch8.like₈ : BindInd → BindInd → Type

"like" as a non-trivial binary relation. Sam likes everyone, Bill likes Kim and himself, Kim likes herself only. This makes binding witnesses non-trivially constrained: ℜ(like₈)(Kim) is inhabited but like₈.kim.sam is not, so reflexivization genuinely restricts which argument pairs are witnessable.

Equations

• Studies.Anaphora.Cooper2023.Ch8.like₈ Studies.Anaphora.Cooper2023.Ch8.BindInd.sam x✝ = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.like₈ Studies.Anaphora.Cooper2023.Ch8.BindInd.bill Studies.Anaphora.Cooper2023.Ch8.BindInd.bill = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.like₈ Studies.Anaphora.Cooper2023.Ch8.BindInd.bill Studies.Anaphora.Cooper2023.Ch8.BindInd.kim = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.like₈ Studies.Anaphora.Cooper2023.Ch8.BindInd.kim Studies.Anaphora.Cooper2023.Ch8.BindInd.kim = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.like₈ x✝¹ x✝ = Empty

theorem Studies.Anaphora.Cooper2023.Ch8.like₈_nontrivial : IsEmpty (like₈ BindInd.kim BindInd.sam)

like₈ is non-trivial: not everyone likes everyone.

def Studies.Anaphora.Cooper2023.Ch8.likeParam : Semantics.TypeTheoretic.PPpty BindInd

"like" as parametric content: the object comes from background. Cooper Ch8, eq (69): the verb phrase "likes him" has the object's referent in the context (𝔤.x₀).

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.samLikesHimself : reflexivize like₈ BindInd.sam

"Sam likes himself" via ℜ: Cooper Ch8, eq (84). ℜ(like)(Sam) = like(Sam, Sam).

Equations

• Studies.Anaphora.Cooper2023.Ch8.samLikesHimself = PUnit.unit

def Studies.Anaphora.Cooper2023.Ch8.samLikesBill : anaphoricResolve likeParam (fun (x : BindInd) => BindInd.bill) BindInd.sam

"Sam likes him(=Bill)" via pronoun resolution: Cooper Ch8, eq (72). @_{0,1}(Sam, likes him) resolves "him" to Bill from context.

Equations

• Studies.Anaphora.Cooper2023.Ch8.samLikesBill = PUnit.unit

theorem Studies.Anaphora.Cooper2023.Ch8.reflexive_is_self : reflexivize like₈ BindInd.sam = like₈ BindInd.sam BindInd.sam

ℜ forces coreference: the reflexive witness IS like(Sam, Sam).

theorem Studies.Anaphora.Cooper2023.Ch8.pronoun_is_distinct : anaphoricResolve likeParam (fun (x : BindInd) => BindInd.bill) BindInd.sam = like₈ BindInd.sam BindInd.bill

Pronoun resolution gives like(Sam, Bill) — distinct arguments.

def Studies.Anaphora.Cooper2023.Ch8.allLikeSelf (x : BindInd) : reflexivize like₈ x

Every individual can like themselves (ℜ always witnessable). Non-trivial: each case uses a different constructor witness.

Equations

• Studies.Anaphora.Cooper2023.Ch8.allLikeSelf Studies.Anaphora.Cooper2023.Ch8.BindInd.sam = PUnit.unit
• Studies.Anaphora.Cooper2023.Ch8.allLikeSelf Studies.Anaphora.Cooper2023.Ch8.BindInd.bill = PUnit.unit
• Studies.Anaphora.Cooper2023.Ch8.allLikeSelf Studies.Anaphora.Cooper2023.Ch8.BindInd.kim = PUnit.unit

theorem Studies.Anaphora.Cooper2023.Ch8.param_reflexivize_agrees : anaphoricResolve likeParam id = reflexivize like₈

ℜ applied to likeParam is the same as reflexivize applied to like₈. This shows the parametric and direct formulations agree.

theorem Studies.Anaphora.Cooper2023.Ch8.reflexive_constrains_kim : Nonempty (reflexivize like₈ BindInd.kim) ∧ IsEmpty (like₈ BindInd.kim BindInd.bill)

ℜ genuinely constrains: Kim can like herself (ℜ) but NOT Bill (pronoun resolution). This is non-trivial because like₈.kim.bill is Empty while like₈.kim.kim is PUnit.

Bridge to positional binding interface

Connect TTR's semantic binding (ℜ / @_{i,j}) to the syntactic binding interface in Theories.Interfaces.SyntaxSemantics.Binding.

TTR's binding theory is semantic (argument identification via types), while BindingSemantics is syntactic (position-based binder–bindee relations). The bridge maps:

• ℜ applied → BindingRelation with subject as binder, object as bindee
• @_{i,j} resolution (pronoun) → free variable in the BindingConfig

def Studies.Anaphora.Cooper2023.Ch8.reflexivize_to_binding (subjectPos objectPos : Interfaces.BindingSemantics.Position) : Interfaces.BindingSemantics.BindingRelation

ℜ induces a binding relation: subject binds the reflexive object. Cooper Ch8, (81): S → NP VP | B(NP'(@VP')). The subject at position 0 binds "himself" at position 2.

Equations

• Studies.Anaphora.Cooper2023.Ch8.reflexivize_to_binding subjectPos objectPos = { binder := subjectPos, bindee := objectPos, varIndex := 0 }

def Studies.Anaphora.Cooper2023.Ch8.reflexiveBindingConfig : Interfaces.BindingSemantics.BindingConfig

Binding config for "Sam likes himself": one local binding.

Equations

• Studies.Anaphora.Cooper2023.Ch8.reflexiveBindingConfig = { bindings := [Studies.Anaphora.Cooper2023.Ch8.reflexivize_to_binding { index := 0 } { index := 2 }], freeVariables := [] }

theorem Studies.Anaphora.Cooper2023.Ch8.reflexive_config_wellFormed : reflexiveBindingConfig.wellFormed = true

The reflexive binding config is well-formed: no double binding, no self-binding, consistent indices.

def Studies.Anaphora.Cooper2023.Ch8.pronominalBindingConfig : Interfaces.BindingSemantics.BindingConfig

Binding config for "Sam likes him": no local bindings, the pronoun at position 2 is a free variable.

Equations

• Studies.Anaphora.Cooper2023.Ch8.pronominalBindingConfig = { bindings := [], freeVariables := [({ index := 2 }, 0)] }

theorem Studies.Anaphora.Cooper2023.Ch8.pronominal_no_local_binding : pronominalBindingConfig.bindings = []

The pronominal config has no local bindings (Condition B).

theorem Studies.Anaphora.Cooper2023.Ch8.binding_mechanism_determines_config : reflexiveBindingConfig.bindings.length = 1 ∧ pronominalBindingConfig.bindings.length = 0

Bridge: TTR ℜ maps to a non-trivial binding config (one binding), while @{i,j} pronoun resolution maps to an empty binding config. The semantic mechanism (ℜ vs @{i,j}) determines the syntactic binding structure.

Full Ch8 context

Context evolves: eq 10 {q,𝔰,𝔴,𝔤,𝔠} → eq 74 adds 𝔩 → eq 82 adds 𝔯. Cntxt₈ encodes eq 82 (final). Earlier versions recoverable via 𝔩 := empty / 𝔯 := empty. Extends CntxtFull (Ch7, eq 122) with q/𝔩/𝔯.

structure Studies.Anaphora.Cooper2023.Ch8.Cntxt₈ (E : Type) : Type 1

Ch8 context, eq (82).

• q : QStore E
• 𝔰 : Semantics.TypeTheoretic.Assgnmnt E
• 𝔩 : Semantics.TypeTheoretic.Assgnmnt E
• 𝔯 : Semantics.TypeTheoretic.Assgnmnt E
• 𝔴 : Semantics.TypeTheoretic.Assgnmnt E
• 𝔤 : Semantics.TypeTheoretic.Assgnmnt E
• 𝔠 : Semantics.TypeTheoretic.PropCntxt

def Studies.Anaphora.Cooper2023.Ch8.Cntxt₈.initial {E : Type} : Cntxt₈ E

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.Cntxt₈.isEq10 {E : Type} (c : Cntxt₈ E) : Prop

Eq 10 context: 𝔩 and 𝔯 both empty.

Equations

• c.isEq10 = ((∀ (i : ℕ), c.𝔩 i = none) ∧ ∀ (i : ℕ), c.𝔯 i = none)

def Studies.Anaphora.Cooper2023.Ch8.Cntxt₈.isEq74 {E : Type} (c : Cntxt₈ E) : Prop

Eq 74 context: 𝔯 empty.

Equations

• c.isEq74 = ∀ (i : ℕ), c.𝔯 i = none

theorem Studies.Anaphora.Cooper2023.Ch8.Cntxt₈.initial_isEq10 {E : Type} : initial.isEq10

def Studies.Anaphora.Cooper2023.Ch8.boundary₈ {E : Type} (P : Cntxt₈ E → Type) : Cntxt₈ E → Type

B(α): boundary operation, eq (77). Resets l-field at clause boundaries.

Equations

• Studies.Anaphora.Cooper2023.Ch8.boundary₈ P c = P { q := c.q, 𝔰 := c.𝔰, 𝔩 := Core.PartialAssign.empty, 𝔯 := c.𝔯, 𝔴 := c.𝔴, 𝔤 := c.𝔤, 𝔠 := c.𝔠 }

def Studies.Anaphora.Cooper2023.Ch8.anaphoricCombine₈ {E : Type} [Inhabited E] (i j : ℕ) (P Q : Cntxt₈ E → Type) : Cntxt₈ E → Type

@_{i,j} with locality check, eq (76). Identifies 𝔰.xⱼ with 𝔰.xᵢ only when 𝔰.xᵢ is in the l-field.

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.sentenceRule₈ {E : Type} (np vp : Cntxt₈ E → Type) : Cntxt₈ E → Type

S → NP VP | B(NP'(@VP')), eq (81).

Equations

• Studies.Anaphora.Cooper2023.Ch8.sentenceRule₈ np vp = Studies.Anaphora.Cooper2023.Ch8.boundary₈ fun (c : Studies.Anaphora.Cooper2023.Ch8.Cntxt₈ E) => np c × vp c

theorem Studies.Anaphora.Cooper2023.Ch8.boundary₈_clears_locality {E : Type} (c : Cntxt₈ E) (i : ℕ) : { q := c.q, 𝔰 := c.𝔰, 𝔩 := Core.PartialAssign.empty, 𝔯 := c.𝔯, 𝔴 := c.𝔴, 𝔤 := c.𝔤, 𝔠 := c.𝔠 }.𝔩 i = none

"Sam thinks she is lucky" — B enables non-local pronoun binding.

inductive Studies.Anaphora.Cooper2023.Ch8.NLPInd : Type

• sam : NLPInd
• she_ref : NLPInd

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instDecidableEqNLPInd : DecidableEq NLPInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instDecidableEqNLPInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Studies.Anaphora.Cooper2023.Ch8.localCtx₈ : Cntxt₈ NLPInd

Equations

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

theorem Studies.Anaphora.Cooper2023.Ch8.local_pronoun_ok : (localCtx₈.𝔩 0).isSome = true

theorem Studies.Anaphora.Cooper2023.Ch8.boundary_clears_for_nonlocal : (have __src := localCtx₈; { q := __src.q, 𝔰 := __src.𝔰, 𝔩 := Core.PartialAssign.empty, 𝔯 := __src.𝔯, 𝔴 := __src.𝔴, 𝔤 := __src.𝔤, 𝔠 := __src.𝔠 }).𝔩 0 = none

def Studies.Anaphora.Cooper2023.Ch8.anaphorFree₈ {E : Type} (P : Cntxt₈ E → Type) : Cntxt₈ E → Type

𝔄(T): anaphor-free filter, eq (85). Requires r-field empty.

Equations

• Studies.Anaphora.Cooper2023.Ch8.anaphorFree₈ P c = (Semantics.TypeTheoretic.propT (∀ (i : ℕ), c.𝔯 i = none) × P c)

def Studies.Anaphora.Cooper2023.Ch8.reflexivize₈ {E : Type} (i : ℕ) (P : Cntxt₈ E → E → Type) : Cntxt₈ E → E → Type

ℜ₈(P): full reflexivization, eq (84). Clears r-field and sets 𝔰(i) = x.

Equations

• Studies.Anaphora.Cooper2023.Ch8.reflexivize₈ i P c x = P { q := c.q, 𝔰 := Core.PartialAssign.update c.𝔰 i x, 𝔩 := c.𝔩, 𝔯 := Core.PartialAssign.empty, 𝔴 := c.𝔴, 𝔤 := c.𝔤, 𝔠 := c.𝔠 } x

def Studies.Anaphora.Cooper2023.Ch8.vpRule₈ {E : Type} (verb : Cntxt₈ E → E → E → Type) (np : Cntxt₈ E → E → Type) : Cntxt₈ E → E → Type

VP → V NP | 𝔄(V'(@NP')), eq (88).

Equations

• Studies.Anaphora.Cooper2023.Ch8.vpRule₈ verb np c x = (Semantics.TypeTheoretic.propT (∀ (i : ℕ), c.𝔯 i = none) × (y : E) × verb c x y × np c y)

theorem Studies.Anaphora.Cooper2023.Ch8.reflexivize₈_agrees_with_simple {E : Type} (R : E → E → Type) (x : E) : reflexivize₈ 0 (fun (x : Cntxt₈ E) (a : E) => R a a) Cntxt₈.initial x = reflexivize R x

ℜ₈ agrees with simplified ℜ when P ignores the context.

@[reducible, inline]

abbrev Studies.Anaphora.Cooper2023.Ch8.ContType₈ (_E : Type) : Type 1

eq (20).

Equations

• Studies.Anaphora.Cooper2023.Ch8.ContType₈ _E = Type

inductive Studies.Anaphora.Cooper2023.Ch8.UnderspecClosure₈ (T : Type) : Type 1

𝔖(T): underspecification closure, eq (89). 7 clauses: base, localize, reflexivize, align, anaphoric, store, retrieve.

• base {T : Type} : T → UnderspecClosure₈ T
• localize {T : Type} : UnderspecClosure₈ T → (Bg : Type) → UnderspecClosure₈ T
• reflexivize {T : Type} : UnderspecClosure₈ T → (idx : ℕ) → UnderspecClosure₈ T
• align {T : Type} : UnderspecClosure₈ T → (src tgt : ℕ) → UnderspecClosure₈ T
• anaphoric {T : Type} : UnderspecClosure₈ T → (i j : ℕ) → UnderspecClosure₈ T
• store_ {T : Type} : UnderspecClosure₈ T → UnderspecClosure₈ T
• retrieve_ {T : Type} : UnderspecClosure₈ T → UnderspecClosure₈ T

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.toUnderspecClosure {E : Type} (s : TwoQuantScope E) (w : s.𝔖) : UnderspecClosure₈ s.𝔖

Equations

• s.toUnderspecClosure w = Studies.Anaphora.Cooper2023.Ch8.UnderspecClosure₈.base w

theorem Studies.Anaphora.Cooper2023.Ch8.twoQuant_embeds_in_closure {E : Type} (s : TwoQuantScope E) (w : s.𝔖) : ∃ (uc : UnderspecClosure₈ s.𝔖), uc = UnderspecClosure₈.base w

N-quantifier scope

N quantifiers yield N! scope readings. Scope orderings are lists of Fin n; list order = retrieval order (head = outermost).

structure Studies.Anaphora.Cooper2023.Ch8.NQuantScope (E : Type) (n : ℕ) : Type 1

N-quantifier scope: n-ary relation + n quantifiers.

• rel : (Fin n → E) → Type
• quants : Fin n → Semantics.TypeTheoretic.Quant E

def Studies.Anaphora.Cooper2023.Ch8.NQuantScope.nestQuants {E : Type} {n : ℕ} (s : NQuantScope E n) : List (Fin n) → (Fin n → E) → Type

Nest quantifiers: head = outermost, tail = innermost.

Equations

• s.nestQuants [] x✝ = s.rel x✝
• s.nestQuants (i :: rest) x✝ = s.quants i fun (x : E) => s.nestQuants rest fun (j : Fin n) => if j = i then x else x✝ j

structure Studies.Anaphora.Cooper2023.Ch8.ScopeOrdering (n : ℕ) : Type

A scope ordering: a permutation of Fin n as a list.

• order : List (Fin n)
• complete : self.order.length = n

def Studies.Anaphora.Cooper2023.Ch8.NQuantScope.readingAt {E : Type} {n : ℕ} (s : NQuantScope E n) (σ : ScopeOrdering n) (default : E) : Type

Equations

• s.readingAt σ default = s.nestQuants σ.order fun (x : Fin n) => default

def Studies.Anaphora.Cooper2023.Ch8.NQuantScope.𝔖 {E : Type} {n : ℕ} (s : NQuantScope E n) (default : E) : Type

Equations

• s.𝔖 default = ((σ : Studies.Anaphora.Cooper2023.Ch8.ScopeOrdering n) × s.readingAt σ default)

def Studies.Anaphora.Cooper2023.Ch8.surfaceOrder₂ : ScopeOrdering 2

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.inverseOrder₂ : ScopeOrdering 2

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.TwoQuantScope.toNQuant {E : Type} (s : TwoQuantScope E) : NQuantScope E 2

Equations

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

"Someone gave every child a present" — 3 quantifiers, 6 readings.

inductive Studies.Anaphora.Cooper2023.Ch8.ThreeQInd : Type

• alice : ThreeQInd
• bob : ThreeQInd
• child1 : ThreeQInd
• child2 : ThreeQInd
• present1 : ThreeQInd
• present2 : ThreeQInd

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instDecidableEqThreeQInd : DecidableEq ThreeQInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instDecidableEqThreeQInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Studies.Anaphora.Cooper2023.Ch8.isSomeone₃ : Semantics.TypeTheoretic.Ppty ThreeQInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.isSomeone₃ Studies.Anaphora.Cooper2023.Ch8.ThreeQInd.alice = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isSomeone₃ Studies.Anaphora.Cooper2023.Ch8.ThreeQInd.bob = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isSomeone₃ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.isChild₃ : Semantics.TypeTheoretic.Ppty ThreeQInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.isChild₃ Studies.Anaphora.Cooper2023.Ch8.ThreeQInd.child1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isChild₃ Studies.Anaphora.Cooper2023.Ch8.ThreeQInd.child2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isChild₃ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.isPresent₃ : Semantics.TypeTheoretic.Ppty ThreeQInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.isPresent₃ Studies.Anaphora.Cooper2023.Ch8.ThreeQInd.present1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isPresent₃ Studies.Anaphora.Cooper2023.Ch8.ThreeQInd.present2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isPresent₃ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.gave₃ : ThreeQInd → ThreeQInd → ThreeQInd → Type

Equations

• One or more equations did not get rendered due to their size.
• Studies.Anaphora.Cooper2023.Ch8.gave₃ x✝² x✝¹ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.someoneQ₃ : Semantics.TypeTheoretic.Quant ThreeQInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.someoneQ₃ = Semantics.TypeTheoretic.semIndefArt Studies.Anaphora.Cooper2023.Ch8.isSomeone₃

def Studies.Anaphora.Cooper2023.Ch8.everyChildQ₃ : Semantics.TypeTheoretic.Quant ThreeQInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.everyChildQ₃ = Semantics.TypeTheoretic.semUniversal Studies.Anaphora.Cooper2023.Ch8.isChild₃

def Studies.Anaphora.Cooper2023.Ch8.aPresentQ₃ : Semantics.TypeTheoretic.Quant ThreeQInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.aPresentQ₃ = Semantics.TypeTheoretic.semIndefArt Studies.Anaphora.Cooper2023.Ch8.isPresent₃

def Studies.Anaphora.Cooper2023.Ch8.someoneGaveEveryChildAPresent : NQuantScope ThreeQInd 3

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.scopeOrdering₃_012 : ScopeOrdering 3

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.scopeOrdering₃_021 : ScopeOrdering 3

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.scopeOrdering₃_102 : ScopeOrdering 3

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.scopeOrdering₃_120 : ScopeOrdering 3

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.scopeOrdering₃_201 : ScopeOrdering 3

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.scopeOrdering₃_210 : ScopeOrdering 3

Equations

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

theorem Studies.Anaphora.Cooper2023.Ch8.three_quant_has_six_orderings : [scopeOrdering₃_012, scopeOrdering₃_021, scopeOrdering₃_102, scopeOrdering₃_120, scopeOrdering₃_201, scopeOrdering₃_210].length = 6

Cross-sentential anaphora

"A man walked. He whistled." — eqs (37)-(44). The pronoun resolves to the indefinite via discourse merge: previous sentence's foreground becomes current sentence's background under label 𝔭.

structure Studies.Anaphora.Cooper2023.Ch8.DiscourseContext (E PrevContent : Type) : Type 1

Discourse merge, eqs (40)-(41).

• 𝔭 : PrevContent
• current : Cntxt₈ E

def Studies.Anaphora.Cooper2023.Ch8.crossSententialResolve {E : Type} {P : E → Type} (prev : (x : E) × P x) : E

Cross-sentential resolution, eqs (42)-(44): 𝔰.x₀ = ⇑𝔭.e.x

Equations

• Studies.Anaphora.Cooper2023.Ch8.crossSententialResolve prev = prev.fst

inductive Studies.Anaphora.Cooper2023.Ch8.CSInd : Type

• john : CSInd
• mary : CSInd

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instDecidableEqCSInd : DecidableEq CSInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instDecidableEqCSInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Studies.Anaphora.Cooper2023.Ch8.isMan : Semantics.TypeTheoretic.Ppty CSInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.isMan Studies.Anaphora.Cooper2023.Ch8.CSInd.john = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isMan Studies.Anaphora.Cooper2023.Ch8.CSInd.mary = Empty

def Studies.Anaphora.Cooper2023.Ch8.walked₈ : Semantics.TypeTheoretic.Ppty CSInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.walked₈ Studies.Anaphora.Cooper2023.Ch8.CSInd.john = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.walked₈ Studies.Anaphora.Cooper2023.Ch8.CSInd.mary = Empty

def Studies.Anaphora.Cooper2023.Ch8.whistled₈ : Semantics.TypeTheoretic.Ppty CSInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.whistled₈ Studies.Anaphora.Cooper2023.Ch8.CSInd.john = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.whistled₈ Studies.Anaphora.Cooper2023.Ch8.CSInd.mary = Empty

def Studies.Anaphora.Cooper2023.Ch8.aManWalked : (x : CSInd) × isMan x × walked₈ x

Equations

• Studies.Anaphora.Cooper2023.Ch8.aManWalked = ⟨Studies.Anaphora.Cooper2023.Ch8.CSInd.john, (PUnit.unit, PUnit.unit)⟩

def Studies.Anaphora.Cooper2023.Ch8.heWhistled (referent : CSInd) : Type

Equations

• Studies.Anaphora.Cooper2023.Ch8.heWhistled referent = Studies.Anaphora.Cooper2023.Ch8.whistled₈ referent

def Studies.Anaphora.Cooper2023.Ch8.resolved_he : CSInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.resolved_he = Studies.Anaphora.Cooper2023.Ch8.crossSententialResolve Studies.Anaphora.Cooper2023.Ch8.aManWalked

theorem Studies.Anaphora.Cooper2023.Ch8.resolved_he_is_john : resolved_he = CSInd.john

def Studies.Anaphora.Cooper2023.Ch8.manWalkedHeWhistled : Type

Equations

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

def Studies.Anaphora.Cooper2023.Ch8.manWalkedHeWhistled_witness : manWalkedHeWhistled

Equations

• Studies.Anaphora.Cooper2023.Ch8.manWalkedHeWhistled_witness = ⟨Studies.Anaphora.Cooper2023.Ch8.CSInd.john, (PUnit.unit, PUnit.unit, PUnit.unit)⟩

theorem Studies.Anaphora.Cooper2023.Ch8.crossSentential_correct : ∃ (w : manWalkedHeWhistled), w.fst = crossSententialResolve aManWalked

"No dog which chases a cat catches it"

Eqs (46)-(55): negation + localization + path alignment.

def Studies.Anaphora.Cooper2023.Ch8.alignPaths {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (align : P.Bg → P.Bg) : Semantics.TypeTheoretic.PPpty E

Path alignment, eq (52): φ_{π₁=π₂} replaces path π₁ with π₂.

Equations

• Studies.Anaphora.Cooper2023.Ch8.alignPaths P align = { Bg := P.Bg, fg := fun (c : P.Bg) => P.fg (align c) }

inductive Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd : Type

• dog1 : DonkeyNegInd
• dog2 : DonkeyNegInd
• cat1 : DonkeyNegInd
• cat2 : DonkeyNegInd

@[implicit_reducible]

instance Studies.Anaphora.Cooper2023.Ch8.instDecidableEqDonkeyNegInd : DecidableEq DonkeyNegInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.instDecidableEqDonkeyNegInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Studies.Anaphora.Cooper2023.Ch8.isDog₈ₙ : Semantics.TypeTheoretic.Ppty DonkeyNegInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.isDog₈ₙ Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd.dog1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isDog₈ₙ Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd.dog2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isDog₈ₙ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.isCat₈ : Semantics.TypeTheoretic.Ppty DonkeyNegInd

Equations

• Studies.Anaphora.Cooper2023.Ch8.isCat₈ Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd.cat1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isCat₈ Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd.cat2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.isCat₈ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.chases₈ : DonkeyNegInd → DonkeyNegInd → Type

Equations

• Studies.Anaphora.Cooper2023.Ch8.chases₈ Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd.dog1 Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd.cat1 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.chases₈ Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd.dog2 Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd.cat2 = PUnit.{1}
• Studies.Anaphora.Cooper2023.Ch8.chases₈ x✝¹ x✝ = Empty

@[reducible, inline]

abbrev Studies.Anaphora.Cooper2023.Ch8.CatBg : Type

Equations

• Studies.Anaphora.Cooper2023.Ch8.CatBg = ((c : Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd) × Studies.Anaphora.Cooper2023.Ch8.isCat₈ c)

def Studies.Anaphora.Cooper2023.Ch8.dogChasesACat : Semantics.TypeTheoretic.Ppty DonkeyNegInd

Localized restrictor: cat existential absorbed into "dog which chases a cat".

Equations

• Studies.Anaphora.Cooper2023.Ch8.dogChasesACat x = (Studies.Anaphora.Cooper2023.Ch8.isDog₈ₙ x × (c : Studies.Anaphora.Cooper2023.Ch8.CatBg) × Studies.Anaphora.Cooper2023.Ch8.chases₈ x c.fst)

def Studies.Anaphora.Cooper2023.Ch8.catches₈_none : DonkeyNegInd → DonkeyNegInd → Type

Equations

• Studies.Anaphora.Cooper2023.Ch8.catches₈_none x✝¹ x✝ = Empty

def Studies.Anaphora.Cooper2023.Ch8.catches₈_all : DonkeyNegInd → DonkeyNegInd → Type

Equations

• Studies.Anaphora.Cooper2023.Ch8.catches₈_all = Studies.Anaphora.Cooper2023.Ch8.chases₈

def Studies.Anaphora.Cooper2023.Ch8.semNo₈ (restr scope : Semantics.TypeTheoretic.Ppty DonkeyNegInd) : Type

"no" quantifier: ∀x. restr(x) → ¬scope(x).

Equations

• Studies.Anaphora.Cooper2023.Ch8.semNo₈ restr scope = ((x : Studies.Anaphora.Cooper2023.Ch8.DonkeyNegInd) → restr x → scope x → Empty)

def Studies.Anaphora.Cooper2023.Ch8.noDogCatchesCat_true : semNo₈ dogChasesACat fun (x : DonkeyNegInd) => (c : CatBg) × catches₈_none x c.fst

theorem Studies.Anaphora.Cooper2023.Ch8.noDogCatchesCat_true_scenario : Nonempty (semNo₈ dogChasesACat fun (x : DonkeyNegInd) => (c : CatBg) × catches₈_none x c.fst)

TRUE when no dog catches the cat it chases.

theorem Studies.Anaphora.Cooper2023.Ch8.noDogCatchesCat_false_scenario : IsEmpty (semNo₈ dogChasesACat fun (x : DonkeyNegInd) => (c : CatBg) × catches₈_all x c.fst)

FALSE when every dog catches the cat it chases.

theorem Studies.Anaphora.Cooper2023.Ch8.donkeyNeg_uses_localization : dogChasesACat = fun (x : DonkeyNegInd) => isDog₈ₙ x × localize { Bg := CatBg, fg := fun (c : CatBg) (a : DonkeyNegInd) => chases₈ a c.fst } x

Negation donkey uses 𝔏 (same mechanism as classic donkey).