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

[Coo23] [Cho81] [Kan94] [SP21] [Kam81] [Chi95]

Cooper's From Perception to Communication Chapter 8 introduces content types that replace specific contents with types whose witnesses are fully specified readings. This file formalises §8.2 (quantifier scope and underspecification) and §8.3 (anaphora — donkey, binding, cross-sentential, negation), and provides bridge theorems linking Cooper's TTR machinery to linglib's ScopeConfig and BindingConfig interfaces.

The companion Studies/Cooper2023/Basic.lean wires this Ch. 8 substrate to the donkey rows in Data/Examples/ and the Chomsky1981 binding paradigm.

Main definitions

• QStore, QStore.store, QStore.retrieve — quantifier-storage stack (Cooper §8.2, adapting Cooper 1983-style storage to TTR).
• TwoQuantScope, TwoQuantScope.𝔖 — underspecified content type for a two-quantifier sentence; witnesses correspond to the two scope readings.
• Cntxt₈ — full Ch. 8 context (Cooper §8.2-8.3, evolved across the chapter as locality 𝔩 and reflexive marking 𝔯 are added).
• localize, reflexivize, anaphoricResolve — TTR operations for donkey anaphora and binding (§8.3).
• UnderspecClosure₈ — inductive closure of a content type under the seven Ch. 8 operators (base, localize, reflexivize, align, anaphoric, store, retrieve).
• NQuantScope — formaliser's extension to n quantifiers (Cooper §8.2 treats only n ≤ 2; the N! over-generation is well known to violate empirical scope-island constraints).

Main statements

• tagged_roundtrip — bijection between TwoQuantScope.𝔖 witnesses and Semantics.Scope.ScopeConfig tags. Engineering interface for downstream RSA-style scope listeners ([SP21]); Cooper himself does not draw this connection.
• reflexivize₈_agrees_with_simple — record-typed reflexivize₈ collapses to the simplified reflexivize when the context is initial.
• donkeyNeg_uses_localization — the negation donkey sentence reuses localize.
• reflexivize_to_binding, pronominalBindingConfig — translate TTR's assignment-based binding to positional BindingConfig. Cooper §8.3 (book p.371) deliberately avoids positional encodings in favour of assignment-percolation; the bridge is a linglib engineering convenience, not Cooper's theory.

Notation

• ℒ (Script L, U+2112) — Cooper's localization operator (§8.3 eq 49).
• ℒʸ — universal-localization variant for strong-donkey readings.
• ℜ — reflexivization (§8.3 eq 84).
• Purification operators 𝔓 (Fraktur P) / 𝔓ʸ are inherited from Cooper2023Ch7.

Implementation notes

• localize vs. Ch. 7 purify. Cooper §8.3 eq (49) defines ℒ(𝒫) as a record-type merge: the outer parameter T1 is folded into the inner property's record-domain under label 𝔠, producing another parametric property. linglib's PPpty schema has no inner record-domain (the foreground argument is a bare E), so the record-merge collapses to Σ-existential elimination of the background — definitionally identical to Ch. 7's purify. The abbrev localize := purify records this encoding-collapse, not a text-level identity of ℒ with 𝔓 in Cooper's prose.
• Strong-donkey reading. Cooper §8.3 eq (60) derives the strong reading by applying 𝔓^∀ (Ch. 7 eq 13) to a scope already prepared by ℒ and path-alignment (alignPaths here). The end-to-end three-stage pipeline ℒ → alignPaths → 𝔓^∀ is not formalised here — only the individual stages are present.
• TTR witness types are Type-valued, not Prop. Cooper's witness records are first-class data (fields can be inspected and used compositionally). Nonempty/IsEmpty mediate inhabitance claims where the witness data is not needed downstream.

TODO

• End-to-end formalisation of the ℒ → alignPaths → 𝔓^∀ strong-donkey pipeline (the DonkeyAnaphora section currently exercises only the weak reading).
• Bridge from UnderspecClosure₈ syntax to a semantic evaluator (twoQuant_embeds_in_closure only asserts the base constructor; no compositional interpretation is provided).

Quantifier stores

A quantifier store holds quantifiers that have been "tucked away" during composition and await scope assignment via retrieval. Cooper §8.2 adapts Cooper 1983-style storage to TTR.

structure Cooper2023Ch8.QStore (E : Type) : Type 1

A quantifier store: a list of quantifiers awaiting scope resolution (Cooper §8.2). Stored quantifiers are later retrieved at scope positions; retrieval order determines scope.

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

  The stored quantifiers, ordered by storage time

def Cooper2023Ch8.QStore.empty {E : Type} : QStore E

Empty quantifier store: no pending scope ambiguity.

Equations

• Cooper2023Ch8.QStore.empty = { stored := [] }

def Cooper2023Ch8.QStore.isPlugged {E : Type} (qs : QStore E) : Prop

