# 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` (no `sorry`).

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