Cooper (2023) — TTR Underspecification @cite{cooper-2023} #
Connects TTR underspecification to anaphora data, drawing on @cite{kanazawa-1994}, @cite{groenendijk-stokhof-1991}, @cite{muskens-1996}, @cite{sutton-2024}, @cite{chomsky-1981}.
Connects TTR's localization (donkey anaphora) and binding theory
(reflexivization, anaphoric resolution) from
Theories.Semantics.TypeTheoretic.Underspecification to the empirical
data in Phenomena.Anaphora.DonkeyAnaphora and
Phenomena.Anaphora.Coreference.
Per-datum verification: each theorem verifies one data point from the Phenomena files against TTR predictions.
§§ 4–5 establish the truth-conditional bridge from CDRT (Dynamic/CDRT/Basic.lean, @cite{muskens-1996}) 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 @cite{sutton-2024}.
Per-datum verification: TTR predictions match empirical data #
Connect the TTR localization analysis to the theory-neutral donkey
anaphora data in Phenomena.Anaphora.DonkeyAnaphora. Each theorem
verifies one data point: the empirical datum 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.
Geach donkey: weak reading available -- TTR predicts checkmark.
geachDonkey.weakReading = true and TTR produces a weak (localize) witness
for both farmers in the scenario.
Geach donkey: bound reading — TTR confirms the pronoun depends on the indefinite via parametric background (the donkey is the Bg).
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 theory-neutral binding
data in Phenomena.Anaphora.Coreference.
@cite{cooper-2023} Ch8 section 8.3 gives a type-theoretic account of @cite{chomsky-1981}'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 Coreference.lean.
Changing reflexivize or anaphoricResolve will break these bridges.
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 reflexivePattern from Phenomena.
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 pronounPattern from Phenomena.
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 complementaryDistributionData from Phenomena.
The main bridge theorem (bridge theorem 3): TTR's reflexivization predicts the binding data.
- Reflexivization forces local coreference (Condition A): Cooper eq (84)
- Anaphoric resolution allows disjoint reference (Condition B): Cooper eq (28)
- The empirical coreference patterns match: @cite{chomsky-1981}
- Reflexivization = anaphoricResolve with id: reflexivization is a special case
CDRT (Dynamic/CDRT/Basic.lean, @cite{muskens-1996}) and TTR (TypeTheoretic/, @cite{cooper-2023}) 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.
CDRT existential: introduce dref n, test P on r(n).
Equations
Instances For
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
- Studies.Anaphora.Cooper2023.ttr_exists P = ((x : E) × Semantics.TypeTheoretic.propT (P x))
Instances For
Equivalence 1: CDRT dref introduction and TTR Σ-type have
the same truth conditions. Both reduce to ∃ x, P x.
Both reduce to classical ∃.
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.
Instances For
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
- Studies.Anaphora.Cooper2023.ttr_donkey P Q = ((x : E) → P x → Semantics.TypeTheoretic.propT (Q x))
Instances For
Equivalence 2: CDRT donkey implication and TTR Π-type have
the same truth conditions. Both reduce to ∀ x, P x → Q x.
Both reduce to classical ∀→.
Two-variable donkey #
"Every farmer who owns a donkey beats it."
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Studies.Anaphora.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))
Instances For
Equivalence 3: The full donkey sentence has the same truth conditions in CDRT and TTR.
Connection to TTR's purify / purifyUniv #
The parametric property whose purification is ttr_exists P.
Equations
- Studies.Anaphora.Cooper2023.ttr_exists_as_pppty P = { Bg := E, fg := fun (x x_1 : E) => Semantics.TypeTheoretic.propT (P x) }
Instances For
purify of the existential parametric property is definitionally ttr_exists.
The parametric property whose universal purification is ttr_donkey.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 Poutputs a register withnbound → dref availableneg (new n; test P)outputsiunchanged → 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
(Theories/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.
In CDRT, negation destroys anaphoric potential. After ¬φ, the
output register is unchanged from input — any drefs introduced by φ
are inaccessible.
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).
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 #
Equations
- Studies.Anaphora.Cooper2023.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
CDRT donkey sentence is true on this model.
TTR donkey sentence is true on this model.
The two concrete results agree (by the equivalence theorem).