# RESULTS: formal check of the Appendix of "Local Contexts" (Schlenker)

All Lean files are in `lean/`, are checked by `sh lean/check.sh` (Lean 4.34, core only, no Mathlib),
contain no `sorry`, and depend only on the standard axioms `propext`, `Classical.choice`,
`Quot.sound` (checked with `#print axioms`).  Item numbers are the appendix's (1-41);
page numbers are the printed ones (p. 39 = first appendix page).
File:line refer to the current files in `lean/` (line of the `theorem`/`def`).

Status legend: **proven** = paper's statement proven as formalised; **proven-corrected** = the paper's
proof or statement needed a repair, corrected version proven; **counterexample found** = paper's
non-equivalence claim confirmed by a Lean-checked countermodel; **not formalized** = see reason.

## 1. Results table

**Verdict** (does the paper's claim hold?): **confirmed** = holds as stated; **corrected-proof** = statement holds but the paper's proof was wrong or had a gap, repaired in Lean; **modified-statement** = statement as printed is false or ill-posed, a corrected statement is proven; **disconfirmed** = false with no repair; **n/a** = definition, new result of ours, or not formalized. The **Status** column records only the formalization status.


Notation: `I : Nat -> W -> Bool` interpretation of propositional letters, `C : W -> Prop` context set,
`F : Form` a formula of the propositional fragment; `dyn I F C = none` is `C[F] = #`;
`TranspI/TranspS` = incremental/symmetric Transparency; `LcCond` = "each trigger's presupposition holds at
every world of its incremental local context"; `KleeneAccI` etc. as in items 26/29.

| Result | Location | Informal statement | Lean formalization (as stated in Lean) | Lean file:line | Verdict | Status |
|---|---|---|---|---|---|---|
| Theorem 1 | 9c, p.41 | Propositional fragment: `Transp_i(C,F)` iff `C[F] != #`; and `C[F]` = `{w in C : w |= F}` | `theorem1 I C F : (TranspI I C F <-> dyn I F C != none) /\ (forall D, dyn I F C = some D -> forall w, D w <-> (C w /\ ev I F w = true))` | PropTheory.lean:315 | confirmed | proven |
| Theorem 2 | 9d, p.41 | Quantificational L, under Non-Triviality + Constancy: same as Thm 1 | none in general.  Special case `(No P . QQ')`, one world, `D = Fin n`: `transNo_iff : transNo P Q <-> dynDefined P Q` | Quantifier.lean:52 | n/a | not formalized (imported from Schlenker 2007a; general L, NT and Constancy not modelled); special case proven |
| Lemma 1 | 12, p.41 | In the propositional fragment `lc_i`, `lc_s` exist | `LC.lemma1 (hE : forall Psi, Envs Psi -> Ext Psi) C : IsLC Envs C (lc1 Envs C)` for `Val W Unit`, with `lc1` = paper's candidate **plus the condition `C w`**; instantiated as `lc_exists_prop_i/s` | LCAbstract.lean:145; PropTheory.lean:404,406 | corrected-proof | proven-corrected (see Error E1) |
| Lemma 1, paper's candidate | 12, p.41 | The candidate `LC^i` as written is the bottom of `tr` | `lemma1_paper_candidate_fails : exists Envs C, (forall Psi, Envs Psi -> Ext Psi) /\ Tr Envs C bot /\ not (le (lc1Paper Envs) bot)` | LCAbstract.lean:152 | corrected-proof | counterexample found (candidate is wrong) |
| Lemma 2 | 13, p.41-42 | `tr_i`, `tr_s` closed under finite conjunction | `LC.lemma2 : Tr Envs C x -> Tr Envs C y -> Tr Envs C (meet x y)` (any set of environments, so both versions; any `D`) | LCAbstract.lean:63 | confirmed | proven |
| Lemma 3 | 14, p.42 | If `tr_v` is finite, `lc_v != #` | `LC.lemma3 (hfin : exists L, forall x, Tr Envs C x -> x in L) : exists x, IsLC Envs C x` (uses `top in tr`, unstated in paper) | LCAbstract.lean:92 | modified-statement | proven |
| Lemma 4 | 15, p.42 | If `lc_v({w}, ..)` exists for all `w in C`, `lc_v(C, ..)` exists (pointwise construction; extensionality) | `LC.lemma4` (hyp.: for each `w in C` a local bottom `s : D -> Bool` of `tr({w})`) | LCAbstract.lean:167 | confirmed | proven |
| Existence thm | 16a, p.42 | Propositional fragment: local contexts exist | `lc_exists_prop_i/s (I K C) : exists x, IsLC (EnvI/EnvS I K) C x` | PropTheory.lean:404,406 | corrected-proof | proven (via corrected Lemma 1) |
| Existence thm | 16b, p.42 | Finite domains: local contexts exist | `LC.existence (hE) (hD : exists L, forall s : D -> Bool, s in L) C : exists x, IsLC Envs C x` (abstract environments over any `W`, finite `D -> Bool`) | LCAbstract.lean:202 | modified-statement | proven for the abstract framework; not formalized for the full language L (no syntax of quantifiers) |
| Lemma 5 | 19, p.42-43 | If `lc_v` exists: `Sat_v` iff `Sat'_v` | `LC.lemma5 (hx : IsLC Envs C x) d : SatLC x d <-> SatP Envs C d`; prop. fragment: `lemma5_prop_i : SatI I C F <-> SatI' I C F` | LCAbstract.lean:258; PropTheory.lean:427 | corrected-proof | proven |
| Theorem 20 a-c | 20, p.43 | `tr_i` subset `tr_s`; `lc_s <= lc_i`; `Sat_i` implies `Sat_s` | `LC.thm20a`, `LC.thm20bc`; prop.: `thm20_prop : SatI I C F -> SatS I C F`; also `transpI_transpS` | LCAbstract.lean:270,275; PropTheory.lean:445,84 | confirmed | proven |
| Theorem 21 | 21, p.43 | `Sat'_v(C,dd',a_b)` iff `Transp_v(C,dd',a_b)`; hence for formulas | `LC.thm21 (hE) d : SatP Envs C d <-> Tr Envs C d`; prop.: `thm21_prop_i/s : SatI' I C F <-> TranspI I C F` (given `Expressive I`), likewise symmetric | LCAbstract.lean:236; PropTheory.lean:410,418 | confirmed | proven |
| Theorem 22 | 22, p.43 | Under NT + Constancy: lc exist; `Sat_i` iff `Sat'_i` iff `C[F] != #` | prop. fragment, no side conditions: `thm22_prop : (SatI I C F <-> SatI' I C F) /\ (SatI' I C F <-> dyn I F C != none)` | PropTheory.lean:439 | modified-statement | proven for the propositional fragment; general L not formalized (rests on Theorem 2) |
| Example 23a | 23a, p.44 | `QQ'` in `(Infinitely-many P . QQ')` has no local context in `{w}` | `example23a : not (exists x, IsLC Envs C x)` (`W = Unit`, `D = Nat`, `Inf` = infinitely many) | InfinitelyMany.lean:49 | confirmed | proven |
| Example 23b | 23b, p.44 | `Sat'_i`/`Transp_i` holds without `C |= (Every P . Q)` | `example23b : Tr Envs C Qinf /\ SatP Envs C Qinf /\ not (forall d, Qinf () d = true)` (`Q d := d != 0`) | InfinitelyMany.lean:75 | confirmed | proven |
| Lemma 6 | 30, p.45 | If each trigger occurs once, `Super = Kleene` | `lemma6 I F (hL : LinK symS F) w : Super I F w = Kleene I F w` (propositional; hyp. = distinct trigger symbols) | KleeneCore.lean:328 | confirmed | proven (propositional) |
| Lemma 7 | 31, p.45-46 | `Kleene(F,w) != #` implies `Super = Kleene` | `lemma7 I F w (h : Kleene I F w != none) : Super I F w = Kleene I F w` | KleeneCore.lean:350 | confirmed | proven (propositional) |
| Lemma 8 | 32, p.46 | `Kleene-acc_v(C,F)` implies `Super-acc_v(C,F)` and `Kleene = Super` on C | `lemma8_i_super`, `lemma8_s_super`, `lemma8_i_eq`, `lemma8_s_eq`, `kleeneAccI_S` | KleeneTheory.lean:314,321,343,331,336 | confirmed | proven (propositional) |
| Lemmas 9, 10, Def. 33 | 33-35, p.46-47 | `n`-indexed acceptability, prefix lemmas | -- | -- | n/a | not formalized (auxiliary machinery of the paper's inductive proofs of 36/38; our proofs of those theorems use a different route) |
| Theorem 36 | 36, p.47 | (a) `Kleene-acc_i` iff `Super-acc_i`; (b) then `Kleene(F,w)=Super(F,w)` on C | `theorem36 I C F : (KleeneAccI I C F <-> SuperAccI I C F) /\ (KleeneAccI I C F -> forall w, C w -> Kleene I F w = Super I F w)` | KleeneTheory.lean:349 | corrected-proof | proven (propositional fragment; the paper's proof has a gap, E7) |
| (new) | -- | In the propositional fragment all incremental notions coincide | `prop_fragment_collapse : (TranspI <-> dyn != none) /\ (KleeneAccI <-> TranspI) /\ (SuperAccI <-> TranspI)` | KleeneTheory.lean:364 | n/a | proven |
| Lemma 11 | 37, p.47 | `Kleene-acc_s` implies `Super-acc_s`; converse fails for `(pp' or (not pp'))` if `p` not a tautology | `lemma8_s_super`; `lemma11_super : SuperAccS I C (exF a b)` (every `C`); `lemma11_not_kleene (hw : C w) (hp : I a w = false) : not KleeneAccS I C (exF a b)` | KleeneTheory.lean:321,377,388 | confirmed | proven |
| Theorem 38 (a) | 38a, p.47-48 | `Transp_i(C,F)` implies `Kleene-acc_i(C,F)` and `Super-acc_i` | `theorem38a I C F : TranspI I C F -> KleeneAccI I C F /\ SuperAccI I C F` | KleeneTheory.lean:356 | confirmed | proven (propositional); predicative triggers/quantifiers not formalized |
| Theorem 38 (b) | 38b, p.48 | Converse fails: `(No P . QQ')`, `C={w}`, `d1` not Q, `d2` Q and Q' | `theorem38b_39b : Det (VP P2 Q2 Q2') /\ not transNo P2 Q2 /\ not dynDefined P2 Q2` (also `ex_value_false : valOpt (VP P2 Q2 Q2') = some false`; general characterisation `kleeneNo_iff`) | Quantifier.lean:167,153,81 | confirmed | counterexample found (claim confirmed; needs quantifiers: false in the propositional fragment) |
| Theorem 39 (a) | 39a, p.48-49 | `(pp' and qq')`, `C={w1,w2}`: sym. Transp holds, sym. Kleene and Super fail | `theorem39a : TranspS I39 (fun _ => True) F39 /\ not KleeneAccS I39 (fun _ => True) F39 /\ not SuperAccS I39 (fun _ => True) F39` | KleeneTheory.lean:405 | confirmed | counterexample found (claim confirmed) |
| Theorem 39 (b) | 39b, p.49 | `(No P . QQ')` same model: sym. Kleene/Super hold, sym. Transp fails | `theorem38b_39b` (trigger last, so incremental = symmetric) | Quantifier.lean:167 | confirmed | counterexample found (claim confirmed) |
| Theorem 41 | 41, p.49-50 | Propositional fragment: `Standard-Kleene(F,w) = Kleene(F,w)` | `theorem41 I F w : Kleene I F w = sk I F w` | KleeneCore.lean:322 | confirmed | proven |
| Sanity | -- | `pp'` presupposes `p`; `(p and pp')` presupposes nothing; `(pp' and p)` presupposes `p` | `sanity_*` (4 theorems) | Sanity.lean | confirmed | proven |

## 2. Errors and issues found in the paper

Severity: **ERROR** = a stated claim or proof step is false as written; **GAP** = proof step missing/unjustified but
repairable; **OVERCLAIM**; **TYPO**.

**E1. ERROR (proof of Lemma 1, item 12, p.41).**  The candidate
`LC^i := λw. 1 iff for some g, some good final β', w ⊭ ... ` is not restricted to `w ∈ C`.  Step 2 ("for every
x in tr^i(C,E,a_b), LC^i entails x") supposes `LC^i(w)=1`, `x(w)=0` and then uses `x in tr` at `w`; but
membership in `tr(C,...)` only constrains `x` on `C`, so for `w ∉ C` there is no contradiction.  With `≤` as in
items 4a/11 (global), `LC^i` is then not below every transparent `x`.  Worse, for the top-level sentence `pp'`
(hole with empty `α`, `β`) `LC^i(w)=1` at *every* world (take `g` a tautology), so `Sat` (item 17a, `lc ≤ d`)
would demand that `p` be a tautology.  Lean: `lemma1_paper_candidate_fails` (with `C = ∅`, `bot` is transparent
but the paper's candidate is true everywhere).  **Fix:** define `LC^i(w)=1` iff `w ∈ C` and (...) (this is what
Lemma 4 does with its "`z` otherwise" clause); the corrected statement is `LC.lemma1` (LCAbstract.lean:145).
(Alternative fix: read `≤` in 11/17 as `C`-relative; then the step "`lc ≤ C`" in Lemma 5 must be dropped.)
Also in this proof: "x ∈ tr^i(C, **F**, a_b)" should read `E`.

**E2. OVERCLAIM (sentence introducing item 23, p.44).**  "...`Sat'`, whose incremental version yields full
equivalence with Dynamic Semantics."  Example 23b itself shows `Sat'_i(C,F)` (= `Transp_i`) without the dynamic
presupposition `C |= (Every P . Q)`.  Equivalence with dynamic semantics is only established (Thm 22)
under Non-Triviality + Constancy (finite domain).  Lean: `example23b`.

**E3. ERROR (cross-reference, proof of Theorem 22(ii), p.43).**  "follows from (i), **9c** and 21(ii)": 9c is
Theorem 1 (propositional fragment only); the needed result is **9d** (Theorem 2).

**E4. GAP (Definition 10, p.41; Lemma 2 and Theorem 21).**  `tr` quantifies over "every constituent d' of the same
type as d".  Lemma 2's step 2 applies the property to `(c'' and d')` and Theorem 21 to `(d and d'')`, which are
not constituents of the formula.  `d'` must range over *all* expressions (hence Expressivity, item 3).  Lean
quantifies over all `γ`.

**E5. GAP (Lemma 3 and Existence Theorem 16(b), p.42).**  (i) Lemma 3 needs `tr` nonempty (it contains the
top element `λw.1`), never mentioned.  (ii) The proof of 16(b) says `tr_v({w},E,a_b)` is finite because "there are
only finitely many functions of type τ with `D_s={w}`".  Literally, objects are intensions over all of `W`,
so `tr` is infinite if `W` is; finiteness holds only modulo the value at `w`.  The argument works when
restrictions are identified up to their value at `w`, which is what Lemma 4's pointwise construction
uses.  Formalised this way in `LC.existence` (finite enumeration of `D → Bool` is a hypothesis).

**E6. GAP/TYPO (Lemma 5, Def. 18, p.42-43).**  (i) "`lc ≤ C`" (proof of Lemma 5) is true only for the
corrected `lc` (cf. E1).  (ii) In Def. 18a the clause "for every `X' ≤ X` in `tr`, `C |= X' ≤ d`" is redundant:
`Sat'` is equivalent to "some `X ∈ tr` is `≤_C d`"; the proof of Lemma 5 in Lean does not need it.
Global `≤` (17a) and `C`-relative `≤` (18a) are mixed.

**E7. GAP (proof of Theorem 36, p.47).**  The induction statement `P(n)` is for a fixed `F`, but the induction
step applies the induction hypothesis to `α D β'` (another formula) and needs `Super-acc_i(C, α D β', m)`
(justification via Lemma 10 is only indirect: Lemma 10a gives `Super-acc(C, α dd' β')`, not `α D β'`);
`for all w ∈ W` should be `w ∈ C`.  Repair: state `P(n)` for all formulas.  The theorem itself is TRUE for
the propositional fragment (proven in Lean by a different route: super-acceptability forces the local-context
condition, `superAcc_lcCond`, which gives Kleene-acceptability, `lcCond_kleeneAccI`).

**E8. GAP/TYPOS (proof of Theorem 38a, p.48-49).**  The set `D` is defined and `D'` is used ("Step 1: D' ⊆ G");
"`g0`, `g1`" become "`g1`, `g2`"; "`I**(g)(w) = i'(d)(w)`" should be `i'(dd'^{m+1})(w)`;
"if `I**(d')(w)(x)=0`" should be `d`.  The statement is true for the propositional fragment (Lean:
`theorem38a`); the predicative case is not formalised.

**E9. TYPOS.**
* 5b: `[[E'E]] = [[(E' and E)]] = [[E']] ∧ [[E']]` should end in `[[E']] ∧ [[E]]`.
* 14 (Lemma 3): "`v ∈ {i, g}`" should be `{i, s}`; 16(a): "`a dd b`" should be `a E b`; 15: "`lc_v({w}, a d, a_b)`".
* 17b: "`lc_v(C, dd', a_b) ≠ #`" inside a quantification over `ee'` should read `ee'`.
* 13 (Lemma 2), steps 4-5: "`a' d' b'`" should be `a d' b'`.
* 2 vs 6: `Q` is used both for the quantifier `Q_i` and for the scope predicate (`R` in 6).
* 7b: incremental Be Brief is stated with `β` (PDF) although it quantifies over good finals `β'` (8a).
* 21(i): `Transp_v(C, dd', a_b)` is not defined in the appendix (only for formulas, item 8; the main text
  (57)-(58) has it).
* 24: stray "`i'=(pp')(w)`"; 26b/29b omit the quantification over `dd', α, β`
  (equivalent to `Super(F,w) ≠ #` for all `w ∈ C`); 39 (proof): items (ii)a/(ii)b are in the
  opposite order of the two triggers; 41, Case 3(b): "`j'/At(H)`" should be `j''`.
* 23a: "(and also `x ≤ x'`)" is false as an inclusion (`x'` is `x` minus one element); harmless, the argument only needs `x' ≤ x` and `x'` transparent.
* 38b: "(35)" is item (35) of the main text, not the appendix's Lemma 10 (item 35).

**E10. NOT AN ERROR, but worth stating (new result).**  In the propositional fragment the converse of
Theorem 38 also holds: `Transp_i`, `Kleene-acc_i`, `Super-acc_i` and definedness of Heim's `C[F]` coincide
(`prop_fragment_collapse`).  So "in general the converse does not hold" is correct only because
of quantificational sentences, as in the paper's example `(No P . QQ')`.  Also in the propositional
fragment Theorems 22 needs neither Non-Triviality nor Constancy (`thm22_prop`).

**Claims checked and found correct** (modulo typos): Lemma 2, Lemma 3 (given non-emptiness), Lemma 4, Lemma 5,
Theorem 20, Theorem 21, Example 23a/b (the "remove one element" argument is sound), Lemmas 6-8, Theorem 36 (statement),
Lemma 11, Theorem 38 (a) and (b), Theorem 39 (a) and (b), Theorem 41 (the proof's independence step for
`i'+j'` is valid because the tokens of `F#` are pairwise distinct).

## 3. Fidelity of the formalisation: what was simplified

1. **Language.**  The main results are formalised for the *propositional fragment* only (atoms, `pp'`, not, and,
   or, if).  The full L (predicates, generalized quantifiers, context variables `c'`, assignment functions) is *not*
   formalised.  Quantificational content is covered by (i) the abstract framework `LCAbstract.lean`, which is
   stated for arbitrary extensional environments over arbitrary `D` (so Lemmas 2-5, Thm 20, 21 hold for
   predicates too, as in the paper), (ii) the single sentence `(No P . QQ')` on one world with `D = Fin n`
   (Thm 38b/39b), (iii) Example 23 with `D = Nat`.  Not covered: Theorem 2, general Theorem 22,
   Theorem 16(b) for full L, quantificational versions of Thm 36/38a and Lemmas 6-8.
2. **Good finals.**  A string `α _ β'` is modelled abstractly by an *environment* `Ψ : Val → W → Bool` (semantic
   effect of filling the hole), and in the propositional instance by a list of frames (`neg`, `left o G`, `right o F`).
   Incremental version = same left siblings, arbitrary right siblings (`Frame.same`); symmetric = the actual
   context.  For a hole that is the *left* operand, the connective is fixed by the frame (in the paper,
   `β'` may also change the connective).  I did not prove this makes no difference; informally it does not, since
   the `and`/trivial-completion already forces the same condition (and the brute-force checks below agree).
3. **Expressions `γ`, `d'`** range over all formulas (Transp) or all functions (abstract `tr`), i.e. Expressivity
   (item 3) is assumed; in the propositional bridge (`bridge_i`) it is the hypothesis `Expressive I`.
4. **Context sets** are `W -> Prop` on an arbitrary type `W` (no finiteness).  The dynamic semantics is
   classical-logic-based (`dyn` is noncomputable).
5. **Trivalent values** are `Option Bool`.  `valOpt` reads a trivalent value off the set of values attained
   by extensions; `Super`/`Kleene` are then exactly items 25/28 (`super_eq_some_iff`, `kleene_eq_some_iff`).
6. **Numbering (item 27)** is global (token `k` = k-th trigger, left to right) instead of per-symbol;
   since distinct superscripts make tokens independent, this is equivalent.  Trigger symbols are pairs of
   letter *names* `(a,b)`, so two names for the same proposition are different symbols, as in the paper.
7. **Acceptability** (`SuperAccI` etc.) is as in items 26/29: all trigger occurrences, all good finals
   without triggers, all `w ∈ C`.
8. **`(No P . QQ')`** is specialised: a single world, `D = Fin n`, quantifier as tree of numbers, the trigger is
   the whole scope, so incremental and symmetric versions coincide.  Super and Kleene coincide because the trigger
   occurs once.
9. **Independent evidence.**  Before proving, the propositional claims (Thm 1, 36, 38a, 41, converse of 38, `Kleene = SK`)
   were also brute-force checked in Python on random formulas over 2 and 3 worlds
   (`lean/bruteforce_check.py`, run `python3 bruteforce_check.py 2 1 3000`; prints `{}` when no counterexample is found);
   no discrepancy.  This is exploration only, the Lean files are the proofs.