# Anti-Dynamics (Schlenker 2007, JoLLI 16:325-356) — extraction checklist

Source: `source/Schlenker-Anti-Dynamics-P-copy.{pdf,txt}` (journal pages 325-356; the PDF was read
visually wherever the text extraction lost logical symbols: pp. 336-342, 348, 351-353).
Status legend: **P** proven in Lean as stated; **PC** proven after correction; **CE** counterexample
found (checked in Lean); **C** confirmed (paper's claim checked in Lean); **N** not formalized (reason).
All Lean names refer to `lean/AntiDynamics/*.lean`; line numbers are in `RESULTS.md`.

## A. Definitions

| # | Where | Content | Status |
|---|---|---|---|
| A1 | §1.2 p.326 | Stalnaker's (i)-(iii): `C[pp']=#` unless presupposition holds on `C`; update with assertion; `C[F and G]=C[F][G]` | N (historical background; (iii) is Heim's `and`, formalized in A6) |
| A2 | §1.3 (2) p.328 | deviant `and*`: `C[F and* G]=C[G][F]` | C: `andStarDef/Upd`, `andStar_eq_swap`, `andStar_agrees_trigfree`, `andStar_not_transparency`, `andStar_too_strong` |
| A3 | §2.1 (5) p.330 | Definition of Transparency (`α(d and γ)β ⇔ αγβ`) | formalized twice: contexts (`Sys.Transp`) and literal strings (`Sys.StrTransp`); equivalence PC/P `strTransp_iff_transp` |
| A4 | §2.1 (6) p.331 | Principle of Transparency (acceptability iff competitor ruled out) | same as A3 (the "iff" is the definition of `Transp`) |
| A5 | §3.1 (18) p.335 | Syntax: predicates, propositions, formulas, `Qi P . P`, meta-language | `Fm`, `PLeaf`, `QLeaf`, `Pred` (object language only; meta-language `∀d`, `⇒`, `⇔` are Lean's) |
| A6 | §3.2 (20)-(21) p.336 | Interpretation of lexical items; Heim/Beaver CCPs with definedness | `Sys.Upd`, `Sys.Def`, `QModel.qupd/qdef` |
| A7 | §3.2 (22) p.337 | Truth/falsity/presupposition failure at `w ∈ C` | N (only a definition; `Def` and `Upd` are used directly) |
| A8 | §3.2 (25) p.338 | Static bivalent semantics (`p̲p'` = conjunction; `if` = material implication; quantifier via `f(a,b)`) | `evalF`, `Sys.eval`, `QModel.qsem` |
| A9 | §3.2 (26) p.338 | Principle of Transparency, concise form; `Transp(C,F)` | = A3 |
| A10 | §5.1 (28) p.344 | Non-Triviality | `Sys.NT` |
| A11 | §5.3 p.348 | Definition of "accessed"/"parent" pairs | `Accessed` |
| A12 | §5, intro p.343 | Heim's claims: `(Q P̲P'. R)` presupposes `∀d P(d)`; `(Q P. R̲R')` presupposes `∀d[P(d)⇒R(d)]` | C: `heim_claim_i/ii`, `qdef_both` |

## B. Lemmas

| # | Where | Content | Status |
|---|---|---|---|
| B1 | §2.2 (8), §3.2 (23) p.332,337 | Dynamic Transparency `C[F]≠# ⇒ C[F]=C[F*]` | P: `dynamic_transparency` (propositional), `dynamic_transparency_quant` |
| B2 | §3.2 (24) p.337-8 | `or*` violates Dynamic Transparency (`H=((not p) or* p̲p')`) | C: `or_star_breaks_dynamic_transparency` |
| B3 | §3.1 (19a) p.335 | Syntactic Lemma (a) | P: `syntactic_lemma_a` (string level; proof in paper only sketched) |
| B4 | §3.1 (19b) p.335 | Syntactic Lemma (b) | P: `ser_append_inj` (= unique readability; the paper's hypothesis "starts with `(s`, `s` not a parenthesis" is unnecessary) |
| B5 | §4 (27a,b) p.339 | Transparency Lemma | P: `transparency_lemma_a/b` (via `transp_conj/cond`) |
| B6 | §5.1 (29) p.344-5 | Non-Triviality Corollary (i),(ii) | P: `nt_corollary_i/ii` |
| B7 | §5.2 Lemma 1(i) p.345-7 | `Transp(C,(Qi P̲P'.R)) iff C ⊨ ∀d P(d)` | PC: `lemma1_i` (proof of Case 2 has a gap: `paper_zoneB_step_fails`, repaired by `find_step`) |
| B8 | §5.2 Lemma 1(ii) p.347-8 | `Transp(C,(Qi P.R̲R')) iff C ⊨ ∀d[P(d)⇒R(d)]` | P: `lemma1_ii` |
| B9 | §5.2 Remark p.345 | (c) can be replaced by Non-Triviality | P: `quant_leaf` (uses B6) |
| B10 | §5.3 Lemma 2 p.348-50 | NT is inherited by accessed pairs | P: `lemma2` (paper tacitly uses `C[G]={w∈C:w⊨G}`; here `upd_eq_TS`) |
| B11 | §4 proof, cases (a)-(f) p.339-42 | Inductive steps of Theorem 1 | P: `transp_neg/conj/disj/cond`, `Sys.lift`; typo found in (e) |
| B12 | §5.3 Thm 2 proof (a)-(g) p.351-2 | Inductive steps of Theorem 2 (incl. case (g)) | P: `Sys.lift`, `quant_leaf`, `theorem2`; typo found in (f) |

## C. Theorems

| # | Where | Content | Status |
|---|---|---|---|
| C1 | §4 Theorem 1(i) p.338 | `Transp(C,F) iff C[F]≠#` (propositional) | P: `theorem1_i`, `theorem1_i_strings` |
| C2 | §4 Theorem 1(ii) p.339 | `C[F]≠# ⇒ C[F]={w∈C: w⊨F}` | P: `theorem1_ii` |
| C3 | §5.3 Theorem 2 p.350 | quantified case under (i) constant domain size, (ii) constant restrictor size, (iii) NT | **CE as stated** (`theorem2_needs_expressiveness`); PC: `theorem2` with the extra hypothesis `Expressive` |
| C4 | §5.3 Thm 2 (ii) | `C'[F']={w∈C':w⊨F'}` | P: part of `theorem2` (`Sys.upd_eq_TS`, unconditional) |

## D. Worked derivations / examples

| # | Where | Content | Status |
|---|---|---|---|
| D1 | §1.1 (1), §2.1 (3),(4),(7) | Moldavia, Pavarotti data | N (empirical data) |
| D2 | §2.2 (10) p.332 | naive `C ⊨ F ⇔ F*` cannot yield asymmetry | C: `naive_conj_symmetric`, `transp_conj_asymmetric` |
| D3 | §2.2 (11)-(12) p.332-3 | atomic case: naive = `C ⊨ p'⇒p`, too weak | C: `naive_atomic`, `naive_strictly_weaker` |
| D4 | §2.2 (13) p.333 | Transparency of atom iff `C ⊨ p` | C: `transp_atomic` |
| D5 | §2.3 (14) p.333 | `(p̲p' and q)` presupposes `p` | C: `ex14` |
| D6 | §2.3 (15) p.333 | `(p and q̲q')` presupposes `p⇒q` | C: `ex15` |
| D7 | §2.3 (16) p.334 | `(if p̲p'. q)` presupposes `p` | C: `ex16` |
| D8 | §2.3 (17) p.334 | `(if p. q̲q')` presupposes `p⇒q` | C: `ex17` |

## E. Quantifier discussion

| # | Where | Content | Status |
|---|---|---|---|
| E1 | §5.1 p.343 | scenario: 2 P-individuals, `Q = less than three`: Transp trivially holds | C: `less_than_three_scenario` |
| E2 | §5.1 p.343 | NT rules out (E1) when all worlds have < 3 P | C: `not_nt_of_lt3` |
| E3 | §5.1 p.343-4 | three-world scenario (sizes 2,4,4): NT holds, Transp holds, Heim fails; Constancy needed | C: `constancy_needed` |
| E4 | fn 12 p.344 | `Q = infinitely many`: if `P^w−R^w` finite, Transp holds | C: `transpInf_of_finite`; new converse `not_transpInf_of_infinite`, iff `transpInf_iff` |
| E5 | fn 16 p.355 | integers / lucky-not-to-be-13: `P−Q` a singleton so Transp holds | C: `footnote16` |
| E6 | §6.5 (34) p.354-5 | soccer example: Transp holds, Heim predicts failure | C: `soccer_example` |

## F. §6 Conclusion claims

| # | Where | Content | Status |
|---|---|---|---|
| F1 | §6.1 (32)a-d p.352 | four candidate CCPs for `unless` | C, with **typo in (32)d** (`unlessD_paper_is_wrong`); (32)b,c leave the update undefined (`unlessB_update_ill_defined`) |
| F2 | §6.1 (33) p.352-3 | predictions of (32)a-d for "Unless John didn't come, Mary will know he is here" | C: `unless_33`, `unless_rules_differ` |
| F3 | §6.1 p.353 | Transparency: `unless` ~ `if not` | C: `transp_unless_eq_if_not` (Transparency verdict = (32)a: `unless_33`, last clause) |
| F4 | §6.1 p.353 | "same syntax + same bivalent content ⇒ same projection" | true by construction of `Transp` (depends only on syntax and static semantics); instance F3 |
| F5 | §6.2 p.353 | global/local accommodation | N (informal proposal) |
| F6 | §6.3 p.354 | Transparency as meta-constraint on lexical CCPs | N (research suggestion; not a claim) |
| F7 | §6.4, 6.6 p.354-5 | linear order vs processing order; DRT rivals | N (open questions) |

## G. Verification tasks (hunt for errors)

* Statement of Theorem 1: hypotheses checked (needs `⊤`,`⊥` in the language; nothing else). **No error.**
* Each case of the proof of Theorem 1: checked; typos Q4(a),(b),(c) in RESULTS.md.
* Lemma 1 proofs step by step: gap in Case 2/Zone B (Q2), typo in Case 1 (Q3).
* Statement of Theorem 2: missing hypothesis (Q1); notational ambiguity (Q5); circular-looking use of `C[G]` (Q6).
* Quantifier equivalence "weaker than propositional": confirmed with explicit finite countermodels (E1, E3, E6, Q1).