A store is plugged when all quantifiers have taken scope (terminology from Bos's plugged/unplugged distinction, adopted by Cooper §8.2).

Equations

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

def Cooper2023Ch8.QStore.isUnplugged {E : Type} (qs : QStore E) : Prop

A store is unplugged when quantifiers remain to be scoped.

Equations

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

@[simp]

theorem Cooper2023Ch8.plugged_iff_not_unplugged {E : Type} (qs : QStore E) : qs.isPlugged ↔ ¬qs.isUnplugged

Plugged ↔ ¬ unplugged.

@[simp]

theorem Cooper2023Ch8.empty_isPlugged {E : Type} : QStore.empty.isPlugged

The empty store is plugged by construction.

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

A plugged QStore corresponds to a trivial Parametric background: an empty store contributes no scope presuppositions, exactly as Parametric.trivial has Bg = Unit.

Equations

• Cooper2023Ch8.pluggedToTrivial c qs _h = Semantics.TypeTheoretic.Parametric.trivial c

Store and retrieve operations

store moves a quantifier from the content into the qstore, leaving a trace variable in the content. retrieve pops the outermost stored quantifier and applies it at a scope position; retrieval order determines relative scope (Cooper §8.2).

def Cooper2023Ch8.QStore.store {E : Type} (qs : QStore E) (q : Semantics.TypeTheoretic.Quant E) : QStore E

Push a quantifier onto the store (Cooper §8.2).

Equations

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

theorem Cooper2023Ch8.store_unplugs {E : Type} (q : Semantics.TypeTheoretic.Quant E) : (QStore.empty.store q).isUnplugged

Storing into a plugged store makes it unplugged.

def Cooper2023Ch8.QStore.retrieve {E : Type} (qs : QStore E) : Option (Semantics.TypeTheoretic.Quant E × QStore E)

Pop the outermost stored quantifier (Cooper §8.2). 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 Cooper2023Ch8.retrieve_none_iff_plugged {E : Type} (qs : QStore E) : qs.retrieve = none ↔ qs.isPlugged

Retrieve returns none iff the store is plugged.

@[simp]

theorem Cooper2023Ch8.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 and the underspecification closure

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

structure Cooper2023Ch8.TwoQuantScope (E : Type) : Type 1

A two-quantifier scope configuration: two quantifiers and a relation. The minimal underspecified content for a doubly-quantified sentence (Cooper §8.2).

• 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 Cooper2023Ch8.TwoQuantScope.surfaceScope {E : Type} (s : TwoQuantScope E) : Type

Surface scope reading: Q₁ scopes over Q₂. Retrieving Q₁ first gives 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 Cooper2023Ch8.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 Cooper2023Ch8.TwoQuantScope.𝔖 {E : Type} (s : TwoQuantScope E) : Type

The underspecification closure 𝔖 for two quantifiers: the join of all possible scope readings. Each witness of 𝔖(content) is one fully specified reading; with two quantifiers, 𝔖 has at most two witnesses.

Equations

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

theorem Cooper2023Ch8.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 Cooper2023Ch8.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 Cooper2023Ch8.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 Cooper2023Ch8.TwoQuantScope.readingAt {E : Type} (s : TwoQuantScope E) (sc : Semantics.Scope.ScopeConfig) : Type

Select a scope reading by ScopeConfig. Ch8 → [SP21] 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 to ScopeConfig

The witnesses of 𝔖(content) are in bijection with the Semantics.Scope.ScopeConfig tags used by [SP21]'s RSA scope listener: each ScopeConfig selects one reading, and every witness of 𝔖 comes from exactly one reading. The bridge is a linglib engineering interface; Cooper himself does not draw this connection.

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

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 Cooper2023Ch8.TwoQuantScope.tagged_to_𝔖 {E : Type} (s : TwoQuantScope E) (tagged : (sc : Semantics.Scope.ScopeConfig) × s.readingAt sc) : s.𝔖

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 Cooper2023Ch8.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. The bijection between 𝔖 witnesses and ScopeConfig-tagged readings.

Phenomenon: scope ambiguity in "every boy hugged a dog"

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 Cooper2023Ch8.ScopeInd : Type

Individuals for the scope example.

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

@[implicit_reducible]

instance Cooper2023Ch8.instDecidableEqScopeInd : DecidableEq ScopeInd

Equations

• Cooper2023Ch8.instDecidableEqScopeInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch8.instReprScopeInd.repr : ScopeInd → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cooper2023Ch8.instReprScopeInd : Repr ScopeInd

Equations

• Cooper2023Ch8.instReprScopeInd = { reprPrec := Cooper2023Ch8.instReprScopeInd.repr }

def Cooper2023Ch8.isBoy : Semantics.TypeTheoretic.Ppty ScopeInd

Boy predicate: Tom and Bill are boys.

Equations

• Cooper2023Ch8.isBoy Cooper2023Ch8.ScopeInd.tom = PUnit.{1}
• Cooper2023Ch8.isBoy Cooper2023Ch8.ScopeInd.bill = PUnit.{1}
• Cooper2023Ch8.isBoy x✝ = Empty

def Cooper2023Ch8.isDog₈ : Semantics.TypeTheoretic.Ppty ScopeInd

Dog predicate: Fido and Rex are dogs.

Equations

• Cooper2023Ch8.isDog₈ Cooper2023Ch8.ScopeInd.fido = PUnit.{1}
• Cooper2023Ch8.isDog₈ Cooper2023Ch8.ScopeInd.rex = PUnit.{1}
• Cooper2023Ch8.isDog₈ x✝ = Empty

def Cooper2023Ch8.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

• Cooper2023Ch8.hugs Cooper2023Ch8.ScopeInd.tom Cooper2023Ch8.ScopeInd.fido = PUnit.{1}
• Cooper2023Ch8.hugs Cooper2023Ch8.ScopeInd.bill Cooper2023Ch8.ScopeInd.rex = PUnit.{1}
• Cooper2023Ch8.hugs x✝¹ x✝ = Empty

def Cooper2023Ch8.everyBoy : Semantics.TypeTheoretic.Quant ScopeInd

The universal quantifier for boys.

Equations

• Cooper2023Ch8.everyBoy = Semantics.TypeTheoretic.semUniversal Cooper2023Ch8.isBoy

def Cooper2023Ch8.aDog : Semantics.TypeTheoretic.Quant ScopeInd

The existential quantifier for dogs.

Equations

• Cooper2023Ch8.aDog = Semantics.TypeTheoretic.semIndefArt Cooper2023Ch8.isDog₈

def Cooper2023Ch8.everyBoyHuggedADog : TwoQuantScope ScopeInd

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

Equations

• Cooper2023Ch8.everyBoyHuggedADog = { rel := Cooper2023Ch8.hugs, q₁ := Cooper2023Ch8.everyBoy, q₂ := Cooper2023Ch8.aDog }

def Cooper2023Ch8.surfaceScopeWitness : everyBoyHuggedADog.surfaceScope

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

Equations

• Cooper2023Ch8.surfaceScopeWitness Cooper2023Ch8.ScopeInd.tom x_2 = { individual := Cooper2023Ch8.ScopeInd.fido, restrWit := PUnit.unit, scopeWit := PUnit.unit }
• Cooper2023Ch8.surfaceScopeWitness Cooper2023Ch8.ScopeInd.bill x_2 = { individual := Cooper2023Ch8.ScopeInd.rex, restrWit := PUnit.unit, scopeWit := PUnit.unit }

theorem Cooper2023Ch8.no_inverse_scope : Semantics.TypeTheoretic.IsFalse everyBoyHuggedADog.inverseScope

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

def Cooper2023Ch8.underspecInhabited : everyBoyHuggedADog.𝔖

𝔖 is inhabited (via the surface scope reading).

Equations

• Cooper2023Ch8.underspecInhabited = Cooper2023Ch8.everyBoyHuggedADog.surfaceToUnderspec Cooper2023Ch8.surfaceScopeWitness

theorem Cooper2023Ch8.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 Cooper2023Ch8.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 to Ch. 7 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 REFSET).

