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).