Cooper (2023) — TTR Underspecification [Coo23]

Connects TTR underspecification to anaphora data, drawing on [Kan94], [GS91], [Mus96], [Sut24], [Cho81].

Connects TTR's localization (donkey anaphora) and binding theory (reflexivization, anaphoric resolution) from Semantics.TypeTheoretic.Underspecification to the donkey rows in Data/Examples/Geach1962.json / Kanazawa1994.json and the binding paradigm in Studies/Chomsky1981.lean.

Per-datum verification: each theorem verifies one data point against TTR predictions.

§§ 4–5 establish the truth-conditional bridge from CDRT (Dynamic/CDRT/Basic.lean, [Mus96]) to TTR for the existential and donkey-implication core, and the divergence under negation: TTR and CDRT agree on truth conditions but differ on anaphoric potential (state-threading vs. type-structure). This is the formal correspondence surveyed in [Sut24].

Per-datum verification: TTR predictions match empirical data

Connect the TTR localization analysis to the donkey rows in Data/Examples/Geach1962.json and Kanazawa1994.json. Each theorem verifies one data point: the row records a reading as available, and TTR produces a witness for that reading.

Changing a Ppty (e.g., making beats asymmetric) will break exactly the theorems whose empirical predictions depend on it.

theorem Cooper2023.geach_weak_available : Geach1962.Examples.donkey_classic.readings.contains ("weak/existential", Features.Judgment.acceptable) = true ∧ Nonempty (Cooper2023Ch8.localize Cooper2023Ch8.farmerOwnsBeatsDonkey Cooper2023Ch8.DonkeyInd.farmer1) ∧ Nonempty (Cooper2023Ch8.localize Cooper2023Ch8.farmerOwnsBeatsDonkey Cooper2023Ch8.DonkeyInd.farmer2)

Geach donkey: weak reading available -- TTR predicts checkmark. The row records the weak/existential reading and TTR produces a weak (localize) witness for both farmers in the scenario.

theorem Cooper2023.geach_bound_reading : Geach1962.Examples.donkey_classic.readings.contains ("bound", Features.Judgment.acceptable) = true ∧ Cooper2023Ch8.farmerOwnsBeatsDonkey.Bg = Cooper2023Ch8.DonkeyBg

Geach donkey: bound reading — TTR confirms the pronoun depends on the indefinite via parametric background (the donkey is the Bg).

theorem Cooper2023.strongDominant_readings_available : Kanazawa1994.Examples.strong_dominant.readings.contains ("strong/universal", Features.Judgment.acceptable) = true ∧ Kanazawa1994.Examples.strong_dominant.readings.contains ("weak/existential", Features.Judgment.acceptable) = true ∧ Nonempty (Cooper2023Ch8.localize Cooper2023Ch8.farmerOwnsBeatsDonkey Cooper2023Ch8.DonkeyInd.farmer1)

