Charlow (2014) — The Side-Effects Dichotomy in Dynamic Anaphora

@cite{charlow-2014} @cite{sutton-2024} @cite{groenendijk-stokhof-1991} @cite{kamp-reyle-1993} @cite{muskens-1996} @cite{cooper-2023}

@cite{charlow-2014} Ch. 2 ("Dynamic side effects") recasts dynamic semantics in terms of side effects in the monadic sense: state-threading frameworks (DPL, DRT, CDRT, BUS) all use a state monad — externally static negation falls out because negation is a test on the state. Type-theoretic frameworks (TTR, MTT) use Σ-type witness persistence — externally dynamic negation falls out because the witness type survives independently of any state.

@cite{sutton-2024} §6.2 surveys the same dichotomy from the type-theory side: RTT donkey approaches (Sundholm 1986, Ranta 1994, Bekki 2014, Cooper 2023, Luo 2021) use Σ/Π-types, contrasting with the Frege-Church-Montague tradition.

This study formalises the dichotomy as a single theorem rather than the ugly four-way conjunction of pairwise comparisons. Four anaphora frameworks are registered as AnaphoraFramework instances; the headline anaphora_quartet theorem unpacks them with two facts:

1. Truth-conditional consilience: every framework agrees with the classical universal-reading donkey (∀ x y, F x → D y → O x y → B x y).
2. Dref-preservation dichotomy: dref accessibility under negation is preserved iff the framework's representational strategy is typeStructure (TTR) rather than stateThreading (DRT/DPL/CDRT).

Each instance delegates to the existing study/substrate file rather than re-stipulating the framework's primitives. The AnaphoraFramework record is local — earned by exactly one consumer (this file's headline theorem) and not promoted to substrate. If a similar quartet appears in another phenomenon (e.g., a Modality quartet built on the existing Cooper-Kratzer bridge), the record can promote to Theories/Semantics/Anaphora/Framework.lean at that point.

Anchoring

Charlow 2014 Ch. 2 is the canonical source for the side-effects / state-threading dichotomy. Sutton 2024 §6.2 is the cross-framework anaphora survey. Cooper 2023 §8.5 supplies the type-structure side of the dichotomy. Each of DPL, DRT, CDRT supplies one stateful framework.

def Studies.Anaphora.Charlow2014.Examples.donkey1 : Data.Examples.LinguisticExample

Equations

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

def Studies.Anaphora.Charlow2014.Examples.all : List Data.Examples.LinguisticExample

Equations

• Studies.Anaphora.Charlow2014.Examples.all = [Studies.Anaphora.Charlow2014.Examples.donkey1]

inductive Studies.Anaphora.Charlow2014.RepStrategy : Type

The two representational strategies @cite{charlow-2014} Ch. 2 identifies in dynamic anaphora.

• stateThreading — DPL, DRT, CDRT, BUS, and other state-monadic frameworks. Negation is a test on the state; drefs introduced inside negation do not survive externally.
• typeStructure — TTR (Cooper 2023), MTT (Luo, Chatzikyriakidis). Drefs are Σ-type projections; the witness type persists independently of any state machinery, so negation does not destroy it.

• stateThreading : RepStrategy
• typeStructure : RepStrategy

def Studies.Anaphora.Charlow2014.instReprRepStrategy.repr : RepStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Studies.Anaphora.Charlow2014.instReprRepStrategy : Repr RepStrategy

Equations

• Studies.Anaphora.Charlow2014.instReprRepStrategy = { reprPrec := Studies.Anaphora.Charlow2014.instReprRepStrategy.repr }

@[implicit_reducible]

instance Studies.Anaphora.Charlow2014.instDecidableEqRepStrategy : DecidableEq RepStrategy

Equations

