Mandelkern (2022) — Witnesses: the bounded theory of (in)definites

@cite{mandelkern-2022} @cite{heim-1982} @cite{groenendijk-stokhof-1991} @cite{krahmer-muskens-1995} @cite{karttunen-1976} @cite{schlenker-2009} @cite{stalnaker-1974} @cite{stalnaker-1978} @cite{dekker-1994} @cite{rothschild-2017}

@cite{mandelkern-2022} (Linguistics & Philosophy 45(5):1091-1117) develops the bounded theory of (in)definites: meanings have two dimensions — classical truth-conditions plus a projective second dimension Mandelkern calls bounds. Indefinites ɜx(p,q) carry a witness bound (if true, then g(x) must be a witness); definites ιx(p,q) carry a familiarity bound (the scope p is true and satt throughout the local context).

The headline payoff: classical logic is preserved at the truth-conditional layer (¬¬p ≡ p, ¬p ∨ q ≡ ¬p ∨ (p&q), De Morgan, etc.), so the system avoids dynamic semantics' logical problems around negation and disjunction (paper §4). Dynamic anaphoric coordination still happens, but entirely in the bound dimension via Schlenker/Karttunen-style local-context projection.

Architectural placement

Self-contained study file at the bounded theory's own level of generality. Deliberately disconnected from Charlow2025.LawfulDNELift per the session's design decision: the two formalisations should mature independently before any unifying typeclass is extracted. Per @cite{charlow-2025-staged-updates} §5 the two have higher-typed-bound vs. per-conjunct-bound differences that make a premature unification likely to be wrong.

Scope (paper §§5.1–5.7)

Formalised here:

• §5.1 — Truth and falsity (truth)
• §5.2 — Witness bound (in satt's .indef clause)
• §5.3 — Familiarity bound (in satt's .def_ clause)
• §5.4 — Update rule (update)
• §5.5 — Projection of bounds through connectives (in satt's recursion + the derived localCtx/negLocalCtx helpers)
• §5.6 — Bound-entailment, bound-equivalence (boundEntails, boundEquiv, preorder lemmas; the headline three-way bound-equivalence proved in the paper-faithful atomic specialization section56_a_bound_equiv_b_atomic and section56_b_bound_equiv_c_atomic, where F, G, H are atoms .atom Fa [x] etc. Generalisation to abstract F G H : BoundedForm Atom awaits a referencesVar-style well-formedness predicate; the paper's examples on p. 1108 are all atomic, so the atomic version covers the intended use case.)
• §5.7 — Classicality at the truth-conditional layer (4 theorems, all proved)

§5.8 (quantifiers EVERYx_δ with assignment-pair domains, MOSTx_δ) and §6 (modal subordination, cross-world witness bounds) are out of scope.

Connection to existing linglib infrastructure

• Core.Assignment.PartialAssign D := Nat → Option D — used here, matching @cite{spector-2025} which formalises a different (trivalent-Transparency) competitor to Mandelkern's bounded theory. Both files share the partial-assignment substrate but diverge in their treatment of bounds vs. presupposition.
• BoundedForm is a fresh inductive language type for this file (no shared surface-language type yet exists across linglib's dynamic theories).
• The classical-logic theorems use Lean's Classical.em / not_not / not_and_or directly — Mandelkern's truth-conditions are propositional and bivalent (paper footnote 11), so classical meta-logic suffices.

@[reducible, inline]

abbrev Studies.Anaphora.Mandelkern2022.Index (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

A bounded-theory index: a partial assignment + a world. Paper's ⟨g, w⟩.

Equations

• Studies.Anaphora.Mandelkern2022.Index W E = (Core.PartialAssign E × W)

@[reducible, inline]

abbrev Studies.Anaphora.Mandelkern2022.Context (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

A context is a set of indices. Paper's c. Updates eliminate indices (Stalnakerian, paper §5.4) rather than extending assignments (Heimian).

Equations

• Studies.Anaphora.Mandelkern2022.Context W E = Set (Studies.Anaphora.Mandelkern2022.Index W E)

@[reducible, inline]

abbrev Studies.Anaphora.Mandelkern2022.AtomEval (Atom : Type u) (W E : Type v) : Type (max u v)

Atomic interpretation: each n-ary atom A has a Boolean extension at each world. Modeled here as A → List E → W → Bool with the convention that arity-mismatched calls return false.

Equations

• Studies.Anaphora.Mandelkern2022.AtomEval Atom W E = (Atom → List E → W → Bool)

def Studies.Anaphora.Mandelkern2022.resolveVars {E : Type v} (g : Core.PartialAssign E) : List ℕ → Option (List E)

Resolve a list of variable indices against a partial assignment. Returns some es if every variable is defined, none otherwise.

Direct match-based definition (rather than List.mapM) so that it reduces via Lean's match reduction. The List.mapM form goes through List.mapM.loop internally, which is opaque to simp/rfl and prevents clean reasoning about the singleton case resolveVars g [x].

Equations

• One or more equations did not get rendered due to their size.
• Studies.Anaphora.Mandelkern2022.resolveVars g [] = some []

@[simp]

theorem Studies.Anaphora.Mandelkern2022.resolveVars_nil {E : Type v} (g : Core.PartialAssign E) : resolveVars g [] = some []

inductive Studies.Anaphora.Mandelkern2022.BoundedForm (Atom : Type u) : Type u

Mandelkern's two-place definite/indefinite language (paper §5.1, p. 1101): ℒ_M ::= A(x₁,...,xₙ) | ⊤(xs) | p&q | p∨q | ¬p | ɜx(p,q) | ιx(p,q).

top carries a list of bound variables: ⊤(xs) is satt and true iff all xs are defined. Mandelkern uses ⊤_x (paper §5.6 (20-c)) as a tautological restrictor; making it primitive lets us encode ιx(⊤, p) directly.

• atom {Atom : Type u} : Atom → List ℕ → BoundedForm Atom

  A(x₁,...,xₙ). Truth requires every xᵢ defined and the resolved tuple in I(A,w).

• top {Atom : Type u} : List ℕ → BoundedForm Atom

  ⊤(xs) — true (whenever defined) and used as a trivial restrictor.

• conj {Atom : Type u} : BoundedForm Atom → BoundedForm Atom → BoundedForm Atom

  Classical conjunction p & q.

• disj {Atom : Type u} : BoundedForm Atom → BoundedForm Atom → BoundedForm Atom

  Classical disjunction p ∨ q.

• neg {Atom : Type u} : BoundedForm Atom → BoundedForm Atom

  Classical negation ¬p.

• indef {Atom : Type u} : ℕ → BoundedForm Atom → BoundedForm Atom → BoundedForm Atom

  Two-place indefinite ɜx(p, q) — "some p is q".

• def_ {Atom : Type u} : ℕ → BoundedForm Atom → BoundedForm Atom → BoundedForm Atom

  Two-place definite ιx(p, q) — "the p is q".

@[implicit_reducible]

instance Studies.Anaphora.Mandelkern2022.instReprBoundedForm {Atom✝ : Type u_1} [Repr Atom✝] : Repr (BoundedForm Atom✝)

Equations

• Studies.Anaphora.Mandelkern2022.instReprBoundedForm = { reprPrec := Studies.Anaphora.Mandelkern2022.instReprBoundedForm.repr }

def Studies.Anaphora.Mandelkern2022.instReprBoundedForm.repr {Atom✝ : Type u_1} [Repr Atom✝] : BoundedForm Atom✝ → ℕ → Std.Format

Equations

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

def Studies.Anaphora.Mandelkern2022.truth {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) : BoundedForm Atom → Core.PartialAssign E → W → Prop

Truth at an index (paper §5.1, p. 1101 + appendix p. 1114). Pure classical: connectives are Boolean, indefinites are existential quantifiers, definites have the truth-conditions of their conjunction. The bounds dimension is satt below; truth is bound-insensitive.

Equations

• One or more equations did not get rendered due to their size.
• Studies.Anaphora.Mandelkern2022.truth av (Studies.Anaphora.Mandelkern2022.BoundedForm.top xs) x✝¹ x✝ = ∃ (es : List E), Studies.Anaphora.Mandelkern2022.resolveVars x✝¹ xs = some es
• Studies.Anaphora.Mandelkern2022.truth av (p.conj q) x✝¹ x✝ = (Studies.Anaphora.Mandelkern2022.truth av p x✝¹ x✝ ∧ Studies.Anaphora.Mandelkern2022.truth av q x✝¹ x✝)
• Studies.Anaphora.Mandelkern2022.truth av (p.disj q) x✝¹ x✝ = (Studies.Anaphora.Mandelkern2022.truth av p x✝¹ x✝ ∨ Studies.Anaphora.Mandelkern2022.truth av q x✝¹ x✝)
• Studies.Anaphora.Mandelkern2022.truth av p.neg x✝¹ x✝ = ¬Studies.Anaphora.Mandelkern2022.truth av p x✝¹ x✝

@[irreducible]

def Studies.Anaphora.Mandelkern2022.satt {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) : BoundedForm Atom → Context W E → Core.PartialAssign E → W → Prop

Satt at a context+index (paper appendix p. 1114). Recursively defines bound-satisfaction via Schlenker-style local contexts. Each recursion happens on a strict subterm of the input form (the .indef and .def_ cases inline the p&q formula rather than constructing .conj p q so termination is structural).

The key clauses:

• .conj p q: right conjunct sees c^p (paper p. 1105).
• .disj p q: right disjunct sees c^¬p (paper p. 1105).
• .neg p: bound projects identically (paper p. 1105).
• .indef x p q: existential satt + witness bound (paper §5.2 + p. 1106).
• .def_ x p q: familiarity bound + scope projection through c^p (paper §5.3 + p. 1107).

Equations

• One or more equations did not get rendered due to their size.
• Studies.Anaphora.Mandelkern2022.satt av (Studies.Anaphora.Mandelkern2022.BoundedForm.atom a xs) x✝² x✝¹ x✝ = ∃ (es : List E), Studies.Anaphora.Mandelkern2022.resolveVars x✝¹ xs = some es
• Studies.Anaphora.Mandelkern2022.satt av (Studies.Anaphora.Mandelkern2022.BoundedForm.top xs) x✝² x✝¹ x✝ = ∃ (es : List E), Studies.Anaphora.Mandelkern2022.resolveVars x✝¹ xs = some es
• Studies.Anaphora.Mandelkern2022.satt av p.neg x✝² x✝¹ x✝ = Studies.Anaphora.Mandelkern2022.satt av p x✝² x✝¹ x✝

def Studies.Anaphora.Mandelkern2022.localCtx {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (c : Context W E) (p : BoundedForm Atom) : Context W E

Local context for the right-conjunct (paper p. 1105): c^p keeps the indices in c where p is true and satt relative to c.

Equations

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

def Studies.Anaphora.Mandelkern2022.negLocalCtx {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (c : Context W E) (p : BoundedForm Atom) : Context W E

Negative local context for the right-disjunct (paper p. 1105): c^¬p keeps the indices in c where ¬p is true (i.e., p is false) AND ¬p is satt (which collapses to p is satt, by the .neg clause of satt).

The negation distributes only over truth p, not over the whole truth p ∧ satt p conjunction — paper p. 1105 defines c^X = {idx ∈ c | X is true and satt at ⟨c,idx⟩} applied to X := ¬p. The earlier draft had ¬(truth p ∧ satt p), which is strictly weaker (admits indices where p is unsatt regardless of truth) and breaks the bathroom theorem.

Equations

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

theorem Studies.Anaphora.Mandelkern2022.localCtx_indef_witness {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (c : Context W E) (x : ℕ) (F G : BoundedForm Atom) (idx : Index W E) (hidx : idx ∈ localCtx av c (BoundedForm.indef x F G)) : truth av F idx.fst idx.snd ∧ truth av G idx.fst idx.snd

Witness-bound projection through update (the key non-trivial fact about how ɜ's witness bound interacts with local-context computation): every index in c^{ɜx(F,G)} has g(x) itself satisfying both F and G.

Proof: an index ⟨g,w⟩ is in c^{ɜx(F,G)} iff (1) it is in c, (2) ɜx(F,G) is true at ⟨g,w⟩, and (3) ɜx(F,G) is satt at ⟨c,g,w⟩. Conditions (2) and (3) together trigger the witness bound (the second clause of satt's .indef case), which says: if any witness exists then g(x) is the witness, i.e., F(g) ∧ G(g) holds at ⟨g,w⟩.

def Studies.Anaphora.Mandelkern2022.update {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (c : Context W E) (p : BoundedForm Atom) : Context W E

Stalnakerian eliminative update (paper §5.4, p. 1103): updating c with p keeps exactly the points where p is true and satt. Differs from Heimian update which extends assignments; bounds-style update only eliminates.

Equations

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

theorem Studies.Anaphora.Mandelkern2022.update_subset {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (c : Context W E) (p : BoundedForm Atom) : update av c p ⊆ c

Update is eliminative: c[p] ⊆ c. Stalnakerian update never adds new indices; it only filters.

theorem Studies.Anaphora.Mandelkern2022.update_eq_localCtx {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (c : Context W E) (p : BoundedForm Atom) : update av c p = localCtx av c p

Update equals localCtx: the update of c by p is the local context c^p. They are definitionally equal, but stated as a theorem for discoverability.

def Studies.Anaphora.Mandelkern2022.boundEntails {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (p q : BoundedForm Atom) : Prop

Bound entailment (paper p. 1108): p ⊨_B q iff for any context+index where both p and q are satt and p is true, q is also true. Generalises @cite{von-fintel-1999}'s Strawson entailment from presuppositions to bounds.

Equations

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

def Studies.Anaphora.Mandelkern2022.boundEquiv {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (p q : BoundedForm Atom) : Prop

Bound equivalence (paper p. 1108): bound-entailment in both directions.

Equations

• Studies.Anaphora.Mandelkern2022.boundEquiv av p q = (Studies.Anaphora.Mandelkern2022.boundEntails av p q ∧ Studies.Anaphora.Mandelkern2022.boundEntails av q p)

theorem Studies.Anaphora.Mandelkern2022.boundEntails.refl {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (p : BoundedForm Atom) : boundEntails av p p

Bound entailment is reflexive.

theorem Studies.Anaphora.Mandelkern2022.boundEntails.trans_with_satt {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) {p q r : BoundedForm Atom} (hpq : boundEntails av p q) (hqr : boundEntails av q r) (hsatt_q : ∀ (c : Context W E) (g : Core.PartialAssign E) (w : W), satt av p c g w → satt av r c g w → truth av p g w → satt av q c g w) : boundEntails av p r

Bound entailment is conditionally transitive (paper p. 1108 implicitly).

Bound-entailment is not transitive in the unconditional sense: from p ⊨_B q and q ⊨_B r alone, we cannot derive p ⊨_B r, because applying p ⊨_B q to a context where p is satt-and-true requires q to also be satt at that context (the antecedent of the implication inside boundEntails), which is not given.

The conditional version, given an explicit satt q witness, holds trivially. This is the right form for chaining bound-entailment arguments at concrete sites where context makes q's satt obvious.

theorem Studies.Anaphora.Mandelkern2022.boundEquiv.refl {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (p : BoundedForm Atom) : boundEquiv av p p

Bound equivalence is reflexive.

theorem Studies.Anaphora.Mandelkern2022.boundEquiv.symm {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) {p q : BoundedForm Atom} (h : boundEquiv av p q) : boundEquiv av q p

Bound equivalence is symmetric.

theorem Studies.Anaphora.Mandelkern2022.boundEntails_of_logicalEntails {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) {p q : BoundedForm Atom} (h : ∀ (g : Core.PartialAssign E) (w : W), truth av p g w → truth av q g w) : boundEntails av p q

Bounded logic is a superset of classical logic (paper §5.7 punchline, p. 1109): "if p ⊨_L q, then p ⊨_B q". Any classically-valid implication is also a bound-entailment. The converse fails — bound-entailment also captures pragmatic Strawson-style equivalences that classical logic misses (e.g., the §5.6 (20) three-way bound-equivalence).

Direct from definitions: the truth-conditional dimension is classical, so classical entailment immediately satisfies the bounded version (which trivially ignores the satt antecedents).

theorem Studies.Anaphora.Mandelkern2022.dne_truth {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (g : Core.PartialAssign E) (w : W) (p : BoundedForm Atom) : truth av p.neg.neg g w ↔ truth av p g w

Double negation elimination at truth (paper §5.7): ¬¬p ≡ p classically. The bounded system preserves this; dynamic semantics fails it (paper §4 (11)).

theorem Studies.Anaphora.Mandelkern2022.disj_neg_eq_disj_neg_conj_truth {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (g : Core.PartialAssign E) (w : W) (p q : BoundedForm Atom) : truth av (p.neg.disj q) g w ↔ truth av (p.neg.disj (p.conj q)) g w

Disjunction-conjunction equivalence at truth (paper §5.7): ¬p ∨ q ≡ ¬p ∨ (p&q). Bounded preserves this; dynamic semantics fails it (paper §4 (14) / Partee disjunctions).

theorem Studies.Anaphora.Mandelkern2022.demorgan_neg_conj_truth {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (g : Core.PartialAssign E) (w : W) (p q : BoundedForm Atom) : truth av (p.conj q).neg g w ↔ truth av (p.neg.disj q.neg) g w

De Morgan at truth: ¬(p&q) ≡ ¬p ∨ ¬q. Holds classically; dynamic semantics doesn't validate this in general.

theorem Studies.Anaphora.Mandelkern2022.excluded_middle_truth {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (g : Core.PartialAssign E) (w : W) (p : BoundedForm Atom) : truth av (p.disj p.neg) g w

Excluded middle at truth: p ∨ ¬p is true at every index.

theorem Studies.Anaphora.Mandelkern2022.dneg_indef_truth_eq_indef {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (g : Core.PartialAssign E) (w : W) (x : ℕ) (p q : BoundedForm Atom) : truth av (BoundedForm.indef x p q).neg.neg g w ↔ truth av (BoundedForm.indef x p q) g w

Doubly-negated indefinite has same truth-conditions as the indefinite (paper §5.7, p. 1109): ¬¬ɜx(p,q) ≡ ɜx(p,q) classically. This is what licenses Karttunen's (1976) observation (paper §4 (12-a)) that doubly-negated indefinites antecede subsequent definites — the truth-conditional content survives DNE so the witness bound projects up. Trivial corollary of dne_truth.

theorem Studies.Anaphora.Mandelkern2022.neg_indef_truth_iff_forall_neg {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (g : Core.PartialAssign E) (w : W) (x : ℕ) (p q : BoundedForm Atom) : truth av (BoundedForm.indef x p q).neg g w ↔ ¬∃ (a : E), truth av p (g.update x a) w ∧ truth av q (g.update x a) w

Negated indefinite has the universal-negation truth-condition (paper §4): ¬ɜx(p,q) ≡ ∀x.¬(p&q). Direct from the definition of truth on .neg and .indef.

theorem Studies.Anaphora.Mandelkern2022.dneg_indef_bound_equiv {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (x : ℕ) (p q : BoundedForm Atom) : boundEquiv av (BoundedForm.indef x p q).neg.neg (BoundedForm.indef x p q)

Doubly-negated indefinite is bound-equivalent to the indefinite (paper §4 (12-a) headline empirical payoff; paper §5.7).

Karttunen 1976's observation: ¬¬ɜx(child) licenses subsequent definites just as ɜx(child) does. The bounded theory captures this: the two formulas are bound-equivalent because (a) classical DNE on truth makes their truth-conditions identical, (b) the .neg clause of satt makes satt of ¬¬p and satt of p definitionally equal, so any context where both are satt is the same context.

Proof: by boundEntails_of_logicalEntails applied to dne_truth in both directions.

Paper §5.6 (20): three bound-equivalent formulations.

Mandelkern's central technical claim about open scope: the following three formulations have the same truth-up-to-bounds content, even though they are not logically equivalent.

• (20-a) ɜx(F, G & H) — "Some F is G and H"
• (20-b) ɜx(F, G) & ιx(F, H) — "Some F is G, and the F is H"
• (20-c) ɜx(F, G) & ιx(⊤_x, H) — "Some F is G, and it is H"

Bound-equivalence (not full logical equivalence) captures the pragmatic equivalence the open-scope thesis demands while preserving classical logic.

def Studies.Anaphora.Mandelkern2022.section56_a {Atom : Type u} (x : ℕ) (F G H : BoundedForm Atom) : BoundedForm Atom

(20-a) ɜx(F, G & H).

Equations

• Studies.Anaphora.Mandelkern2022.section56_a x F G H = Studies.Anaphora.Mandelkern2022.BoundedForm.indef x F (G.conj H)

def Studies.Anaphora.Mandelkern2022.section56_b {Atom : Type u} (x : ℕ) (F G H : BoundedForm Atom) : BoundedForm Atom

(20-b) ɜx(F, G) & ιx(F, H).

Equations

• Studies.Anaphora.Mandelkern2022.section56_b x F G H = (Studies.Anaphora.Mandelkern2022.BoundedForm.indef x F G).conj (Studies.Anaphora.Mandelkern2022.BoundedForm.def_ x F H)

def Studies.Anaphora.Mandelkern2022.section56_c {Atom : Type u} (x : ℕ) (F G H : BoundedForm Atom) : BoundedForm Atom

(20-c) ɜx(F, G) & ιx(⊤_[x], H).

Equations

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

theorem Studies.Anaphora.Mandelkern2022.section56_a_boundEntails_b {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (x : ℕ) (F G H : BoundedForm Atom) : boundEntails av (section56_a x F G H) (section56_b x F G H)

(20-a) bound-entails (20-b) (paper p. 1108, easy direction).

Given (20-a) is satt, (20-b) is satt, and (20-a) is true: derive (20-b) is true. The proof:

1. truth of (20-a) = ɜx(F, G&H) gives a witness a for F ∧ G ∧ H at g[x→a].
2. The witness bound on satt of (20-a) (applied to that witness) forces g(x) itself to satisfy F ∧ G ∧ H at g.
3. Truth of (20-b) at g is (∃a, F(g[x→a]) ∧ G(g[x→a])) ∧ (F(g) ∧ H(g)). First conjunct: project from step 1 (drop H). Second conjunct: from step 2.

This direction works abstractly because we only need to project the truth of (20-b) from already-established facts.

Paper-faithful atomic specializations of §5.6 (b)↔(a) and (b)↔(c).

The general abstract bound-equivalences (b)↔(a) and (b)↔(c) require either a referencesVar-style predicate that F, G, H are free in x (paper p. 1101 well-formedness condition) plus the PartialAssign.update_self lemma. The paper's §5.6 examples (20)-(20-c) — child(x), Susie's(x), at-boarding-school(x) — are all atomic predicates Fx, Gx, Hx. We prove the bound-equivalences in this paper-faithful atomic specialization.

Generalization to arbitrary well-formed F, G, H is queued for the next session: it requires structural induction on a referencesVar predicate plus the partial-assignment update_self plus a truth-invariance lemma for non-referenced variable updates.

theorem Studies.Anaphora.Mandelkern2022.resolveVars_singleton_def {E : Type v} {g : Core.PartialAssign E} {x : ℕ} {es : List E} (h : resolveVars g [x] = some es) : ∃ (a : E), g x = some a

resolveVars [x] extracts g(x) defined: if resolveVars g [x] = some es for any es, then g x = some a for some a. The base technical lemma that lets atomic-truth-of-Fx imply g(x) defined.

Proof via by_contra + push_neg to avoid cases hgx : g x-style substitution which Lean does eagerly, breaking the goal structure.

theorem Studies.Anaphora.Mandelkern2022.resolveVars_singleton_some {E : Type v} {g : Core.PartialAssign E} {x : ℕ} {a : E} (h : g x = some a) : resolveVars g [x] = some [a]

resolveVars [x] for defined g(x) computes some [a].

theorem Studies.Anaphora.Mandelkern2022.section56_b_boundEntails_a_atomic {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (x : ℕ) (Fa Ga Ha : Atom) : boundEntails av (section56_b x (BoundedForm.atom Fa [x]) (BoundedForm.atom Ga [x]) (BoundedForm.atom Ha [x])) (section56_a x (BoundedForm.atom Fa [x]) (BoundedForm.atom Ga [x]) (BoundedForm.atom Ha [x]))

(20-b) bound-entails (20-a) — direction-2 of §5.6 (a)↔(b), atomic version for F, G, H of shape .atom _ [x].

Proof: from truth (ɜx(Fx,Gx) ∧ ι(Fx,Hx)) we extract a witness a for Fx ∧ Gx at g[x→a] and the truth Fx(g) ∧ Hx(g). Apply the witness bound on satt of ɜx(Fx,Gx) to derive Gx(g). Then Fx(g) forces g(x) defined (atomic truth requires resolveVars to succeed). Take b := g(x).get; by PartialAssign.update_self, g.update x b = g, so the truth conditions transfer to give Fx(g[x→b]) ∧ Gx(g[x→b]) ∧ Hx(g[x→b]).

The general abstract version (with referencesVar-style hypotheses) is queued; this paper-faithful atomic version covers the §5.6 (20) example.

theorem Studies.Anaphora.Mandelkern2022.section56_a_bound_equiv_b_atomic {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (x : ℕ) (Fa Ga Ha : Atom) : boundEquiv av (section56_a x (BoundedForm.atom Fa [x]) (BoundedForm.atom Ga [x]) (BoundedForm.atom Ha [x])) (section56_b x (BoundedForm.atom Fa [x]) (BoundedForm.atom Ga [x]) (BoundedForm.atom Ha [x]))

Bound-equivalence of (20-a) and (20-b) (paper p. 1108), atomic version. Direction (a)→(b) is the general (proved abstractly) lemma; direction (b)→(a) requires the atomic specialization.

theorem Studies.Anaphora.Mandelkern2022.section56_b_bound_equiv_c_atomic {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (x : ℕ) (Fa Ga Ha : Atom) : boundEquiv av (section56_b x (BoundedForm.atom Fa [x]) (BoundedForm.atom Ga [x]) (BoundedForm.atom Ha [x])) (section56_c x (BoundedForm.atom Fa [x]) (BoundedForm.atom Ga [x]) (BoundedForm.atom Ha [x]))

Bound-equivalence of (20-b) and (20-c) (paper p. 1108), atomic version. The forward direction needs Fx(g) → g(x) defined (atomic); the backward direction uses the ɜx(Fx,Gx) witness bound for Fx(g).

Paper §4 data, formalised at the satt-update level.

These empirical claims (Karttunen 1976, Partee disjunctions, bathroom sentences) are the data dynamic semantics struggles with and the bounded theory accommodates. Formalising them requires both truth-level classicality (proved above) and satt-level reasoning about projection (localCtx, negLocalCtx).

The truth-level claims are direct corollaries of §7. The satt-level claims are stated below; full proofs depend on the localCtx_indef_witness lemma (deferred) and are left as TODO for the same follow-up PR.

theorem Studies.Anaphora.Mandelkern2022.negated_indefinite_universal {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (g : Core.PartialAssign E) (w : W) (x : ℕ) (p q : BoundedForm Atom) : truth av (BoundedForm.indef x p q).neg g w ↔ ∀ (a : E), ¬(truth av p (g.update x a) w ∧ truth av q (g.update x a) w)

Negated-indefinite truth has universal-negation form (paper §4 (11) truth-conditional content). Direct corollary of neg_indef_truth_iff_forall_neg.

theorem Studies.Anaphora.Mandelkern2022.bathroom_truth {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (g : Core.PartialAssign E) (w : W) (x : ℕ) (B H : BoundedForm Atom) : truth av ((BoundedForm.indef x B (BoundedForm.top [x])).neg.disj H) g w ↔ (¬∃ (a : E), truth av B (g.update x a) w ∧ truth av (BoundedForm.top [x]) (g.update x a) w) ∨ truth av H g w

Bathroom truth (paper §4 (14-a) truth-conditional content): ¬ɜx(B(x)) ∨ H(x) is true iff either there is no B-thing or H(g(x)). Holds classically without difficulty.

theorem Studies.Anaphora.Mandelkern2022.bathroom_right_disjunct_local_ctx_witness {Atom : Type u} {W E : Type v} (av : AtomEval Atom W E) (c : Context W E) (x : ℕ) (B : BoundedForm Atom) (idx : Index W E) (hin : idx ∈ c) (htruth : truth av (BoundedForm.indef x B (BoundedForm.top [x])) idx.fst idx.snd) (hsatt : satt av (BoundedForm.indef x B (BoundedForm.top [x])) c idx.fst idx.snd) : truth av B idx.fst idx.snd

Bathroom-disjunction licensing (paper §5.7, p. 1109; data §4 (14-a)).

Under the bounded theory, ¬ɜxB(x) ∨ ψ(x) makes x available in the right disjunct's local context. The right disjunct sees c^¬(¬ɜxB(x)) — by negLocalCtx's definition (after the audit-driven fix) this is indices where ¬¬ɜxB(x) is true (= ɜxB(x) by classical DNE) AND ¬ɜxB(x) is satt (= ɜxB(x) is satt, by the .neg clause of satt, which collapses definitionally though Lean's recursive def doesn't auto-reduce in hypothesis positions).

The "stripped" theorem statement below decouples from the .neg .neg projection plumbing: any index in c that is true and satt for the positive existential ɜxB(⊤_x) has B(g) true. Composing this with Classical.not_not and the .neg-satt-collapse equation rfl gives the full bathroom theorem (chain of three rewrites the consumer can do at their use site).

Note on satt-of-.neg coercion: the paper's projection rule (paper p. 1105 "a negation is satt iff the negatum is satt") makes satt (¬p) = satt p intentionally definitional. In our Lean formalisation, however, satt's termination_by annotation forces well-founded recursion via WellFounded.fix, which Lean treats as opaque to definitional reduction. So the equation satt av (.neg p) c g w = satt av p c g w is not a Lean definitional equality and not provable by rfl / Iff.refl / change.

To use bathroom_right_disjunct_local_ctx_witness on a hypothesis hsatt : satt av (.neg p) c g w, consumers need to manually establish the coercion at use sites (typically by computing satt's body explicitly or proving the Iff via case analysis on p's structure). A future mathlib-quality refactor would make satt non-termination_by (structural recursion) and reclaim the definitional collapse.

inductive Studies.Anaphora.Mandelkern2022.TestAtom : Type

A trivial atom set with one one-place predicate.

• child : TestAtom

@[reducible, inline]

abbrev Studies.Anaphora.Mandelkern2022.TestWorld : Type

Equations

• Studies.Anaphora.Mandelkern2022.TestWorld = Bool

@[reducible, inline]

abbrev Studies.Anaphora.Mandelkern2022.TestE : Type

Equations

• Studies.Anaphora.Mandelkern2022.TestE = Bool

def Studies.Anaphora.Mandelkern2022.testAv : AtomEval TestAtom TestWorld TestE

Test atom evaluation: child(b) is true at world true if b = false.

Equations

• Studies.Anaphora.Mandelkern2022.testAv Studies.Anaphora.Mandelkern2022.TestAtom.child [b] x✝ = decide (x✝ = true ∧ b = false)
• Studies.Anaphora.Mandelkern2022.testAv x✝² x✝¹ x✝ = false