def Cooper2023Ch8.surfaceScopeInnerWitness {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) : Semantics.TypeTheoretic.ParticularWC_Exist Q fun (y : E) => R x y

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 — predicting REFSET anaphora for the object NP.

Equations

• Cooper2023Ch8.surfaceScopeInnerWitness P Q R w x hP = { x := (w x hP).individual, pWit := (w x hP).restrWit, qWit := (w x hP).scopeWit }

def Cooper2023Ch8.inverseScopeOuterWitness {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) : Semantics.TypeTheoretic.ParticularWC_Exist Q fun (y : E) => Semantics.TypeTheoretic.semUniversal P fun (x : E) => R x y

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 under which the universal scopes.

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

Equations

• Cooper2023Ch8.inverseScopeOuterWitness P Q R w = { x := w.individual, pWit := w.restrWit, qWit := w.scopeWit }

theorem Cooper2023Ch8.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)

Surface scope (semUniversal + ExistWitness) matches existPQ at each individual — the Ch. 7 existential-predicate overlap; scope retrieval order determines which witness conditions hold per quantifier position.

Localization

Cooper §8.3 eq (49): localization ℒ(𝒫) takes a doubly-parametric property ˹λc:T1.˹λr:T2.φ˺˺ and folds the outer context-parameter T1 into the inner property's record-domain under label 𝔠, producing another parametric property whose body has paths c.π rewritten to r.𝔠.π. This is the Ch. 8 mechanism for donkey anaphora ("Every farmer who owns a donkey beats it"): the indefinite "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.

In linglib's flat PPpty encoding (no inner record-domain), this record-merge collapses to Σ-existential elimination of the background, making localize definitionally identical to Ch. 7's purify. See the Implementation notes in the module docstring.

@[reducible, inline]

abbrev Cooper2023Ch8.localize {E : Type} : Semantics.TypeTheoretic.PPpty E → Semantics.TypeTheoretic.Ppty E

Cooper's localization operator ℒ (§8.3 eq 49).

In linglib's flat PPpty encoding localize is the same as Ch. 7's purify; see the module-level Implementation notes for the encoding-collapse argument. The abbrev records this identification so Ch. 7 lemmas discharge Ch. 8 obligations definitionally.

Equations

• Cooper2023Ch8.localize = Cooper2023Ch7.purify

@[reducible, inline]

abbrev Cooper2023Ch8.localizeUniv {E : Type} : Semantics.TypeTheoretic.PPpty E → Semantics.TypeTheoretic.Ppty E

Cooper's universal-localization variant ℒʸ (the strong-donkey companion to ℒ). Coincides with Ch. 7's purifyUniv for the same encoding reason.

Equations

• Cooper2023Ch8.localizeUniv = Cooper2023Ch7.purifyUniv

def Cooper2023Ch8.termℒ_ : Lean.ParserDescr

Cooper's localization operator ℒ (§8.3 eq 49).

In linglib's flat PPpty encoding localize is the same as Ch. 7's purify; see the module-level Implementation notes for the encoding-collapse argument. The abbrev records this identification so Ch. 7 lemmas discharge Ch. 8 obligations definitionally.

Equations

• Cooper2023Ch8.termℒ_ = Lean.ParserDescr.node `Cooper2023Ch8.termℒ_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℒ") (Lean.ParserDescr.cat `term 1024))

def Cooper2023Ch8.«termℒʸ_» : Lean.ParserDescr

Cooper's universal-localization variant ℒʸ (the strong-donkey companion to ℒ). Coincides with Ch. 7's purifyUniv for the same encoding reason.

Equations

• Cooper2023Ch8.«termℒʸ_» = Lean.ParserDescr.node `Cooper2023Ch8.«termℒʸ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℒʸ") (Lean.ParserDescr.cat `term 1024))

Localization lemmas (inherited from Ch7 purification)

Since localize := purify, witness-existence lemmas about purification carry over verbatim. We restate them under the Ch. 8 vocabulary for discoverability.

theorem Cooper2023Ch8.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 Cooper2023Ch8.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.

@[simp]