• Studies.Anaphora.Charlow2014.instDecidableEqRepStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Studies.Anaphora.Charlow2014.classicalDonkey {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : Prop

Classical universal-reading donkey: "every farmer who owns a donkey beats it" interpreted via plain ∀∀. The four frameworks below each prove their native encoding agrees with this.

The CLDF-typed surface form of this example lives in Examples.donkey1 above, with provenance recorded as Geach 1962. The two cannot be definitionally bridged — classicalDonkey is a Prop parameterised over abstract predicates (farmer, donkey, owns, beats); the typed example carries a sentence string + Leipzig gloss. They are two different representations of the same datum: one for proofs (Prop), one for citation/data-exchange (LinguisticExample).

Equations

• Studies.Anaphora.Charlow2014.classicalDonkey farmer donkey owns beats = ∀ (x y : E), farmer x → donkey y → owns x y → beats x y

structure Studies.Anaphora.Charlow2014.AnaphoraFramework {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : Type

A registered anaphora framework, parameterised over the lexical predicates of the donkey scenario. Four instances follow.

The two load-bearing fields are:

• donkey_iff_classical — the framework's encoding of the Geach donkey is truth-conditionally equivalent to classicalDonkey. All four frameworks satisfy this (Charlow 2014 Ch. 2, Sutton 2024 §6.2).
• preservation_iff_typeStructure — the framework's negation preserves dref accessibility iff its strategy is typeStructure. This is the side-effects dichotomy made decidable.

• name : String

  Author-year identifier (e.g. "DPL (Groenendijk-Stokhof 1991)")

• strategy : RepStrategy

  The framework's representational strategy

• donkeyHolds : Prop

  The framework's truth condition for the Geach donkey

• donkey_iff_classical : self.donkeyHolds ↔ classicalDonkey farmer donkey owns beats

  The framework's encoding agrees with the classical universal

• negPreservesDref : Bool

  Whether negation preserves dref accessibility

• preservation_iff_typeStructure : self.negPreservesDref = true ↔ self.strategy = RepStrategy.typeStructure

  The dichotomy: dref preservation iff type-structure representation

DRT (Kamp & Reyle 1993)

Donkey encoding: [| ⟨[u₁ u₂ | farmer u₁, donkey u₂, owns u₁ u₂] ⇒ [| beats u₁ u₂]⟩] (the exDonkeyStandalone DRS). Truth equivalence: donkey_universal_reading (Phenomena/Anaphora/Studies/KampReyle1993.lean). Negation: subordinating box; drefs introduced inside neg boxes are inaccessible to successor sentences.

def Studies.Anaphora.Charlow2014.drt {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : AnaphoraFramework farmer donkey owns beats

Equations

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

DPL (Groenendijk & Stokhof 1991)

Donkey encoding: DPLRel.impl (∃x. farmer x ∧ ∃y. donkey y ∧ owns x y) (beats x y). By donkey_equivalence + scope_extension, this DPL formula has universal force. Truth equivalence reduces to the classical universal under DPL's externally-dynamic existential. Negation: DPLRel.neg φ := λ g h => g = h ∧ ¬ ∃ k, φ g k. The output assignment equals the input; drefs from inside negation are dropped (dpl_dne_fails_anaphora).

def Studies.Anaphora.Charlow2014.dpl {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : AnaphoraFramework farmer donkey owns beats

Equations

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

CDRT (Muskens 1996)

Donkey encoding: cdrt_full_donkey (Cooper2023.lean §4): DProp.impl (DProp.new 0 ;; ofStatic (farmer ∘ ·0) ;; DProp.new 1 ;; ofStatic (donkey ∘ ·1 ∧ owns ·0 ·1)) (ofStatic (beats ·0 ·1)). Truth equivalence: full_donkey_equiv (Cooper2023 §4) + Π-type classical reduction. Negation: DProp.neg φ := λ i o => i = o ∧ ¬ ∃ k, φ i k. Output register equals input; drefs from inside negation are dropped (neg_destroys_dref, dne_same_truth in Cooper2023 §5).

def Studies.Anaphora.Charlow2014.cdrt {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : AnaphoraFramework farmer donkey owns beats

Equations

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

TTR (Cooper 2023)

Donkey encoding: ttr_full_donkey farmer donkey owns beats := (x : E) → farmer x → (y : E) → donkey y → owns x y → propT (beats x y) (Cooper2023.lean §4). The Π-type form makes the universal-reading donkey structurally inevitable. Truth equivalence: PLift unwrap + curry. Negation: TTR has no state to mutate. The Σ-type (x : E) × P x carries its witness structurally; the projection Sigma.fst is always available regardless of logical context (ttr_witness_survives in Cooper2023 §5).

def Studies.Anaphora.Charlow2014.ttr {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : AnaphoraFramework farmer donkey owns beats

Equations

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

def Studies.Anaphora.Charlow2014.supported {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : List (AnaphoraFramework farmer donkey owns beats)

The supported quartet. New instances (Heim 1982, Charlow 2018/2019, Hofmann 2025, BUS, ...) can be registered by adding to this list and extending the headline theorem's case-analysis hypothesis.

Equations

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

theorem Studies.Anaphora.Charlow2014.anaphora_quartet {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) (F : AnaphoraFramework farmer donkey owns beats) : F ∈ supported farmer donkey owns beats → (F.donkeyHolds ↔ classicalDonkey farmer donkey owns beats) ∧ (F.negPreservesDref = true ↔ F.strategy = RepStrategy.typeStructure)

The Anaphora Quartet (@cite{charlow-2014} Ch. 2; @cite{sutton-2024} §6.2).

Every supported framework satisfies two facts: (i) its donkey encoding is truth-conditionally equivalent to the classical universal reading, and (ii) its negation preserves dref accessibility iff its representational strategy is typeStructure.

The proof is a one-liner: both facts are recorded as fields of the AnaphoraFramework record, and each instance proves them once. The headline theorem unpacks the structure. The "ugly conjunction" version (spelling out four donkeyHolds ↔ donkeyHolds agreements and four negPreservesDref discriminations) collapses into the single quantified statement below.

theorem Studies.Anaphora.Charlow2014.donkey_truth_consilience {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) (F G : AnaphoraFramework farmer donkey owns beats) (hF : F ∈ supported farmer donkey owns beats) (hG : G ∈ supported farmer donkey owns beats) : F.donkeyHolds ↔ G.donkeyHolds

Truth-conditional consilience: any two supported frameworks agree on the truth conditions of the Geach donkey, regardless of their representational strategy. The disagreement is not about truth.

theorem Studies.Anaphora.Charlow2014.dref_preservation_partition {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : (∀ F ∈ supported farmer donkey owns beats, F.strategy = RepStrategy.stateThreading → F.negPreservesDref = false) ∧ ∀ F ∈ supported farmer donkey owns beats, F.strategy = RepStrategy.typeStructure → F.negPreservesDref = true

Dref-preservation partition: the supported quartet partitions into state-threading frameworks (no dref preservation under negation) and type-structure frameworks (dref preservation under negation). The partition is the side-effects dichotomy from Charlow 2014 Ch. 2.

theorem Studies.Anaphora.Charlow2014.three_vs_one_disagreement {E : Type} (farmer donkey : E → Prop) (owns beats : E → E → Prop) : (drt farmer donkey owns beats).negPreservesDref = false ∧ (dpl farmer donkey owns beats).negPreservesDref = false ∧ (cdrt farmer donkey owns beats).negPreservesDref = false ∧ (ttr farmer donkey owns beats).negPreservesDref = true

Three-vs-one disagreement: among the supported quartet, exactly the three state-threading frameworks (DRT, DPL, CDRT) lose drefs under negation, and exactly the one type-structure framework (TTR) preserves them. This is the empirical content of the Charlow 2014 dichotomy specialised to the four canonical instances.

theorem Studies.Anaphora.Charlow2014.geach_example_id : Examples.donkey1.id = "charlow2014_donkey1"

The Geach donkey example carries the expected stable ID. Anchors the example for grep-based discovery across the codebase: a search for charlow2014_donkey1 returns every theorem (in any study) that references this datum.

theorem Studies.Anaphora.Charlow2014.geach_example_source : Examples.donkey1.source.bibkey = "geach-1962"

Provenance check: the example's source.bibkey correctly attributes the Geach donkey to Geach 1962 (rather than to Charlow 2014, the paper whose CSV file owns this row). Catches CSV regressions where a contributor edits Source_Bibkey and breaks attribution.