← Local Contexts (appendix) · raw TODO.md
TODO: definitions and results of the Appendix of "Local Contexts" (Schlenker)
Source: source/Local-Contexts-08.02.08-Appendix.pdf (14 pp., numbered pp. 39-52). Item numbers below are the appendix's own numbering (1-41). Page numbers are the running page numbers printed in the appendix (p. 39 = first page of the appendix). Status legend: done = formalised and checked in Lean; done-corrected = paper's statement/proof needed a fix, corrected version proven; cex = paper's non-equivalence claim, countermodel checked in Lean; partial = only a fragment/special case formalised; no = not formalised (reason given). Everything "done" is in lean/ and checked by sh lean/check.sh.
A. Definitions
| # | Item | Page | Content | Status |
|---|---|---|---|---|
| D1 | 1 | 39 | Syntax of L: Q, P, p, F ::= p, (not F), (F and F), (F or F), (if F. F), (Qi P . P); enrichments (predicate conjunction, context variables c') | partial: propositional fragment only (PropSyntax.lean); quantifier clause only in the (No P . QQ') example |
| D2 | 2 | 39-40 | Classical semantics I (w |= F), tree-of-numbers quantifiers | partial: propositional (ev), (No P . QQ') (quant) |
| D3 | 3 | 40 | Expressivity: every proposition/property denoted by an atom | done as hypothesis Expressive I (propositional part); properties: Val ranges over all functions |
| D4 | 4 | 40 | Generalized entailment x <= x' | done (LC.le, LC.cle for the C-relative version) |
| D5 | 5 | 40 | Generalized conjunction | done (LC.meet); NB typo in 5b |
| D6 | 6 | 40 | Dynamic semantics (Heim; Beaver for or) | partial: propositional (dyn), (No P . QQ') (dynDefined) |
| D7 | 7 | 40 | Transparency: Be Articulate, Be Brief (incremental / symmetric), ordering | done in the derived form 8 |
| D8 | 8 | 40 | Transp_i(C,F), Transp_s(C,F) | done for propositional F (TranspI, TranspS); (No P . QQ') (transNo) |
| D9 | 9a,b | 40-41 | Non-Triviality, Constancy | no (only needed for Theorem 2 / 22, not formalised) |
| D10 | 10 | 41 | Transparent restrictions tr_i, tr_s | done abstractly (LC.Tr, LC.Env) and instantiated (EnvI, EnvS) |
| D11 | 11 | 41 | Local contexts lc_i, lc_s = bottom of tr | done (LC.IsLC) |
| D12 | 17 | 42 | Sat_v (local contexts exist) | done (LC.SatLC, SatI, SatS) |
| D13 | 18 | 42 | Sat'_v (general case) | done (LC.SatP, SatI', SatS') |
| D14 | 24 | 44 | Extensions Ext(I) (i < i') | done (AdmK, propositional; predicative for (No P . QQ'): AdmP) |
| D15 | 25 | 44 | Super-true / false / indeterminate | done (Super, super_eq_some_iff) |
| D16 | 26 | 44-45 | Super-acceptability, incremental / symmetric | done (SuperAccI, SuperAccS) |
| D17 | 27 | 45 | [s]#, L**, I** | done (numF, tokS); global numbering (equivalent) |
| D18 | 28 | 45 | Strong Kleene from supervaluations | done (Kleene) |
| D19 | 29 | 45 | Kleene-acceptability | done (KleeneAccI, KleeneAccS) |
| D20 | 33 | 46 | n-indexed acceptability / Ext(F,n) | no (auxiliary machinery for the paper's proofs of 36/38; our proofs go a different way) |
| D21 | 40 | 49 | Standard Strong Kleene (propositional) | done (sk, skop, derived clauses skop_or_def, skop_imp_def) |
B. Results
| # | Item | Page | Claim | Status |
|---|---|---|---|---|
| R1 | 9c Thm 1 | 41 | propositional fragment: Transp_i(C,F) iff C[F] != #; C[F] = {w in C: w |= F} | done (PropTheory.lean theorem1) |
| R2 | 9d Thm 2 | 41 | quantificational, under Non-Triviality + Constancy: same | no (imported from Schlenker 2007a); special case (No P . QQ'), one world, finite domain: done (transNo_iff) |
| R3 | 12 Lemma 1 | 41 | local contexts exist in the propositional fragment | done-corrected: paper's LC^i is not the bottom element (lemma1_paper_candidate_fails); corrected lemma1 |
| R4 | 13 Lemma 2 | 41-42 | tr closed under finite conjunction | done (LC.lemma2, both versions) |
| R5 | 14 Lemma 3 | 42 | finite tr implies lc exists | done (LC.lemma3; needs tr nonempty, i.e. top in tr, unmentioned) |
| R6 | 15 Lemma 4 | 42 | point-wise construction of local contexts | done (LC.lemma4) |
| R7 | 16 Existence Thm | 42 | (a) propositional fragment, (b) finite domains: local contexts exist | (a) done (lc_exists_prop_i/s); (b) partial: abstract form LC.existence (finite D -> Bool), full L not formalised |
| R8 | 19 Lemma 5 | 42-43 | if lc exists, Sat_v iff Sat'_v | done (LC.lemma5, lemma5_prop_i) |
| R9 | 20 a,b,c | 43 | tr_i in tr_s; lc_s <= lc_i; Sat_i implies Sat_s | done (LC.thm20a, LC.thm20bc, thm20_prop) |
| R10 | 21 Thm | 43 | Sat'_v(C, dd', a_b) iff Transp_v; (ii) for formulas | done abstractly (LC.thm21) and for the propositional fragment (thm21_prop_i/s) |
| R11 | 22 Thm | 43 | under NT + Constancy: local contexts exist and Sat_i iff Sat'_i iff C[F] != # | partial: propositional fragment, no side conditions (thm22_prop); general L relies on Theorem 2, not formalised |
| R12 | 23a | 44 | QQ' in (Infinitely-many P . QQ') has no local context in {w} | done (InfinitelyMany.lean example23a) |
| R13 | 23b | 44 | Sat'_i / Transp_i does not entail C |= (Every P . Q) | done (example23b); overclaim in the sentence introducing 23 (see RESULTS) |
| R14 | 30 Lemma 6 | 45 | if each trigger occurs once, Super = Kleene | done for the propositional fragment (lemma6) |
| R15 | 31 Lemma 7 | 45-46 | Kleene != # implies Super = Kleene | done (propositional; lemma7) |
| R16 | 32 Lemma 8 | 46 | Kleene-acc_v implies Super-acc_v and Kleene = Super on C | done (propositional; lemma8_*, kleeneAccI_S) |
| R17 | 34 Lemma 9 a,b | 46 | n-indexed characterisation of Kleene-acc | no (auxiliary, see D20) |
| R18 | 35 Lemma 10 a,b | 46-47 | restriction of acceptability to prefixes | no (auxiliary) |
| R19 | 36 Thm | 47 | (a) Kleene-acc_i iff Super-acc_i; (b) values agree | done for the propositional fragment (theorem36), plus the stronger prop_fragment_collapse |
| R20 | 37 Lemma 11 | 47 | Kleene-acc_s implies Super-acc_s; converse fails: (pp' or (not pp')) | done (lemma8_s_super, lemma11_super, lemma11_not_kleene) |
| R21 | 38 Thm (a) | 47-48 | Transp_i implies Kleene-acc_i (hence Super-acc_i) | done for the propositional fragment (theorem38a); predicative triggers not formalised |
| R22 | 38 Thm (b) | 48 | converse fails: (No P . QQ'), 2 P-individuals, d1 not Q, d2 Q and Q' | cex (Quantifier.lean theorem38b_39b); NOT available in the propositional fragment (converse holds there, prop_fragment_collapse) |
| R23 | 39a | 48-49 | (pp' and qq'), C={w1,w2}: sym. Transp satisfied, sym. Kleene / Super not | cex (theorem39a) |
| R24 | 39b | 49 | (No P . QQ'): sym. Kleene satisfied, sym. Transp not | cex (theorem38b_39b) |
| R25 | 41 Thm | 49-50 | propositional: Standard-Kleene = Kleene | done (theorem41) |
Additional (not in the paper): prop_fragment_collapse; sanity checks (Sanity.lean).