theorem Cooper2023Ch8.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 Cooper2023Ch8.localization_readings_agree_when_pure {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (hPure : Cooper2023Ch7.PPpty.isPure P) (a : E) : Nonempty (localize P a) ↔ Nonempty (localizeUniv P a)

Weak and strong donkey readings agree when the parametric background is trivial. Corollary of donkey_readings_agree_when_pure.

Phenomenon: "Every farmer who owns a donkey beats it"

The classical Geach/Kamp donkey example (Cooper §8.3 uses "no dog which chases a cat catches it" as his primary case; we use the better-known farmer/donkey variant). 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 (ℒ in linglib's encoding = 𝔓) is witnessable — 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 Cooper2023Ch8.DonkeyInd : Type

Individuals for the donkey example.

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

@[implicit_reducible]

instance Cooper2023Ch8.instDecidableEqDonkeyInd : DecidableEq DonkeyInd

Equations

• Cooper2023Ch8.instDecidableEqDonkeyInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch8.isFarmer : Semantics.TypeTheoretic.Ppty DonkeyInd

Equations

• Cooper2023Ch8.isFarmer Cooper2023Ch8.DonkeyInd.farmer1 = PUnit.{1}
• Cooper2023Ch8.isFarmer Cooper2023Ch8.DonkeyInd.farmer2 = PUnit.{1}
• Cooper2023Ch8.isFarmer x✝ = Empty

def Cooper2023Ch8.isDonkey₈ : Semantics.TypeTheoretic.Ppty DonkeyInd

Equations

• Cooper2023Ch8.isDonkey₈ Cooper2023Ch8.DonkeyInd.donkey1 = PUnit.{1}
• Cooper2023Ch8.isDonkey₈ Cooper2023Ch8.DonkeyInd.donkey2 = PUnit.{1}
• Cooper2023Ch8.isDonkey₈ x✝ = Empty

def Cooper2023Ch8.owns : DonkeyInd → DonkeyInd → Type

Ownership: farmer1 owns donkey1, farmer2 owns donkey2.

Equations

• Cooper2023Ch8.owns Cooper2023Ch8.DonkeyInd.farmer1 Cooper2023Ch8.DonkeyInd.donkey1 = PUnit.{1}
• Cooper2023Ch8.owns Cooper2023Ch8.DonkeyInd.farmer2 Cooper2023Ch8.DonkeyInd.donkey2 = PUnit.{1}
• Cooper2023Ch8.owns x✝¹ x✝ = Empty

def Cooper2023Ch8.beats : DonkeyInd → DonkeyInd → Type

Beating: each farmer beats the donkey they own.

Equations

• Cooper2023Ch8.beats Cooper2023Ch8.DonkeyInd.farmer1 Cooper2023Ch8.DonkeyInd.donkey1 = PUnit.{1}
• Cooper2023Ch8.beats Cooper2023Ch8.DonkeyInd.farmer2 Cooper2023Ch8.DonkeyInd.donkey2 = PUnit.{1}
• Cooper2023Ch8.beats x✝¹ x✝ = Empty

@[reducible, inline]

abbrev Cooper2023Ch8.DonkeyBg : Type

Background type: a donkey that exists.

Equations

• Cooper2023Ch8.DonkeyBg = ((d : Cooper2023Ch8.DonkeyInd) × Cooper2023Ch8.isDonkey₈ d)

def Cooper2023Ch8.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 Cooper2023Ch8.farmer1WeakDonkey : localize farmerOwnsBeatsDonkey DonkeyInd.farmer1

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

Equations

• Cooper2023Ch8.farmer1WeakDonkey = ⟨⟨Cooper2023Ch8.DonkeyInd.donkey1, PUnit.unit⟩, (PUnit.unit, PUnit.unit, PUnit.unit)⟩

def Cooper2023Ch8.farmer2WeakDonkey : localize farmerOwnsBeatsDonkey DonkeyInd.farmer2

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

Equations

• Cooper2023Ch8.farmer2WeakDonkey = ⟨⟨Cooper2023Ch8.DonkeyInd.donkey2, PUnit.unit⟩, (PUnit.unit, PUnit.unit, PUnit.unit)⟩

theorem Cooper2023Ch8.farmer1_fails_strong_donkey : IsEmpty (localizeUniv farmerOwnsBeatsDonkey DonkeyInd.farmer1)

The strong-donkey reading fails for farmer1: the universal "every donkey d, farmer1 owns d ∧ beats d" is falsified by donkey2, which farmer1 does not own.

theorem Cooper2023Ch8.donkey_readings_diverge : Nonempty (localize farmerOwnsBeatsDonkey DonkeyInd.farmer1) ∧ ¬Nonempty (localizeUniv farmerOwnsBeatsDonkey DonkeyInd.farmer1)

Weak and strong donkey readings genuinely diverge in this scenario: weak is witnessable, strong is empty. Witness that donkey_readings_agree_when_pure has a real hypothesis — when Bg is non-trivial (multiple donkeys), the readings differ.

def Cooper2023Ch8.everyFarmerBeatsDonkeyWeak : Semantics.TypeTheoretic.semUniversal (localize farmerOwnsBeatsDonkey) fun (x : DonkeyInd) => PUnit.{1}

The full sentence "every farmer who owns a donkey beats it" is witnessed under the weak donkey reading.

Equations

• Cooper2023Ch8.everyFarmerBeatsDonkeyWeak Cooper2023Ch8.DonkeyInd.farmer1 x_2 = PUnit.unit
• Cooper2023Ch8.everyFarmerBeatsDonkeyWeak Cooper2023Ch8.DonkeyInd.farmer2 x_2 = PUnit.unit

TODO: Cooper's strong-donkey pipeline ℒ → alignPaths → 𝔓^∀

Cooper §8.3 eq (60) derives the strong-donkey reading by composing three distinct operations: localize the verb-phrase parametric content (ℒ, eq 49); align two paths in the result so the pronoun depends on the indefinite (alignPaths, eq 51-52); then apply 𝔓^∀ (Ch. 7 eq 13) to this prepared scope as the witness condition for the universal quantifier. The composite pipeline is not formalised here; we have each stage independently (localize, alignPaths, purifyUniv), but the end-to-end derivation for "every farmer who owns a donkey likes it" is deferred.

Reflexivization and anaphoric resolution

Cooper §8.3 introduces two binding operations: ℜ (reflexivization, eq 84) removes the reflexive marking from the context and binds the reflexive pronoun to the subject variable; @_{i,j} (anaphoric combination, eq 28) identifies assignment path j with path i, linking a pronoun to its antecedent.

The interplay yields complementary distribution: ℜ forces local binding for reflexives; @_{i,j} with a constant resolution gives disjoint reference for pronouns; the boundary operation B (eq 77, see below) clears locality at clause boundaries.

The record-typed versions (reflexivize₈, anaphoricCombine₈, etc., using Cntxt₈) are defined further down; the simplified versions here serve as the clean semantic interface for bridge theorems, with reflexivize₈_agrees_with_simple connecting the two layers.

def Cooper2023Ch8.reflexivize {E : Type} (R : E → E → Type) : Semantics.TypeTheoretic.Ppty E

Reflexivization (Cooper §8.3 eq 84): identify the two arguments of a binary relation. 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

• Cooper2023Ch8.reflexivize R x = R x x

def Cooper2023Ch8.termℜ_ : Lean.ParserDescr

Reflexivization (Cooper §8.3 eq 84): identify the two arguments of a binary relation. 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

• Cooper2023Ch8.termℜ_ = Lean.ParserDescr.node `Cooper2023Ch8.termℜ_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℜ") (Lean.ParserDescr.cat `term 1024))

def Cooper2023Ch8.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} (§8.3): identifying path 𝔤.xⱼ with 𝔤.xᵢ creates the anaphoric link.

• Reflexives: resolve = id (subject is the referent) — equivalent to ℜ.
• Pronouns: resolve = const (g i) (assignment provides referent).

Equations

• Cooper2023Ch8.anaphoricResolve P resolve x = P.fg (resolve x) x

@[simp]

theorem Cooper2023Ch8.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.

theorem Cooper2023Ch8.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).