Strong dominant: TTR records the weak reading is available (ℒ produces a witness). The conditional-strong reading via the formaliser-invented localizeConditional was deleted in 0.230.564 (per audit: Cooper's own strong-donkey mechanism is 𝔓^∀ over an indexed background, not a separate conditional gate; see TODO note in Cooper2023Ch8.lean DonkeyAnaphora section).

Per-datum verification: binding predictions match coreference data

Connect TTR's reflexivization and anaphoric resolution to the binding paradigm in Studies/Chomsky1981.lean.

[Coo23] Ch8 section 8.3 gives a type-theoretic account of [Cho81]'s binding conditions:

• Condition A (reflexives must be locally bound): reflexivization forces argument identity
• Condition B (pronouns must be locally free): anaphoric resolution with disjoint reference
• Complementary distribution: reflexivization vs anaphoric resolution for the same position

Each theorem verifies one empirical pattern from Studies/Chomsky1981.lean. Changing reflexivize or anaphoricResolve will break these bridges.

theorem Cooper2023.reflexive_predicts_condA : Chomsky1981.reflexivePattern.requiresAntecedent = true ∧ Chomsky1981.reflexivePattern.antecedentDomain = some Chomsky1981.Domain.local_ ∧ ∀ (R : Cooper2023Ch8.BindInd → Cooper2023Ch8.BindInd → Type) (x : Cooper2023Ch8.BindInd), Cooper2023Ch8.reflexivize R x = R x x

TTR's reflexivization predicts Binding Condition A: reflexives require a local antecedent because reflexivization forces argument identity within the local clause. Cooper Ch8, eq (84) + (88): reflexivization at VP level binds reflexive to subject. Matches Chomsky1981.reflexivePattern.

theorem Cooper2023.pronoun_predicts_condB : Chomsky1981.pronounPattern.requiresAntecedent = false ∧ Chomsky1981.pronounPattern.antecedentDomain = some Chomsky1981.Domain.nonlocal ∧ ∀ (y x : Cooper2023Ch8.BindInd), Cooper2023Ch8.anaphoricResolve Cooper2023Ch8.likeParam (fun (x : Cooper2023Ch8.BindInd) => y) x = Cooper2023Ch8.like₈ x y

TTR predicts Binding Condition B: pronouns allow disjoint reference via anaphoric resolution with a constant function (the assignment provides the referent from non-local context). Cooper Ch8, eq (28). Matches Chomsky1981.pronounPattern.

theorem Cooper2023.complementary_distribution_predicted : Chomsky1981.reflexivePattern.anaphorType = Chomsky1981.AnaphorType.reflexive ∧ Chomsky1981.pronounPattern.anaphorType = Chomsky1981.AnaphorType.pronoun ∧ Nonempty (Cooper2023Ch8.reflexivize Cooper2023Ch8.like₈ Cooper2023Ch8.BindInd.sam) ∧ Nonempty (Cooper2023Ch8.anaphoricResolve Cooper2023Ch8.likeParam (fun (x : Cooper2023Ch8.BindInd) => Cooper2023Ch8.BindInd.bill) Cooper2023Ch8.BindInd.sam)

Complementary distribution: reflexive and pronoun are predicted by different TTR mechanisms (reflexivization vs anaphoric resolution). Cooper Ch8, eqs (67)-(73): "Sam likes him" is NOT appropriate for "Sam likes himself" -- reflexivization must be used instead. Matches Chomsky1981.complementaryDistributionData.

theorem Cooper2023.reflexive_predicts_binding : (∀ (R : Cooper2023Ch8.BindInd → Cooper2023Ch8.BindInd → Type) (x : Cooper2023Ch8.BindInd), Cooper2023Ch8.reflexivize R x = R x x) ∧ (∀ (y x : Cooper2023Ch8.BindInd), Cooper2023Ch8.anaphoricResolve Cooper2023Ch8.likeParam (fun (x : Cooper2023Ch8.BindInd) => y) x = Cooper2023Ch8.like₈ x y) ∧ Cooper2023Ch8.anaphoricResolve Cooper2023Ch8.likeParam id = Cooper2023Ch8.reflexivize Cooper2023Ch8.like₈ ∧ Chomsky1981.reflexivePattern.requiresAntecedent = true ∧ Chomsky1981.pronounPattern.requiresAntecedent = false ∧ Chomsky1981.reflexivePattern.antecedentDomain = some Chomsky1981.Domain.local_ ∧ Chomsky1981.pronounPattern.antecedentDomain = some Chomsky1981.Domain.nonlocal

The main bridge theorem (bridge theorem 3): TTR's reflexivization predicts the binding data.

1. Reflexivization forces local coreference (Condition A): Cooper eq (84)
2. Anaphoric resolution allows disjoint reference (Condition B): Cooper eq (28)
3. The empirical coreference patterns match: [Cho81]
4. Reflexivization = anaphoricResolve with id: reflexivization is a special case

CDRT (Dynamic/CDRT/Basic.lean, [Mus96]) and TTR (TypeTheoretic/, [Coo23]) handle overlapping anaphora phenomena — discourse referents, donkey anaphora, cross-sentential binding — with no shared infrastructure. This section proves they agree on truth conditions for the existential and donkey cores, and identifies where they diverge (§ 5).

Dynamic (CDRT)	Type-Theoretic (TTR)	Classical
DProp.ofStatic p	propT (p i)	p i
DProp.new n; test P	Σ (x : E), P x	∃ x, P x
DProp.impl (new;P) Q	Π (x : E), P x → Q x	∀ x, P x → Q x

The first column is state-threading (assignments as side effects); the second is type-dependency (witnesses as structure). Both reduce to the same classical truth conditions.

def Cooper2023.cdrt_exists {E : Type} (n : ℕ) (P : E → Prop) : Semantics.Dynamic.CDRT.DProp E

CDRT existential: introduce dref n, test P on r(n).

Equations

• Cooper2023.cdrt_exists n P = Semantics.Dynamic.CDRT.DProp.new n ;; Semantics.Dynamic.CDRT.DProp.ofStatic fun (r : Semantics.Dynamic.CDRT.Register E) => P (r n)

def Cooper2023.ttr_exists {E : Type} (P : E → Prop) : Type

TTR existential: Σ-type with entity witness. This is purify applied to a parametric property with background E; the result doesn't depend on the input, so we state it directly.

Equations

• Cooper2023.ttr_exists P = ((x : E) × Semantics.TypeTheoretic.propT (P x))

theorem Cooper2023.exists_equiv {E : Type} (n : ℕ) (P : E → Prop) (i : Semantics.Dynamic.CDRT.Register E) : (cdrt_exists n P).true_at i ↔ Nonempty (ttr_exists P)

Equivalence 1: CDRT dref introduction and TTR Σ-type have the same truth conditions. Both reduce to ∃ x, P x.

theorem Cooper2023.exists_classical {E : Type} (P : E → Prop) : Nonempty (ttr_exists P) ↔ ∃ (x : E), P x

Both reduce to classical ∃.

def Cooper2023.cdrt_donkey {E : Type} (n : ℕ) (P Q : E → Prop) : Semantics.Dynamic.CDRT.DProp E

CDRT donkey: impl(new n; test P, test Q). "For every way of extending the register with a P-entity at n, Q holds of that entity."

Equations

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

def Cooper2023.ttr_donkey {E : Type} (P Q : E → Prop) : Type

TTR donkey: Π-type over witnesses. "For every P-witness, Q holds." This is purifyUniv on the parametric property with background {x : E // P x}.

Equations

• Cooper2023.ttr_donkey P Q = ((x : E) → P x → Semantics.TypeTheoretic.propT (Q x))

theorem Cooper2023.donkey_equiv {E : Type} (n : ℕ) (P Q : E → Prop) (i : Semantics.Dynamic.CDRT.Register E) : (cdrt_donkey n P Q).true_at i ↔ Nonempty (ttr_donkey P Q)

Equivalence 2: CDRT donkey implication and TTR Π-type have the same truth conditions. Both reduce to ∀ x, P x → Q x.

theorem Cooper2023.donkey_classical {E : Type} (P Q : E → Prop) : Nonempty (ttr_donkey P Q) ↔ ∀ (x : E), P x → Q x

Both reduce to classical ∀→.

Two-variable donkey

"Every farmer who owns a donkey beats it."

def Cooper2023.cdrt_full_donkey {E : Type} (farmer donkey_ : E → Prop) (owns beats : E → E → Prop) : Semantics.Dynamic.CDRT.DProp E

Equations

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

def Cooper2023.ttr_full_donkey {E : Type} (farmer donkey_ : E → Prop) (owns beats : E → E → Prop) : Type

Equations

• Cooper2023.ttr_full_donkey farmer donkey_ owns beats = ((x : E) → farmer x → (y : E) → donkey_ y → owns x y → Semantics.TypeTheoretic.propT (beats x y))

theorem Cooper2023.full_donkey_equiv {E : Type} (farmer donkey_ : E → Prop) (owns beats : E → E → Prop) (i : Semantics.Dynamic.CDRT.Register E) : (cdrt_full_donkey farmer donkey_ owns beats).true_at i ↔ Nonempty (ttr_full_donkey farmer donkey_ owns beats)

Equivalence 3: The full donkey sentence has the same truth conditions in CDRT and TTR.

Connection to TTR's purify / purifyUniv

def Cooper2023.ttr_exists_as_pppty {E : Type} (P : E → Prop) : Semantics.TypeTheoretic.PPpty E

The parametric property whose purification is ttr_exists P.

Equations

• Cooper2023.ttr_exists_as_pppty P = { Bg := E, fg := fun (x x_1 : E) => Semantics.TypeTheoretic.propT (P x) }

theorem Cooper2023.purify_exists_eq {E : Type} (P : E → Prop) (a : E) : Cooper2023Ch7.purify (ttr_exists_as_pppty P) a = ttr_exists P

purify of the existential parametric property is definitionally ttr_exists.

def Cooper2023.ttr_donkey_as_pppty {E : Type} (P Q : E → Prop) : Semantics.TypeTheoretic.PPpty E

The parametric property whose universal purification is ttr_donkey.

Equations

• Cooper2023.ttr_donkey_as_pppty P Q = { Bg := { x : E // P x }, fg := fun (x : { x : E // P x }) (x_1 : E) => match x with | ⟨x, property⟩ => Semantics.TypeTheoretic.propT (Q x) }

theorem Cooper2023.purifyUniv_donkey_iff {E : Type} (P Q : E → Prop) (a : E) : Nonempty (Cooper2023Ch7.purifyUniv (ttr_donkey_as_pppty P Q) a) ↔ ∀ (x : E), P x → Q x

purifyUniv of the donkey parametric property is inhabited iff the donkey universal holds.

The systems agree on truth conditions but differ on discourse effect. CDRT tracks anaphoric potential via the output register: after processing φ, the output register determines what drefs are available for subsequent sentences.

• new n; test P outputs a register with n bound → dref available
• neg (new n; test P) outputs i unchanged → dref lost

TTR tracks anaphoric potential via type structure: the Σ-type (x : E) × P x makes x available as a projection, regardless of how many negations wrap it.

This is the architectural difference: CDRT uses state for binding; TTR uses structure. The bilateral DNE strategy (Semantics/Dynamic/Bilateral/Basic.lean) is a third approach — bilateral DNE is structural at the state level (swap is involutive), distinct from TTR's structural-at-the-type level. The three are surveyed in Dynamic/Core/DynProp.lean's "three incompatible DNE solutions" table.

theorem Cooper2023.neg_destroys_dref {E : Type} {φ : Semantics.Dynamic.CDRT.DProp E} (i o : Semantics.Dynamic.CDRT.Register E) (h : φ.neg i o) : o = i

In CDRT, negation destroys anaphoric potential. After ¬φ, the output register is unchanged from input — any drefs introduced by φ are inaccessible.

theorem Cooper2023.dne_same_truth {E : Type} (n : ℕ) (P : E → Prop) (i : Semantics.Dynamic.CDRT.Register E) : (cdrt_exists n P).neg.neg.true_at i ↔ (cdrt_exists n P).true_at i

Double negation preserves truth but not drefs. ¬¬(∃x.P(x)) has the same truth conditions as ∃x.P(x), but the output register is the input register (no binding).

theorem Cooper2023.ttr_witness_survives {E : Type} (P : E → Prop) (w : ttr_exists P) : ∃ (x : E), P x

In TTR there is no analogous destruction. The Σ-type (x : E) × P x carries its witness structurally; the projection Sigma.fst is always available, regardless of logical context.

Concrete two-variable donkey verification

inductive Cooper2023.Ent : Type

• john : Ent
• bill : Ent
• fido : Ent

@[implicit_reducible]

instance Cooper2023.instDecidableEqEnt : DecidableEq Ent

Equations

• Cooper2023.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

theorem Cooper2023.cdrt_donkey_concrete : (cdrt_full_donkey Cooper2023.farmerP✝ Cooper2023.donkeyP✝ Cooper2023.ownsP✝ Cooper2023.beatsP✝).true_at Cooper2023.initReg✝

CDRT donkey sentence is true on this model.

theorem Cooper2023.ttr_donkey_concrete : Nonempty (ttr_full_donkey Cooper2023.farmerP✝ Cooper2023.donkeyP✝ Cooper2023.ownsP✝ Cooper2023.beatsP✝)

TTR donkey sentence is true on this model.

theorem Cooper2023.concrete_agreement : (cdrt_full_donkey Cooper2023.farmerP✝ Cooper2023.donkeyP✝ Cooper2023.ownsP✝ Cooper2023.beatsP✝).true_at Cooper2023.initReg✝ ↔ Nonempty (ttr_full_donkey Cooper2023.farmerP✝ Cooper2023.donkeyP✝ Cooper2023.ownsP✝ Cooper2023.beatsP✝)

The two concrete results agree (by the equivalence theorem).