theorem Cooper2023Ch8.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 a constant referent y: resolves to y regardless of the subject x. Captures @_{i,j} when the assignment g i = y is fixed from discourse context. "Sam likes him(=Bill)" yields like(Sam, Bill).

Phenomenon: "Sam likes himself" / "Sam likes him"

Cooper §8.3: "Sam likes him" has two fields x and y for individuals; when y = x, the fields are filled by the same individual. Reflexivization ℜ forces this identification, yielding complementary distribution:

• "Sam likes himself" = ℜ like (Sam) = like(Sam, Sam) (coreference).
• "Sam likes him(=Bill)" = anaphoricResolve likeParam (const Bill) (Sam) = like(Sam, Bill) (disjoint reference).

inductive Cooper2023Ch8.BindInd : Type

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

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

@[implicit_reducible]

instance Cooper2023Ch8.instDecidableEqBindInd : DecidableEq BindInd

Equations

• Cooper2023Ch8.instDecidableEqBindInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch8.like₈ : BindInd → BindInd → Type

"like" as a non-trivial binary relation: Sam likes everyone, Bill likes Kim and himself, Kim likes herself only. The non-triviality is load-bearing — ℜ (like₈) Kim is inhabited but like₈ Kim Sam is not, so reflexivization genuinely restricts which argument pairs are witnessable.

Equations

• Cooper2023Ch8.like₈ Cooper2023Ch8.BindInd.sam x✝ = PUnit.{1}
• Cooper2023Ch8.like₈ Cooper2023Ch8.BindInd.bill Cooper2023Ch8.BindInd.bill = PUnit.{1}
• Cooper2023Ch8.like₈ Cooper2023Ch8.BindInd.bill Cooper2023Ch8.BindInd.kim = PUnit.{1}
• Cooper2023Ch8.like₈ Cooper2023Ch8.BindInd.kim Cooper2023Ch8.BindInd.kim = PUnit.{1}
• Cooper2023Ch8.like₈ x✝¹ x✝ = Empty

theorem Cooper2023Ch8.like₈_nontrivial : IsEmpty (like₈ BindInd.kim BindInd.sam)

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

def Cooper2023Ch8.likeParam : Semantics.TypeTheoretic.PPpty BindInd

"like" as parametric content: the object comes from background. The verb phrase "likes him" has the object's referent in the context.

Equations

• Cooper2023Ch8.likeParam = { Bg := Cooper2023Ch8.BindInd, fg := fun (obj subj : Cooper2023Ch8.BindInd) => Cooper2023Ch8.like₈ subj obj }

def Cooper2023Ch8.samLikesHimself : reflexivize like₈ BindInd.sam

"Sam likes himself" via ℜ: ℜ like₈ Sam = like₈ Sam Sam.

Equations

• Cooper2023Ch8.samLikesHimself = PUnit.unit

def Cooper2023Ch8.samLikesBill : anaphoricResolve likeParam (fun (x : BindInd) => BindInd.bill) BindInd.sam

"Sam likes him(=Bill)" via pronoun resolution.

Equations

• Cooper2023Ch8.samLikesBill = PUnit.unit

theorem Cooper2023Ch8.reflexive_is_self : reflexivize like₈ BindInd.sam = like₈ BindInd.sam BindInd.sam

ℜ forces coreference: the reflexive witness equals like₈ Sam Sam.

theorem Cooper2023Ch8.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 Cooper2023Ch8.allLikeSelf (x : BindInd) : reflexivize like₈ x

Every individual can like themselves; ℜ is always witnessable here.

Equations

• Cooper2023Ch8.allLikeSelf Cooper2023Ch8.BindInd.sam = PUnit.unit
• Cooper2023Ch8.allLikeSelf Cooper2023Ch8.BindInd.bill = PUnit.unit
• Cooper2023Ch8.allLikeSelf Cooper2023Ch8.BindInd.kim = PUnit.unit

theorem Cooper2023Ch8.param_reflexivize_agrees : anaphoricResolve likeParam id = reflexivize like₈

ℜ applied via anaphoricResolve with identity matches direct reflexivization.

theorem Cooper2023Ch8.reflexive_constrains_kim : Nonempty (reflexivize like₈ BindInd.kim) ∧ IsEmpty (like₈ BindInd.kim BindInd.bill)

ℜ genuinely constrains: Kim can like herself but not Bill — the restriction is non-trivial because like₈ Kim Bill is empty while like₈ Kim Kim is PUnit.

Bridge to BindingConfig

Translate TTR's assignment-based binding (ℜ / @_{i,j}) to the position-based BindingConfig interface in Syntax.Binding.Semantics. Cooper §8.3 (book p.371) deliberately avoids positional encodings in favour of assignment-percolation; the bridge is a linglib engineering convenience for consumers that want position-typed binding output, not a claim about Cooper's theory. The mapping is:

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

def Cooper2023Ch8.reflexivizeToBinding (subjectPos objectPos : BindingSemantics.Position) : BindingSemantics.BindingRelation

ℜ induces a binding relation: subject binds the reflexive object. The subject at position 0 binds "himself" at position 2.

Equations

• Cooper2023Ch8.reflexivizeToBinding subjectPos objectPos = { binder := subjectPos, bindee := objectPos, varIndex := 0 }

def Cooper2023Ch8.reflexiveBindingConfig : BindingSemantics.BindingConfig

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

Equations

• Cooper2023Ch8.reflexiveBindingConfig = { bindings := [Cooper2023Ch8.reflexivizeToBinding { index := 0 } { index := 2 }], freeVariables := [] }

theorem Cooper2023Ch8.reflexive_config_wellFormed : reflexiveBindingConfig.wellFormed = true

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

def Cooper2023Ch8.pronominalBindingConfig : BindingSemantics.BindingConfig

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

Equations

• Cooper2023Ch8.pronominalBindingConfig = { bindings := [], freeVariables := [({ index := 2 }, 0)] }

theorem Cooper2023Ch8.pronominal_no_local_binding : pronominalBindingConfig.bindings = []

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

theorem Cooper2023Ch8.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 Ch. 8 context Cntxt₈

Cooper's context evolves across the chapter: the initial 5-field context {q, 𝔰, 𝔴, 𝔤, 𝔠} (§8.2) is extended with 𝔩 (locality) in §8.3 and with 𝔯 (reflexive marking) later in §8.3. Cntxt₈ encodes the final 7-field shape; pre-locality and pre-reflexive variants are recovered by leaving 𝔩 / 𝔯 empty. Extends CntxtFull (Ch. 7) with q, 𝔩, 𝔯.

structure Cooper2023Ch8.Cntxt₈ (E : Type) : Type 1

Cooper's full Ch. 8 context. Fields: quantifier store q, current assignment 𝔰, locality 𝔩, reflexive-marking 𝔯, wh-assignment 𝔴, gap-tracking assignment 𝔤, propositional context 𝔠.

• 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 Cooper2023Ch8.Cntxt₈.initial {E : Type} : Cntxt₈ E

The empty initial context.

Equations

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

def Cooper2023Ch8.Cntxt₈.isPreLocality {E : Type} (c : Cntxt₈ E) : Prop

Pre-locality context shape (Cooper §8.2 initial form): both 𝔩 and 𝔯 are empty.

Equations

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

def Cooper2023Ch8.Cntxt₈.isPreReflexive {E : Type} (c : Cntxt₈ E) : Prop

Pre-reflexive context shape (Cooper §8.3 mid-form): 𝔯 is empty.

Equations

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

theorem Cooper2023Ch8.Cntxt₈.initial_isPreLocality {E : Type} : initial.isPreLocality

Boundary operation B and locality-aware @_{i,j} (Cooper §8.3)

B(α) clears the locality field at clause boundaries; @_{i,j} with a locality check identifies 𝔰.xⱼ with 𝔰.xᵢ only when 𝔰.xᵢ is in the 𝔩-field. Together they enforce a locality constraint on pronoun-antecedent linking.

def Cooper2023Ch8.boundary₈ {E : Type} (P : Cntxt₈ E → Type) : Cntxt₈ E → Type

Boundary operation B(α): resets 𝔩 at clause boundaries.

Equations

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

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

Locality-checked @_{i,j}: identifies 𝔰.xⱼ with 𝔰.xᵢ only when 𝔰.xᵢ is in 𝔩.

Equations

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

def Cooper2023Ch8.sentenceRule₈ {E : Type} (np vp : Cntxt₈ E → Type) : Cntxt₈ E → Type

Sentence rule S → NP VP | B(NP' (@VP')).

Equations

• Cooper2023Ch8.sentenceRule₈ np vp = Cooper2023Ch8.boundary₈ fun (c : Cooper2023Ch8.Cntxt₈ E) => np c × vp c

@[simp]

theorem Cooper2023Ch8.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 Cooper2023Ch8.NLPInd : Type

• sam : NLPInd
• she_ref : NLPInd

@[implicit_reducible]

instance Cooper2023Ch8.instDecidableEqNLPInd : DecidableEq NLPInd

Equations

• Cooper2023Ch8.instDecidableEqNLPInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch8.localCtx₈ : Cntxt₈ NLPInd

Equations

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

theorem Cooper2023Ch8.local_pronoun_ok : (localCtx₈.𝔩 0).isSome = true

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

Anaphor-free filter 𝔄 and full record-typed reflexivization (Cooper §8.3)

def Cooper2023Ch8.anaphorFree₈ {E : Type} (P : Cntxt₈ E → Type) : Cntxt₈ E → Type

Anaphor-free filter 𝔄(T): requires the 𝔯-field to be empty. "Principle A" in Cooper's evocation of [Cho81]'s binding theory.

Equations

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

def Cooper2023Ch8.reflexivize₈ {E : Type} (i : ℕ) (P : Cntxt₈ E → E → Type) : Cntxt₈ E → E → Type

Full record-typed reflexivization ℜ₈(P): clears the 𝔯-field and sets 𝔰(i) = x.

Equations

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

def Cooper2023Ch8.vpRule₈ {E : Type} (verb : Cntxt₈ E → E → E → Type) (np : Cntxt₈ E → E → Type) : Cntxt₈ E → E → Type

VP rule VP → V NP | 𝔄(V' (@NP')).

Equations

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

theorem Cooper2023Ch8.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 the simplified ℜ when P ignores the context.

Generalised underspecification closure

inductive Cooper2023Ch8.UnderspecClosure₈ (T : Type) : Type 1

Inductive closure of a content type T under the seven Ch. 8 operators (base, localize, reflexivize, align, anaphoric, store, retrieve). Compositional interpretation as a semantic evaluator is not yet provided — this is a syntax-tree representation only.

• 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 Cooper2023Ch8.TwoQuantScope.toUnderspecClosure {E : Type} (s : TwoQuantScope E) (w : s.𝔖) : UnderspecClosure₈ s.𝔖

Equations

• s.toUnderspecClosure w = Cooper2023Ch8.UnderspecClosure₈.base w

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

N-quantifier scope (formaliser's extension)

Cooper §8.2 treats only the n ≤ 2 case. We extend the storage-and-retrieve mechanism to n quantifiers, indexing scope orderings by lists of Fin n (head = outermost retrieved). The naïve combinatorial maximum is n! distinct orderings; empirical scope is constrained by scope islands, freezing, and weak-island effects that this substrate does not enforce.

structure Cooper2023Ch8.NQuantScope (E : Type) (n : ℕ) : Type 1

An n-quantifier scope configuration: an n-ary relation plus n quantifiers.

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

def Cooper2023Ch8.NQuantScope.nestQuants {E : Type} {n : ℕ} (s : NQuantScope E n) : List (Fin n) → (Fin n → E) → Type

Nest the quantifiers along a given retrieval order; the head of the list takes outermost scope.

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 Cooper2023Ch8.ScopeOrdering (n : ℕ) : Type

A scope ordering: a (not necessarily distinct) list of Fin n indices of length n. A proper permutation requires additionally order.Nodup; we leave this unconstrained because the witness theorems below construct orderings explicitly.

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

def Cooper2023Ch8.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 Cooper2023Ch8.NQuantScope.𝔖 {E : Type} {n : ℕ} (s : NQuantScope E n) (default : E) : Type

Equations

• s.𝔖 default = ((σ : Cooper2023Ch8.ScopeOrdering n) × s.readingAt σ default)

def Cooper2023Ch8.surfaceOrder₂ : ScopeOrdering 2

Equations

• Cooper2023Ch8.surfaceOrder₂ = { order := [⟨0, Cooper2023Ch8.surfaceOrder₂._proof_3⟩, ⟨1, Cooper2023Ch8.surfaceOrder₂._proof_4⟩], complete := Cooper2023Ch8.surfaceOrder₂._proof_5 }

def Cooper2023Ch8.inverseOrder₂ : ScopeOrdering 2

Equations

• Cooper2023Ch8.inverseOrder₂ = { order := [⟨1, Cooper2023Ch8.surfaceOrder₂._proof_4⟩, ⟨0, Cooper2023Ch8.surfaceOrder₂._proof_3⟩], complete := Cooper2023Ch8.inverseOrder₂._proof_1 }

def Cooper2023Ch8.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" — three quantifiers

Cooper §8.2 does not analyse this case; the six orderings constructed here are the formaliser's combinatorial enumeration.

inductive Cooper2023Ch8.ThreeQInd : Type

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

@[implicit_reducible]

instance Cooper2023Ch8.instDecidableEqThreeQInd : DecidableEq ThreeQInd

Equations

• Cooper2023Ch8.instDecidableEqThreeQInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch8.isSomeone₃ : Semantics.TypeTheoretic.Ppty ThreeQInd

Equations

• Cooper2023Ch8.isSomeone₃ Cooper2023Ch8.ThreeQInd.alice = PUnit.{1}
• Cooper2023Ch8.isSomeone₃ Cooper2023Ch8.ThreeQInd.bob = PUnit.{1}
• Cooper2023Ch8.isSomeone₃ x✝ = Empty

def Cooper2023Ch8.isChild₃ : Semantics.TypeTheoretic.Ppty ThreeQInd

Equations

• Cooper2023Ch8.isChild₃ Cooper2023Ch8.ThreeQInd.child1 = PUnit.{1}
• Cooper2023Ch8.isChild₃ Cooper2023Ch8.ThreeQInd.child2 = PUnit.{1}
• Cooper2023Ch8.isChild₃ x✝ = Empty

def Cooper2023Ch8.isPresent₃ : Semantics.TypeTheoretic.Ppty ThreeQInd

Equations

• Cooper2023Ch8.isPresent₃ Cooper2023Ch8.ThreeQInd.present1 = PUnit.{1}
• Cooper2023Ch8.isPresent₃ Cooper2023Ch8.ThreeQInd.present2 = PUnit.{1}
• Cooper2023Ch8.isPresent₃ x✝ = Empty

def Cooper2023Ch8.gave₃ : ThreeQInd → ThreeQInd → ThreeQInd → Type

Equations

• Cooper2023Ch8.gave₃ Cooper2023Ch8.ThreeQInd.alice Cooper2023Ch8.ThreeQInd.child1 Cooper2023Ch8.ThreeQInd.present1 = PUnit.{1}
• Cooper2023Ch8.gave₃ Cooper2023Ch8.ThreeQInd.alice Cooper2023Ch8.ThreeQInd.child2 Cooper2023Ch8.ThreeQInd.present2 = PUnit.{1}
• Cooper2023Ch8.gave₃ x✝² x✝¹ x✝ = Empty

def Cooper2023Ch8.someoneQ₃ : Semantics.TypeTheoretic.Quant ThreeQInd

Equations

• Cooper2023Ch8.someoneQ₃ = Semantics.TypeTheoretic.semIndefArt Cooper2023Ch8.isSomeone₃

def Cooper2023Ch8.everyChildQ₃ : Semantics.TypeTheoretic.Quant ThreeQInd

Equations

• Cooper2023Ch8.everyChildQ₃ = Semantics.TypeTheoretic.semUniversal Cooper2023Ch8.isChild₃

def Cooper2023Ch8.aPresentQ₃ : Semantics.TypeTheoretic.Quant ThreeQInd

Equations

• Cooper2023Ch8.aPresentQ₃ = Semantics.TypeTheoretic.semIndefArt Cooper2023Ch8.isPresent₃

def Cooper2023Ch8.someoneGaveEveryChildAPresent : NQuantScope ThreeQInd 3

Equations

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

def Cooper2023Ch8.scopeOrdering₃_012 : ScopeOrdering 3

Equations

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

def Cooper2023Ch8.scopeOrdering₃_021 : ScopeOrdering 3

Equations

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

def Cooper2023Ch8.scopeOrdering₃_102 : ScopeOrdering 3

Equations

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

def Cooper2023Ch8.scopeOrdering₃_120 : ScopeOrdering 3

Equations

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

def Cooper2023Ch8.scopeOrdering₃_201 : ScopeOrdering 3

Equations

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

def Cooper2023Ch8.scopeOrdering₃_210 : ScopeOrdering 3

Equations

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

theorem Cooper2023Ch8.six_distinct_orderings_for_n_eq_3 : [scopeOrdering₃_012, scopeOrdering₃_021, scopeOrdering₃_102, scopeOrdering₃_120, scopeOrdering₃_201, scopeOrdering₃_210].length = 6

Cross-sentential anaphora (Cooper §8.3)

"A man walked. He whistled." The pronoun resolves to the indefinite via asymmetric merge under label 𝔭: the previous sentence's foreground becomes the current sentence's background.

structure Cooper2023Ch8.DiscourseContext (E PrevContent : Type) : Type 1

Discourse merge under label 𝔭: the previous sentence's content becomes a background field of the current context.

• 𝔭 : PrevContent
• current : Cntxt₈ E

def Cooper2023Ch8.crossSententialResolve {E : Type} {P : E → Type} (prev : (x : E) × P x) : E

Cross-sentential resolution: project the individual from the previous sentence's sigma-typed content.

Equations

• Cooper2023Ch8.crossSententialResolve prev = prev.fst

inductive Cooper2023Ch8.CSInd : Type

• john : CSInd
• mary : CSInd

@[implicit_reducible]

instance Cooper2023Ch8.instDecidableEqCSInd : DecidableEq CSInd

Equations

• Cooper2023Ch8.instDecidableEqCSInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch8.isMan : Semantics.TypeTheoretic.Ppty CSInd

Equations

• Cooper2023Ch8.isMan Cooper2023Ch8.CSInd.john = PUnit.{1}
• Cooper2023Ch8.isMan Cooper2023Ch8.CSInd.mary = Empty

def Cooper2023Ch8.walked₈ : Semantics.TypeTheoretic.Ppty CSInd

Equations

• Cooper2023Ch8.walked₈ Cooper2023Ch8.CSInd.john = PUnit.{1}
• Cooper2023Ch8.walked₈ Cooper2023Ch8.CSInd.mary = Empty

def Cooper2023Ch8.whistled₈ : Semantics.TypeTheoretic.Ppty CSInd

Equations

• Cooper2023Ch8.whistled₈ Cooper2023Ch8.CSInd.john = PUnit.{1}
• Cooper2023Ch8.whistled₈ Cooper2023Ch8.CSInd.mary = Empty

def Cooper2023Ch8.aManWalked : (x : CSInd) × isMan x × walked₈ x

Equations

• Cooper2023Ch8.aManWalked = ⟨Cooper2023Ch8.CSInd.john, (PUnit.unit, PUnit.unit)⟩

def Cooper2023Ch8.heWhistled (referent : CSInd) : Type

Equations

• Cooper2023Ch8.heWhistled referent = Cooper2023Ch8.whistled₈ referent

def Cooper2023Ch8.resolvedHe : CSInd

Equations

• Cooper2023Ch8.resolvedHe = Cooper2023Ch8.crossSententialResolve Cooper2023Ch8.aManWalked

theorem Cooper2023Ch8.resolvedHe_is_john : resolvedHe = CSInd.john

def Cooper2023Ch8.manWalkedHeWhistled : Type

Equations

• Cooper2023Ch8.manWalkedHeWhistled = ((x : Cooper2023Ch8.CSInd) × Cooper2023Ch8.isMan x × Cooper2023Ch8.walked₈ x × Cooper2023Ch8.whistled₈ x)

def Cooper2023Ch8.manWalkedHeWhistledWitness : manWalkedHeWhistled

Equations

• Cooper2023Ch8.manWalkedHeWhistledWitness = ⟨Cooper2023Ch8.CSInd.john, (PUnit.unit, PUnit.unit, PUnit.unit)⟩

theorem Cooper2023Ch8.crossSentential_correct : ∃ (w : manWalkedHeWhistled), w.fst = crossSententialResolve aManWalked

"No dog which chases a cat catches it"

Cooper §8.3 primary donkey example combining negation, localization, and path alignment.

def Cooper2023Ch8.alignPaths {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (align : P.Bg → P.Bg) : Semantics.TypeTheoretic.PPpty E

Path alignment (Cooper §8.3 eq 52, App A11.8): replace path π₁ with π₂ in a parametric property. In Cooper's full TTR this is a type operation T_{π₁ = π₂} creating a manifest field; here we simplify to a relabelling of the background.

Equations

• Cooper2023Ch8.alignPaths P align = { Bg := P.Bg, fg := fun (c : P.Bg) => P.fg (align c) }

inductive Cooper2023Ch8.DonkeyNegInd : Type

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

@[implicit_reducible]

instance Cooper2023Ch8.instDecidableEqDonkeyNegInd : DecidableEq DonkeyNegInd

Equations

• Cooper2023Ch8.instDecidableEqDonkeyNegInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch8.isDog₈ₙ : Semantics.TypeTheoretic.Ppty DonkeyNegInd

Equations

• Cooper2023Ch8.isDog₈ₙ Cooper2023Ch8.DonkeyNegInd.dog1 = PUnit.{1}
• Cooper2023Ch8.isDog₈ₙ Cooper2023Ch8.DonkeyNegInd.dog2 = PUnit.{1}
• Cooper2023Ch8.isDog₈ₙ x✝ = Empty

def Cooper2023Ch8.isCat₈ : Semantics.TypeTheoretic.Ppty DonkeyNegInd

Equations

• Cooper2023Ch8.isCat₈ Cooper2023Ch8.DonkeyNegInd.cat1 = PUnit.{1}
• Cooper2023Ch8.isCat₈ Cooper2023Ch8.DonkeyNegInd.cat2 = PUnit.{1}
• Cooper2023Ch8.isCat₈ x✝ = Empty

def Cooper2023Ch8.chases₈ : DonkeyNegInd → DonkeyNegInd → Type

Equations

• Cooper2023Ch8.chases₈ Cooper2023Ch8.DonkeyNegInd.dog1 Cooper2023Ch8.DonkeyNegInd.cat1 = PUnit.{1}
• Cooper2023Ch8.chases₈ Cooper2023Ch8.DonkeyNegInd.dog2 Cooper2023Ch8.DonkeyNegInd.cat2 = PUnit.{1}
• Cooper2023Ch8.chases₈ x✝¹ x✝ = Empty

@[reducible, inline]

abbrev Cooper2023Ch8.CatBg : Type

Equations

• Cooper2023Ch8.CatBg = ((c : Cooper2023Ch8.DonkeyNegInd) × Cooper2023Ch8.isCat₈ c)

def Cooper2023Ch8.dogChasesACat : Semantics.TypeTheoretic.Ppty DonkeyNegInd

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

Equations

• Cooper2023Ch8.dogChasesACat x = (Cooper2023Ch8.isDog₈ₙ x × (c : Cooper2023Ch8.CatBg) × Cooper2023Ch8.chases₈ x c.fst)

def Cooper2023Ch8.catches₈_none : DonkeyNegInd → DonkeyNegInd → Type

Equations

• Cooper2023Ch8.catches₈_none x✝¹ x✝ = Empty

def Cooper2023Ch8.catches₈_all : DonkeyNegInd → DonkeyNegInd → Type

Equations

• Cooper2023Ch8.catches₈_all = Cooper2023Ch8.chases₈

def Cooper2023Ch8.semNo₈ (restr scope : Semantics.TypeTheoretic.Ppty DonkeyNegInd) : Type

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

Equations

• Cooper2023Ch8.semNo₈ restr scope = ((x : Cooper2023Ch8.DonkeyNegInd) → restr x → scope x → Empty)

def Cooper2023Ch8.noDogCatchesCatWitness : semNo₈ dogChasesACat fun (x : DonkeyNegInd) => (c : CatBg) × catches₈_none x c.fst

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

"No dog which chases a cat catches it" is true when no dog catches the cat it chases.

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

"No dog which chases a cat catches it" is false when every dog catches the cat it chases.

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

The negation donkey case uses ℒ — the same localization mechanism as the classic farmer/donkey example.