Anti-dynamics: presupposition projection without dynamic semantics (J. Logic, Language and Information 16, 2007)
Transparency compared with Heim/Beaver dynamic semantics: Theorem 1 (propositional), Lemmas 1-2 and Theorem 2 (quantificational), the worked examples and the deviant connectives (and*, or*, unless).
Paper text (symbols restored from the PDF)(21) Dynamic (Trivalent) Semantics Let C be a subset of W. C[p] = {w ∈ C: p^w = 1} C[p̲p′] = # iff for some w ∈ C, p^w = 0; if ≠ #, C[p̲p′] = {w ∈ C: p′^w = 1} C[(not F)] = # iff C[F] = #; if ≠ #, C[(not F)] = C−C[F] C[(F and G)] = # iff C[F] = # or (C[F] ≠ # and C[F][G] = #); if ≠ #, C[(F and G)] = C[F][G] C[(F or G)] = # iff C[F] = # or (C[F] ≠ # and C[not F][G] = #); if ≠ #, C[(F or G)] = C[F] ∪ C[not F][G]
Statementformulas over clauses with not/and/or/if; CCPs with definedness (or per Beaver; if F.G = C − C[F][not G])
/-- Formulas over leaf clauses `L`. -/inductive Fm (L : Type) where
| leaf : L → Fm L
| neg : Fm L → Fm L
| conj : Fm L → Fm L → Fm L
| disj : Fm L → Fm L → Fm L
| cond : Fm L → Fm L → Fm L
/-- Heim's update `C[F]` (meaningful only where `Def` holds). Paper (21). -/def Upd (S : Sys W L) : Fm L → WSet W → WSet W
| .leaf l, C => S.lupd l C
| .neg F, C => fun w => C w ∧ ¬ Upd S F C w
| .conj F G, C => Upd S G (Upd S F C)
| .disj F G, C => fun w => Upd S F C w ∨ Upd S G (fun v => C v ∧ ¬ Upd S F C v) w
| .cond F G, C => fun w => C w ∧ ¬ (Upd S F C w ∧ ¬ Upd S G (Upd S F C) w)
/-- `Def S F C` iff `C[F] ≠ #`. Paper (21). -/def Def (S : Sys W L) : Fm L → WSet W → Prop
| .leaf l, C => S.ldef l C
| .neg F, C => Def S F C
| .conj F G, C => Def S F C ∧ Def S G (Upd S F C)
| .disj F G, C => Def S F C ∧ Def S G (fun v => C v ∧ ¬ Upd S F C v)
| .cond F G, C => Def S F C ∧ Def S G (Upd S F C)
def sys (v : W → ι → Bool) (i0 : ι) : Sys W (PLeaf ι) where
sem := fun l w => match l with
| .atom i => v w i
| .trig a b => v w a && v w b
lupd := fun l C => match l with
| .atom i => fun w => C w ∧ v w i = true
| .trig _ b => fun w => C w ∧ v w b = true
ldef := fun l C => match l with
| .atom _ => True
| .trig a _ => ∀ w, C w → v w a = true
lvar := fun l φ₁ φ₂ => match l with
| .atom _ => False
| .trig a _ => ∃ γ, φ₁ = .conj (at_ a) γ ∧ φ₂ = γ
top := .disj (at_ i0) (.neg (at_ i0))
bot := .conj (at_ i0) (.neg (at_ i0))
top_ok := byintro w; simp [evalF, at_]
bot_ok := byintro w; simp [evalF, at_]
lupd_static := byintro l C h
cases l with
| atom i => rfl
| trig a b =>
funext w; apply propext
simp only
...
/-- Heim's update (21) for `(Q P . R)`: only assertive components enter the counts. -/def qupd (q : κ) (P R : Pred ρ) (C : WSet W) : WSet W := fun w =>
C w ∧ M.f q (cnt M.n (fun d => M.passert P w d && !M.passert R w d))
(cnt M.n (fun d => M.passert P w d && M.passert R w d)) = true
/-- Heim's definedness condition (21). -/def qdef (P R : Pred ρ) (C : WSet W) : Prop :=
(∀ w, C w → ∀ d, d < M.n → M.ppre P w d = true) ∧
(∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.ppre R w d = true)
Paper text (symbols restored from the PDF)(25) Static (Bivalent) Semantics w ⊨ p iff p^w = 1 w ⊨ p̲p′ iff p^w = p′^w = 1 w ⊨ (not F) iff w ⊭ F w ⊨ (F and G) iff w ⊨ F and w ⊨ G w ⊨ (F or G) iff w ⊨ F or w ⊨ G w ⊨ (if F. G) iff w ⊭ F or w ⊨ G
Statementp̲p' = conjunction; if = material implication; (Q P.R) = f(|P−R|,|P∩R|)
/-- Bivalent (static) semantics (paper (25)); `if` is material implication. -/def evalF {W L : Type} (sem : L → W → Bool) : Fm L → W → Bool
| .leaf l, w => sem l w
| .neg F, w => !(evalF sem F w)
| .conj F G, w => evalF sem F w && evalF sem G w
| .disj F G, w => evalF sem F w || evalF sem G w
| .cond F G, w => !(evalF sem F w) || evalF sem G w
/-- Static semantics (25) of `(Q P . R)`: `f(|P∖R|, |P∩R|)` computed with the static values. -/def qsem (q : κ) (P R : Pred ρ) (w : W) : Bool :=
M.f q (cnt M.n (fun d => M.pstat P w d && !M.pstat R w d))
(cnt M.n (fun d => M.pstat P w d && M.pstat R w d))
R3definitions
Transparency (two readings)
Paper: §2.1 (5),(6); §3.2 (26), p.330-1, 338 PDF p.6
Paper text (symbols restored from the PDF)(26) Principle of Transparency For any initial string of the form α d̲d′ of a sentence uttered in a background of assumptions C (where d̲d′ is propositional or predicative), it should be the case that for any constituent γ of the same type as d and for any sentence completion β, C ⊨ α (d and γ)β ⇔ αγβ
Statementfor every initial string α d̲d' and completion β: C ⊨ α(d and γ)β ⇔ αγβ
Not stated in the paper as such — related passage (Transparency as defined on strings; the equivalence with the completion-context formulation is implicit in the paper (Syntactic Lemma, §3.1))
Related passage in the paper(5) Definition of Transparency Given a Context Set C, a predicative or propositional occurrence of d is transparent (and hence infelicitous) in a sentence that starts with the string α (d and just in case for any constituent γ of the same type as d and for any sentence completion β, C ⊨ α (d and γ)β ⇔ αγβ
StatementStrTransp C F ↔ Transp C F for every model and every F
Paper text(19) Syntactic Lemma [...] b. If a formula F starts with (s, where s is a symbol different from a parenthesis, then the smallest initial string of F which is a constituent is F itself.
Statementno formula string is a proper initial string of another
Lean statementser_append_inj : ser F ++ s = ser G ++ t → F = G ∧ s = t
Lean: Strings.lean:45 · proven (hypothesis "starts with (s, s not a parenthesis" is not needed)
theorem ser_append_inj : ∀ (F G : Fm L) (s t : List (Tok L)), ser F ++ s = ser G ++ t →
F = G ∧ s = t := byintro F
induction F with
| leaf l =>
intro G s t h
cases G with
| leaf l' => simp [ser] at h; exact ⟨byrw [h.1], h.2⟩
| neg G => simp [ser] at h
| conj G1 G2 => simp [ser] at h
| disj G1 G2 => simp [ser] at h
| cond G1 G2 => simp [ser] at h
| neg F ih =>
intro G s t h
cases G with
| leaf l' => simp [ser] at h
| neg G =>
simp only [ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
have := ih G _ _ h
exact ⟨byrw [this.1], by simpa using this.2⟩
| conj G1 G2 =>
simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
| disj G1 G2 =>
...
Minor typo: (19b): proof should cover all cases (proof gap, statement true)
Q8proof gap Syntactic Lemma (19b): give a proof that covers all cases; (19a) is imprecise
Location: Section 3.1, Syntactic Lemma (19), p. 335-336 PDF p.11
Paper text
Proof Suppose this were not the case, and suppose that c is a proper initial substring of F which is a constituent. Giventhat c is a propersubstring of F,itmust have been concatenated with other symbols (to its right) by one of the object-language rules in (18). But each such rule would require that there be a left parenthesisbeforec, contrary to our assumption that c is initial.
Suggested replacement
Proof Suppose this were not the case, and suppose that c is a proper initial substring of F which is a constituent. Since F starts with a left bracket and no atomic constituent starts with a bracket, c is a complex constituent; so, as noted in the proof of (a), c begins with a left bracket and ends at the first point at which an equal number of left and right brackets has been encountered. But F is itself a complex constituent beginning with a left bracket, so it ends at that same point. Hence c = F, contrary to our assumption.
Further edits
Paper text
a. If α is the beginning of a constituent in a string F, then α is the beginning of a constituent in any well-formed string that containsα.
Suggested replacement (Syntactic Lemma (19a), statement; OPTIONAL and to be checked)
a. If α is the beginning of a constituent in a string F, then α is the beginning of a constituent in any well-formed string that has α as an initial string.
What the paper does, and why it fails
The proof of (19b) says every rule that attaches material to the right of c requires a left parenthesis before c. This is only true of the compound rules; atomic constituents (p_i p_k, P_i P_k) are not covered. The statement of (19a), ‘in any well-formed string that contains α’, is also loose.
What the change does
The new proof of (19b) uses the bracket-counting argument already given for (a), and covers atomic and compound c. (19b) is true (it is the prefix-freeness of the bracketed syntax, Lean: ser_append_inj, which does not even need the assumption ‘F starts with (s’). The optional change to (19a) states it for strings with α as an initial string, the form proved in Lean (syntactic_lemma_a).
Anything else affected?No other change: Theorems 1 and 2 use (19a) only in the form ‘α′ dd′ is the beginning of a constituent in α′ dd′ β’, i.e. for initial strings. Not checked beyond that.
Text note: The original of (19b) runs across a page break (the running head and footnote 9 lie between ‘by one of the’ and ‘object-language rules in (18)’); wording is verbatim.
Judgment call: the wording of this replacement is ours and not checked in Lean. The new proof of (19b) is our wording of the bracket-counting argument (Lean proves prefix-freeness by another route). The (19a) change follows the Lean statement and We have not checked that every use of (19a) in the paper is for an initial string.
theorem ser_append_inj : ∀ (F G : Fm L) (s t : List (Tok L)), ser F ++ s = ser G ++ t →
F = G ∧ s = t := byintro F
induction F with
| leaf l =>
intro G s t h
cases G with
| leaf l' => simp [ser] at h; exact ⟨byrw [h.1], h.2⟩
| neg G => simp [ser] at h
| conj G1 G2 => simp [ser] at h
| disj G1 G2 => simp [ser] at h
| cond G1 G2 => simp [ser] at h
| neg F ih =>
intro G s t h
cases G with
| leaf l' => simp [ser] at h
...
theorem syntactic_lemma_a : ∀ (c : Ctx L) (φ : Fm L) (β : List (Tok L)) (G : Fm L)
(tl : List (Tok L)), pre c ++ ser φ ++ β = ser G ++ tl →
∃ c'', Compl c c'' ∧ G = c''.plug φ ∧ β = post c'' ++ tl := byintro c
induction c with
| hole =>
intro φ β G tl h
simp only [pre, List.nil_append] at h
have := ser_append_inj φ G β tl h
obtain ⟨rfl, rfl⟩ := this
exact ⟨.hole, rfl, rfl, bysimp [post]⟩
| negC c ih =>
intro φ β G tl h
cases G with
| leaf l' => simp [pre, ser] at h
| neg G =>
...
Paper text(19) Syntactic Lemma a. If α is the beginning of a constituent in a string F, then α is the beginning of a constituent in any well-formed string that contains α.
Statementif α φ β is a formula (α initial string of an occurrence) then φ is a constituent of it and the formula is a completion context applied to φ
Lean statementsyntactic_lemma_a : pre c ++ ser φ ++ β = ser G ++ tl → ∃ c'', Compl c c'' ∧ G = c''.plug φ ∧ β = post c'' ++ tl
theorem syntactic_lemma_a : ∀ (c : Ctx L) (φ : Fm L) (β : List (Tok L)) (G : Fm L)
(tl : List (Tok L)), pre c ++ ser φ ++ β = ser G ++ tl →
∃ c'', Compl c c'' ∧ G = c''.plug φ ∧ β = post c'' ++ tl := byintro c
induction c with
| hole =>
intro φ β G tl h
simp only [pre, List.nil_append] at h
have := ser_append_inj φ G β tl h
obtain ⟨rfl, rfl⟩ := this
exact ⟨.hole, rfl, rfl, bysimp [post]⟩
| negC c ih =>
intro φ β G tl h
cases G with
| leaf l' => simp [pre, ser] at h
| neg G =>
simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G ([rp] ++ tl) (by simpa using h)
exact ⟨.negC c'', ⟨c'', rfl, hc⟩, bysimp [Ctx.plug, hG], bysimp [post, hβ]⟩
| conj G1 G2 =>
simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
| disj G1 G2 =>
simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
...
Minor typo: (19a) imprecise as stated; proof needs repair
Q8proof gap Syntactic Lemma (19b): give a proof that covers all cases; (19a) is imprecise (details above)
Paper text (symbols restored from the PDF)We could try to require that if a formula F is uttered in a Context Set C, C should satisfy: (10) C ⊨ F ⇔ F* It is immediate, however, that this fails to derive the asymmetric projective behavior of and. [...] But since the rule in (10) is to be interpreted within classical logic, it is intrinsically incapable of accounting for the asymmetric behavior of conjunction.
StatementC ⊨ F ⇔ F* cannot derive the asymmetry of and
Lean statementnaive_conj_symmetric : Naive C (G and H) ↔ Naive C (H and G); transp_conj_asymmetric (Transparency is asymmetric)
Propositional.lean:224 — lines 224–228 · open file
theorem naive_conj_symmetric (C : WSet W) (G H : PFm ι) :
Naive v i0 C (.conj G H) ↔ Naive v i0 C (.conj H G) := byunfold Naive Sys.CEquiv
constructor <;> intro h w hw <;> have := h w hw <;>
simp only [star, Fm.map, Sys.eval_conj] at this ⊢ <;> grind
Propositional.lean:231 — lines 230–238 · open file
/-- Transparency is asymmetric for `and`: `(p and q̲q')` vs `(q̲q' and p)`. -/theorem transp_conj_asymmetric :
∃ (C : WSet Bool) (v : Bool → Bool → Bool),
(sys v true).Transp C (.conj (at_ true) (tr_ false false)) ∧
¬ (sys v true).Transp C (.conj (tr_ false false) (at_ true)) := by-- worlds `false`/`true`; `p_true` is true only at `true`; `p_false` (= q) is true only at `true`refine ⟨fun _ => True, fun w _ => w, ?_, ?_⟩
· rw [ex15]; intro w _ hp; simpa using hp
· rw [ex14]; intro h; have := h false trivial; simpat this
Paper text (symbols restored from the PDF)Consider the sentence It is John who won. It is usually analyzed as p̲p′ with p = Exactly one person won, and p′ = John won. [...] (11) C ⊨ p̲p′ ⇔ p′ [...] The left-to-right direction is satisfied no matter what C is. As for the right-to-left direction, it is satisfied if and only if: (12) C ⊨ p′ ⇒ p But in the case at hand this yields a result which is too weak: we predict that it should only be presupposed that if John won, exactly one person won—which in most cases is trivially satisfied.
Statementfor p̲p' naive = C ⊨ p'⇒p, strictly weaker than C ⊨ p
Propositional.lean:199 — lines 198–211 · open file
/-- (11)-(12): for an atomic clause the naive requirement says only `C ⊨ p' ⇒ p`. -/theorem naive_atomic (C : WSet W) (a b : ι) :
Naive v i0 C (tr_ a b) ↔ EntImp v C b a := byunfold Naive Sys.CEquiv
rw [star_tr]
simp only [eval_tr, eval_at]
constructor
· intro h w hw hb
have := h w hw
cases ha : v w a <;> simp_all
· intro h w hw
cases hb : v w b
· simp
· simp [h w hw hb]
Propositional.lean:215 — lines 215–220 · open file
theorem naive_strictly_weaker :
∃ (C : WSet Unit) (v : Unit → Bool → Bool),
Naive v true C (tr_ false true) ∧ ¬ (sys v true).Transp C (tr_ false true) := byrefine ⟨fun _ => True, fun _ _ => false, ?_, ?_⟩
· rw [naive_atomic]; intro w _ hb; simpat hb
· rw [transp_atomic]; intro h; have := h () trivial; simpat this
Paper text (symbols restored from the PDF)(13) for every expression γ of the same type as d and every sentence completion β, C ⊨ (d and γ)β ⇔ γβ It is immediate that the condition is satisfied if C ⊨ p. Conversely, if the condition is satisfied, for null β and for some tautology γ, we have C ⊨ (p and γ) ⇔ γ and thus C ⊨ p, as is desired.
Propositional.lean:135 — lines 135–138 · open file
theorem transp_atomic (C : WSet W) (a b : ι) :
(sys v i0).Transp C (tr_ a b) ↔ Ent v C a := byhave := leaf_transp_iff_def v i0 C (.trig a b)
exact this
Paper text (symbols restored from the PDF)(14) (p̲p′ and q) a. Transparency requires that for each clause γ and for each sentence completion β, C ⊨ ((p and γ)β ⇔ (γβ b. Claim Transparency is satisfied ⇔ C ⊨ p
StatementTransp ↔ C ⊨ p
Lean statementex14 (proved from the decomposition lemmas, not from Heim)
Propositional.lean:145 — lines 144–148 · open file
/-- (14): `(p̲p' and q)` presupposes `p`. -/theorem ex14 (C : WSet W) (a b q : ι) :
(sys v i0).Transp C (.conj (tr_ a b) (at_ q)) ↔ Ent v C a := byrw [caseD, transp_atomic]
exact ⟨fun h => h.1, fun h => ⟨h, transp_plain v i0 _ q⟩⟩
Paper text (symbols restored from the PDF)(15) (p and q̲q′) a. Transparency requires that for each clause γ and each sentence completion β, C ⊨ (p and (q and γ)β ⇔ (p and γβ b. Claim Transparency is satisfied ⇔ C ⊨ p ⇒ q
Propositional.lean:151 — lines 150–161 · open file
/-- (15): `(p and q̲q')` presupposes `p ⇒ q`. -/theorem ex15 (C : WSet W) (p a b : ι) :
(sys v i0).Transp C (.conj (at_ p) (tr_ a b)) ↔ EntImp v C p a := byrw [caseD]
constructor
· rintro ⟨_, h⟩ w hw hp
have := (transp_atomic v i0 _ a b).1 h w ⟨hw, by simpa using hp⟩
exact this
· intro h
refine ⟨transp_plain v i0 _ p, (transp_atomic v i0 _ a b).2 ?_⟩
rintro w ⟨hw, hp⟩
exact h w hw (by simpa using hp)
Paper text (symbols restored from the PDF)(16) (if p̲p′ · q) a. Transparency requires that for each clause γ and for each sentence completion β, C ⊨ (if (p and γ)β ⇔ (if γβ b. Claim Transparency is satisfied ⇔ C ⊨ p
Propositional.lean:164 — lines 163–167 · open file
/-- (16): `(if p̲p' . q)` presupposes `p`. -/theorem ex16 (C : WSet W) (a b q : ι) :
(sys v i0).Transp C (.cond (tr_ a b) (at_ q)) ↔ Ent v C a := byrw [caseF, transp_atomic]
exact ⟨fun h => h.1, fun h => ⟨h, transp_plain v i0 _ q⟩⟩
Paper text (symbols restored from the PDF)(17) (if p · q̲q′) a. Transparency requires that for each clause γ and each sentence completion β, C ⊨ (if p. (q and γ)β ⇔ (if p · γβ b. Claim Transparency is satisfied ⇔ C ⊨ p ⇒ q
Propositional.lean:170 — lines 169–179 · open file
/-- (17): `(if p . q̲q')` presupposes `p ⇒ q`. -/theorem ex17 (C : WSet W) (p a b : ι) :
(sys v i0).Transp C (.cond (at_ p) (tr_ a b)) ↔ EntImp v C p a := byrw [caseF]
constructor
· rintro ⟨_, h⟩ w hw hp
exact (transp_atomic v i0 _ a b).1 h w ⟨hw, by simpa using hp⟩
· intro h
refine ⟨transp_plain v i0 _ p, (transp_atomic v i0 _ a b).2 ?_⟩
rintro w ⟨hw, hp⟩
exact h w hw (by simpa using hp)
Paper text (symbols restored from the PDF)(23) Dynamic Transparency Let F be a formula, and let F* be the result of deleting from F all underlined material. Then for any C ⊆ W, if C[F] ≠ #, then C[F] = C[F*].
Propositional.lean:243 — lines 242–245 · open file
/-- **Dynamic Transparency (23)**: if `C[F] ≠ #` then `C[F] = C[F*]`. -/theorem dynamic_transparency (C : WSet W) (F : PFm ι) (h : (sys v i0).Def F C) :
(sys v i0).Upd (star F) C = (sys v i0).Upd F C :=
Sys.dyn_transparency _ star1 (byintro l C _; cases l <;> rfl) F C h
Propositional.lean:248 — lines 247–249 · open file
/-- `F*` is presupposition-free, hence always defined (so (23) is not vacuous). -/theorem star_defined (C : WSet W) (F : PFm ι) : (sys v i0).Def (star F) C :=
Sys.def_map _ star1 (byintro l C; cases l <;> simp [star1, sys]) F C
theorem dynamic_transparency_quant (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(h : (sys M).Def F C) : (sys M).Upd (F.map starL) C = (sys M).Upd F C ∧
(sys M).Def (F.map starL) C := byrefine ⟨Sys.dyn_transparency _ starL ?_ F C h, Sys.def_map _ starL ?_ F C⟩
· intro l C' _
cases l with
| atom i => rfl
| trig a b => rfl
| quant q P R =>
show M.qupd q (starP P) (starP R) C' = M.qupd q P R C'
funext w
simp only [QModel.qupd, passert_starP]
· intro l C'
cases l with
| atom i => trivial
| trig a b => trivial
| quant q P R =>
exact ⟨fun w _ d _ => ppre_starP M P w d, fun w _ d _ _ => ppre_starP M R w d⟩
theorem dyn_transparency (S : Sys W L) (f : L → L)
(hf : ∀ l C, S.ldef l C → S.lupd (f l) C = S.lupd l C) :
∀ (F : Fm L) (C : WSet W), S.Def F C → S.Upd (F.map f) C = S.Upd F C := byintro F
induction F with
| leaf l => intro C h; exact hf l C h
| neg F ih =>
intro C h
have := ih C h
funext w; apply propext
simp only [Fm.map, Upd, this]
| conj F G ihF ihG =>
intro C ⟨h1, h2⟩
have e1 := ihF C h1
simp only [Fm.map, Upd]
rw [e1, ihG _ h2]
| disj F G ihF ihG =>
intro C ⟨h1, h2⟩
have e1 := ihF C h1
simp only [Fm.map, Upd]
rw [e1, ihG _ h2]
| cond F G ihF ihG =>
intro C ⟨h1, h2⟩
have e1 := ihF C h1
...
Paper text (symbols restored from the PDF)Now consider the formula H = ((not p) or* p̲p′), with the assumption that C[p̲p′] = #. [...] By construction, C[H] ≠ #, but in general C[H] ≠ C[H*] (for instance C[H] may contain C-worlds for which p^w = 0 and p′^w = 1, but C[H*] cannot).
Statementfor H = ((not p) or* p̲p') and C[p̲p'] = #: C[H] defined but C[H] ≠ C[H*]
theorem or_star_breaks_dynamic_transparency :
∃ (v : Bool × Bool → Bool → Bool) (C : WSet (Bool × Bool)),
let F : PFm Bool := .neg (at_ false)
(sys v true).Def (.disj F (tr_ false true)) C ∧
¬ (sys v true).Def (tr_ false true) C ∧
∃ w, C w ∧ orStarUpd v true F (tr_ false true) C w ∧
¬ orStarUpd v true F (star (tr_ false true)) C w := byrefine ⟨fun w i => if i then w.2 else w.1, fun _ => True, ?_⟩
intro F
refine ⟨?_, ?_, ((false, true)), trivial, ?_, ?_⟩
· simp only [Sys.Def, Sys.Upd, sys, F, at_, tr_]
refine ⟨trivial, fun w hw => ?_⟩
simpa using hw
· simp only [Sys.Def, sys, tr_]
intro h
have := h (false, true) trivialsimpat this
· have hd : ¬ (sys (fun (w : Bool × Bool) (i : Bool) => if i then w.2 else w.1) true).Def
(tr_ false true) (fun _ => True) := bysimp only [Sys.Def, sys, tr_]
intro h
have := h (false, true) trivialsimpat this
simp only [orStarUpd, hd, ite_false]
...
Paper text (symbols restored from the PDF)(2) C[F and* G] = # iff C[G] = # or (C[G] ≠ # and C[G][F] = #). If ≠ #, C[F and* G] = C[G][F]. It is immediate that C[F and* G] = C[G and F] (with the order of the conjuncts reversed), and that when neither F nor G contains any presupposition trigger, C[F and* G] = C[F and G] (because in this case the order of the conjuncts does not matter).
StatementC[F and* G] = C[G and F]; agrees with and on trigger-free F, G; Moldavia predictions reversed
/-- `C[F and* G] = C[G and F]` (definitionally). -/theorem andStar_eq_swap (F G : PFm ι) (C : WSet W) :
(andStarDef v i0 F G C ↔ (sys v i0).Def (.conj G F) C) ∧
andStarUpd v i0 F G C = (sys v i0).Upd (.conj G F) C := ⟨Iff.rfl, rfl⟩
/-- When neither conjunct contains a trigger, `and*` and `and` agree (definedness and update). -/theorem andStar_agrees_trigfree (F G : PFm ι) (hF : TrigFree F) (hG : TrigFree G) (C : WSet W) :
andStarDef v i0 F G C ∧ (sys v i0).Def (.conj F G) C ∧
andStarUpd v i0 F G C = (sys v i0).Upd (.conj F G) C := byrefine ⟨⟨trigFree_def v i0 G hG C, trigFree_def v i0 F hF _⟩,
⟨trigFree_def v i0 F hF C, trigFree_def v i0 G hG _⟩, ?_⟩
have h1 := (sys v i0).upd_eq_TS (.conj G F) C ⟨trigFree_def v i0 G hG C, trigFree_def v i0 F hF _⟩
have h2 := (sys v i0).upd_eq_TS (.conj F G) C ⟨trigFree_def v i0 F hF C, trigFree_def v i0 G hG _⟩
show (sys v i0).Upd (.conj G F) C = _
rw [h1, h2]
funext w; apply propext
simp only [Sys.TS, Sys.eval_conj]
cases (sys v i0).eval F w <;> cases (sys v i0).eval G w <;> simp
theorem andStar_not_transparency :
¬ ∀ (v : Bool → Bool → Bool) (C : WSet Bool) (F G : PFm Bool),
andStarDef v true F G C ↔ (sys v true).Transp C (.conj F G) := byintro h
have := h (fun _ _ => false) (fun w => w = false) (tr_ false true) (at_ true)
have h1 : andStarDef (fun (_ : Bool) (_ : Bool) => false) true (tr_ false true) (at_ true)
(fun w => w = false) := byrefine ⟨trivial, ?_⟩
intro w hw
simp [Sys.Upd, sys, at_] at hw
have h2 := this.1 h1
rw [ex14] at h2
have := h2 false rflsimpat this
Propositional.lean:101 — lines 100–103 · open file
/-- **Transparency Lemma (27a)**: `Transp(C, (G and δ)) → Transp(C, G)`. -/theorem transparency_lemma_a (C : WSet W) (G δ : PFm ι)
(h : (sys v i0).Transp C (.conj G δ)) : (sys v i0).Transp C G :=
((Sys.transp_conj _ C G δ).1 h).1
theorem transp_conj (S : Sys W L) (C : WSet W) (G H : Fm L) :
S.Transp C (.conj G H) ↔ S.Transp C G ∧ S.Transp (S.TS G C) H := byconstructor
· intro h
constructor
· intro π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.conjL π H) l (bysimp [Ctx.plug, hπ]) (.conjL π' S.top)
⟨π', S.top, Or.inl rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug, S.top_true] using this
· intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
have := h (.conjR G π) l (bysimp [Ctx.plug, hπ]) (.conjR G π')
⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
simpa [Ctx.plug, hwG] using this
· intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case conjL π1 r =>
obtain ⟨hG, rfl⟩ := hπ
obtain ⟨c', r', hor, hc'⟩ := hc
have := h1 π1 l hG c' hc' φ₁ φ₂ hv w hw
rcases hor withrfl | rfl <;> simp [Ctx.plug, this]
case conjR l' π2 =>
obtain ⟨hl, hH⟩ := hπ
subst hl
obtain ⟨c', rfl, hc'⟩ := hc
...
Minor typo: (27): state for every G and delta; define sentence completion delta
Q4ctypo Transparency Lemma (27): state it for every G and δ and say what a sentence completion δ is
Location: Section 4, Transparency Lemma (27), p. 339 PDF p.15
Paper text
a. Iffor some formula G and some sentence completion δ, Transp(C, (G δ)), then Transp(C, G).
Suggested replacement
a. For every formula G and every sentence completion δ (a string such as ‘and H)’ or ‘or H)’, which supplies the connective and the closing bracket), if Transp(C, (G δ)), then Transp(C, G).
Further edits
Paper text
b. Iffor some formula G and some sentence completion δ, Transp(C, (if G. δ)), then Transp(C, G).
Suggested replacement (Transparency Lemma (27b))
b. For every formula G and every sentence completion δ (a string such as ‘H)’), if Transp(C, (if G. δ)), then Transp(C, G).
What the paper does, and why it fails
‘If for some G and some δ, Transp(C, (G δ))’ is logically equivalent to the universal reading, but it reads as if one particular δ were needed. Also (G δ) does not look like a formula, since the connective and the closing bracket are part of δ, which is not said. The proof uses completions of the form ‘… and τ)’.
What the change does
The lemma is now stated for every G and every δ, which is what Theorems 1 and 2 use, and it says that δ includes the connective and the closing bracket. No proof step changes.
Anything else affected?No other change: the lemma as intended is what is used in Theorems 1 and 2 (Lean: transparency_lemma_a, transparency_lemma_b; completions carrying either ‘and’ or ‘or’ are modelled by Compl).
Text note: Wording is verbatim; symbols lost in the text extraction (⊨, ⊭, ⇔, superscripts, underlining, Greek letters, primes) were restored from the PDF.
Judgment call: the wording of this replacement is ours and not checked in Lean. The original statement is not false (‘for some’ is equivalent to ‘for every’ here); the edit is a clarity change. The reading of δ as ‘connective + material + closing bracket’ is our interpretation of the paper’s ‘sentence completion’.
/-- **Transparency Lemma (27a)**: `Transp(C, (G and δ)) → Transp(C, G)`. -/theorem transparency_lemma_a (C : WSet W) (G δ : PFm ι)
(h : (sys v i0).Transp C (.conj G δ)) : (sys v i0).Transp C G :=
((Sys.transp_conj _ C G δ).1 h).1
/-- **Transparency Lemma (27b)**: `Transp(C, (if G . δ)) → Transp(C, G)`. -/theorem transparency_lemma_b (C : WSet W) (G δ : PFm ι)
(h : (sys v i0).Transp C (.cond G δ)) : (sys v i0).Transp C G :=
((Sys.transp_cond _ C G δ).1 h).1
def Compl : Ctx L → Ctx L → Prop
| .hole, π' => π' = .hole
| .negC c, π' => ∃ c', π' = .negC c' ∧ Compl c c'
| .conjL c _, π' => ∃ c' r', (π' = .conjL c' r' ∨ π' = .disjL c' r') ∧ Compl c c'
| .disjL c _, π' => ∃ c' r', (π' = .conjL c' r' ∨ π' = .disjL c' r') ∧ Compl c c'
| .conjR l c, π' => ∃ c', π' = .conjR l c' ∧ Compl c c'
| .disjR l c, π' => ∃ c', π' = .disjR l c' ∧ Compl c c'
| .condL c _, π' => ∃ c' r', π' = .condL c' r' ∧ Compl c c'
| .condR l c, π' => ∃ c', π' = .condR l c' ∧ Compl c c'
Propositional.lean:106 — lines 105–108 · open file
/-- **Transparency Lemma (27b)**: `Transp(C, (if G . δ)) → Transp(C, G)`. -/theorem transparency_lemma_b (C : WSet W) (G δ : PFm ι)
(h : (sys v i0).Transp C (.cond G δ)) : (sys v i0).Transp C G :=
((Sys.transp_cond _ C G δ).1 h).1
theorem transp_cond (S : Sys W L) (C : WSet W) (G H : Fm L) :
S.Transp C (.cond G H) ↔ S.Transp C G ∧ S.Transp (S.TS G C) H := byconstructor
· intro h
constructor
· intro π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.condL π H) l (bysimp [Ctx.plug, hπ]) (.condL π' S.bot)
⟨π', S.bot, rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug, S.bot_false] using this
· intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
have := h (.condR G π) l (bysimp [Ctx.plug, hπ]) (.condR G π')
⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
simpa [Ctx.plug, hwG] using this
· intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case condL π1 r =>
obtain ⟨hG, rfl⟩ := hπ
obtain ⟨c', r', rfl, hc'⟩ := hc
have := h1 π1 l hG c' hc' φ₁ φ₂ hv w hw
simp [Ctx.plug, this]
case condR l' π2 =>
obtain ⟨hl, hH⟩ := hπ
subst hl
obtain ⟨c', rfl, hc'⟩ := hc
...
Minor typo: (27): state for every G and delta; define sentence completion delta
Q4ctypo Transparency Lemma (27): state it for every G and δ and say what a sentence completion δ is (details above)
Paper text (symbols restored from the PDF)Proof (by induction on the construction of formulas): [...] e. F = (G or H) [...] (ii) If C[F] ≠ #, then C[G] ≠ #, C[(not G)][H] ≠ #, and C[F] = C[G] ∪ C[(not G)][H]. By the Induction Hypothesis, C[G] = {w ∈ C: w ⊨ G}, C[(not G)] = {w ∈ C: w ⊭ G}, and C[(not G)][H] = {w ∈ C: w ⊭ G and w ⊨ H}. Therefore C[F]= {w ∈ C: w ⊨ G} ∪ {w ∈ C: w ⊭ G and w ⊨ H} = {w ∈ C: w ⊨ (G or H)}.
StatementTransp decomposes through not/and/or/if exactly as Heim's Def
Lean statementtransp_neg/conj/disj/cond; Sys.lift (induction); typo in (e) (see Q4)
theorem transp_neg (S : Sys W L) (C : WSet W) (G : Fm L) :
S.Transp C (.neg G) ↔ S.Transp C G := byconstructor
· intro h π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.negC π) l (bysimp [Ctx.plug, hπ]) (.negC π') ⟨π', rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug] using this
· intro h π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case negC π1 =>
obtain ⟨c', rfl, hc'⟩ := hc
have := h π1 l hπ c' hc' φ₁ φ₂ hv w hw
simp [Ctx.plug, this]
theorem transp_conj (S : Sys W L) (C : WSet W) (G H : Fm L) :
S.Transp C (.conj G H) ↔ S.Transp C G ∧ S.Transp (S.TS G C) H := byconstructor
· intro h
constructor
· intro π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.conjL π H) l (bysimp [Ctx.plug, hπ]) (.conjL π' S.top)
⟨π', S.top, Or.inl rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug, S.top_true] using this
· intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
have := h (.conjR G π) l (bysimp [Ctx.plug, hπ]) (.conjR G π')
⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
simpa [Ctx.plug, hwG] using this
· intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case conjL π1 r =>
obtain ⟨hG, rfl⟩ := hπ
obtain ⟨c', r', hor, hc'⟩ := hc
have := h1 π1 l hG c' hc' φ₁ φ₂ hv w hw
rcases hor withrfl | rfl <;> simp [Ctx.plug, this]
case conjR l' π2 =>
obtain ⟨hl, hH⟩ := hπ
subst hl
obtain ⟨c', rfl, hc'⟩ := hc
...
theorem transp_disj (S : Sys W L) (C : WSet W) (G H : Fm L) :
S.Transp C (.disj G H) ↔ S.Transp C G ∧ S.Transp (fun w => C w ∧ S.eval G w = false) H := byconstructor
· intro h
constructor
· intro π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.disjL π H) l (bysimp [Ctx.plug, hπ]) (.disjL π' S.bot)
⟨π', S.bot, Or.inr rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug, S.bot_false] using this
· intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
have := h (.disjR G π) l (bysimp [Ctx.plug, hπ]) (.disjR G π')
⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
simpa [Ctx.plug, hwG] using this
· intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case disjL π1 r =>
obtain ⟨hG, rfl⟩ := hπ
obtain ⟨c', r', hor, hc'⟩ := hc
have := h1 π1 l hG c' hc' φ₁ φ₂ hv w hw
rcases hor withrfl | rfl <;> simp [Ctx.plug, this]
case disjR l' π2 =>
obtain ⟨hl, hH⟩ := hπ
subst hl
obtain ⟨c', rfl, hc'⟩ := hc
...
theorem transp_cond (S : Sys W L) (C : WSet W) (G H : Fm L) :
S.Transp C (.cond G H) ↔ S.Transp C G ∧ S.Transp (S.TS G C) H := byconstructor
· intro h
constructor
· intro π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.condL π H) l (bysimp [Ctx.plug, hπ]) (.condL π' S.bot)
⟨π', S.bot, rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug, S.bot_false] using this
· intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
have := h (.condR G π) l (bysimp [Ctx.plug, hπ]) (.condR G π')
⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
simpa [Ctx.plug, hwG] using this
· intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case condL π1 r =>
obtain ⟨hG, rfl⟩ := hπ
obtain ⟨c', r', rfl, hc'⟩ := hc
have := h1 π1 l hG c' hc' φ₁ φ₂ hv w hw
simp [Ctx.plug, this]
case condR l' π2 =>
obtain ⟨hl, hH⟩ := hπ
subst hl
obtain ⟨c', rfl, hc'⟩ := hc
...
theorem lift (S : Sys W L) {C₀ : WSet W} {F₀ : Fm L}
(hleaf : ∀ C l, Accessed S C₀ F₀ C (.leaf l) → (S.Transp C (.leaf l) ↔ S.ldef l C)) :
∀ (F : Fm L) (C : WSet W), Accessed S C₀ F₀ C F → (S.Transp C F ↔ S.Def F C) := byintro F
induction F with
| leaf l => intro C h; exact hleaf C l h
| neg G ih =>
intro C h
rw [transp_neg]
exact ih C (.neg h)
| conj G H ihG ihH =>
intro C h
have hG := ihG C (.conjL h)
rw [transp_conj]
simp only [Def]
constructor
· rintro ⟨t1, t2⟩
have d1 := hG.1 t1
have e := upd_eq_TS S G C d1
have hH := ihH _ (.conjR h d1)
rw [e] at hH ⊢
exact ⟨d1, hH.1 t2⟩
· rintro ⟨d1, d2⟩
have e := upd_eq_TS S G C d1
...
Minor typo: typo in case (e)(i): conclusion should be Transp(C,(G or H))
Q4atypo Proof of Theorem 1, case (e)(i): the conclusion should be Transp(C, (G or H))
Location: Section 4, proof of Theorem 1, case (e)(i), p. 341 PDF p.17
Paper text
But this contradicts our hypothesis that Transp(C′, H). Thus Transp(C, (G and H)), i.e. Transp(C, F).
Suggested replacement
But this contradicts our hypothesis that Transp(C′, H). Thus Transp(C, (G or H)), i.e. Transp(C, F).
What the paper does, and why it fails
This is the last sentence of the converse direction of case (e)(i) (bottom of p. 341); the similar sentence with ‘and’ earlier on the page, in case (d), is correct. Case (e) treats F = (G or H), but its last sentence concludes Transp(C, (G and H)), a copy of the last sentence of case (d).
What the change does
The conclusion now matches the formula F = (G or H) of case (e), as the following ‘i.e. Transp(C, F)’ requires.
Anything else affected?No other change: purely notational; Theorem 1 is proved in Lean (transp_disj, theorem1_i).
Text note: Wording is verbatim; symbols lost in the text extraction (⊨, ⊭, ⇔, superscripts, underlining, Greek letters, primes) were restored from the PDF.
theorem transp_disj (S : Sys W L) (C : WSet W) (G H : Fm L) :
S.Transp C (.disj G H) ↔ S.Transp C G ∧ S.Transp (fun w => C w ∧ S.eval G w = false) H := byconstructor
· intro h
constructor
· intro π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.disjL π H) l (bysimp [Ctx.plug, hπ]) (.disjL π' S.bot)
⟨π', S.bot, Or.inr rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug, S.bot_false] using this
· intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
have := h (.disjR G π) l (bysimp [Ctx.plug, hπ]) (.disjR G π')
⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
simpa [Ctx.plug, hwG] using this
· intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case disjL π1 r =>
...
theorem theorem1_i (C : WSet W) (F : PFm ι) :
(sys v i0).Transp C F ↔ (sys v i0).Def F C :=
Sys.transp_iff_def _ (leaf_transp_iff_def v i0) F C
Q4btypo Proof of Theorem 2, case (f): ‘this entails that’ must be followed by ‘not’
Location: Section 5.3, proof of Theorem 2, case (f), p. 351 PDF p.27
Paper text
By the Transparency Lemma (part (b)), this entails that Transp(C′, (if G. H)).
Suggested replacement
By the Transparency Lemma (part (b)), this entails that not Transp(C′, (if G. H)).
What the paper does, and why it fails
In case (f) the proof has just shown that not Transp(C′, G) and must conclude that not Transp(C′, (if G. H)), as in cases (d) and (e). As printed, it concludes the opposite, Transp(C′, (if G. H)).
What the change does
The sentence now draws the negative conclusion that the argument needs (the contrapositive of Transparency Lemma (b)).
Anything else affected?No other change: the case is used correctly in the rest of the proof; it is formalized as transp_cond and theorem2.
Text note: Wording is verbatim; symbols lost in the text extraction (⊨, ⊭, ⇔, superscripts, underlining, Greek letters, primes) were restored from the PDF.
theorem transp_cond (S : Sys W L) (C : WSet W) (G H : Fm L) :
S.Transp C (.cond G H) ↔ S.Transp C G ∧ S.Transp (S.TS G C) H := byconstructor
· intro h
constructor
· intro π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.condL π H) l (bysimp [Ctx.plug, hπ]) (.condL π' S.bot)
⟨π', S.bot, rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug, S.bot_false] using this
· intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
have := h (.condR G π) l (bysimp [Ctx.plug, hπ]) (.condR G π')
⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
simpa [Ctx.plug, hwG] using this
· intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case condL π1 r =>
...
theorem theorem2 (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) :
∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') := byintro C' F' hacc
refine ⟨?_, fun hd => (sys M).upd_eq_TS F' C' hd⟩
refine (sys M).lift (C₀ := C) (F₀ := F) ?_ F' C' hacc
intro C'' l hl
have hNT' := (sys M).lemma2 hNT hl
obtain ⟨hsub, hleaf⟩ := hl.sub
rw [Sys.transp_leaf]
cases l with
| atom i => simp [sys]
| trig a b =>
simp only [sys]
...
Paper text (symbols restored from the PDF)Theorem 1 Consider the propositional fragment of the language defined above. For any formula F and for any C ⊆ W: (i) Transp(C, F) iff C[F] ≠ #.
Statementfor every F and every C ⊆ W (language containing ⊤,⊥): Transp(C,F) ↔ C[F] ≠ #
Lean statementtheorem1_i : (sys v i0).Transp C F ↔ (sys v i0).Def F C and, with literal strings, theorem1_i_strings : StrTransp C F ↔ Def F C
theorem theorem1_i_strings (C : WSet W) (F : PFm ι) :
(sys v i0).StrTransp C F ↔ (sys v i0).Def F C :=
((sys v i0).strTransp_iff_transp C F).trans (theorem1_i v i0 C F)
Minor typo: typo in proof case (e)(i): conclusion should be Transp(C,(G or H))
Q4atypo Proof of Theorem 1, case (e)(i): the conclusion should be Transp(C, (G or H)) (details above)
Paper text (symbols restored from the PDF)Theorem 1 Consider the propositional fragment of the language defined above. For any formula F and for any C ⊆ W: [...] (ii) If C[F] ≠ #, C[F] = {w ∈ C: w ⊨ F}.
/-- **Theorem 1 (ii)**: if `C[F] ≠ #` then `C[F] = {w ∈ C : w ⊨ F}`. -/theorem theorem1_ii (C : WSet W) (F : PFm ι) (h : (sys v i0).Def F C) :
(sys v i0).Upd F C = (sys v i0).TS F C :=
Sys.upd_eq_TS _ F C h
theorem upd_eq_TS (S : Sys W L) : ∀ (F : Fm L) (C : WSet W), Def S F C → Upd S F C = TS S F C := byintro F
induction F with
| leaf l =>
intro C h
exact S.lupd_static l C h
| neg F ih =>
intro C h
have h1 := ih C h
funext w
apply propext
simp only [Upd, h1, TS, eval_neg]
cases S.eval F w <;> simp
| conj F G ihF ihG =>
intro C ⟨h1, h2⟩
have e1 := ihF C h1
simp only [Upd] at *
rw [e1] at h2 ⊢
rw [ihG _ h2]
funext w
apply propext
simp only [TS, eval_conj]
cases S.eval F w <;> cases S.eval G w <;> simp
| disj F G ihF ihG =>
...
Paper text (symbols restored from the PDF)Heim’s claim is that for any generalized quantifier Q, (i) (Q P̲P′.R) presupposes that every individual in the domain satisfies P, and (ii) (Q P. R̲R′) presupposes that every individual in the domain that satisfies P also satisfies R.
/-- (i) `(Q P̲P' . R)` presupposes that every individual satisfies `P`. -/theorem heim_claim_i (k j : ρ) (R : Pred ρ) (C : WSet W) :
M.qdef (.trig k j) R C ↔ (∀ w, C w → ∀ d, d < M.n → M.I k w d = true) ∧
(∀ w, C w → ∀ d, d < M.n → M.pstat (.trig k j) w d = true → M.ppre R w d = true) := bysimp [QModel.qdef, QModel.ppre]
/-- (ii) `(Q P . R̲R')` presupposes that every individual satisfying `P` satisfies `R`. -/theorem heim_claim_ii (P : Pred ρ) (k j : ρ) (C : WSet W) (hP : ∀ w d, M.ppre P w d = true) :
M.qdef P (.trig k j) C ↔ ∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true := byconstructor
· rintro ⟨-, h⟩; exact h
· intro h
exact ⟨fun w _ d _ => hP w d, h⟩
theorem qdef_both (k j k' j' : ρ) (C : WSet W) :
M.qdef (.trig k j) (.trig k' j') C ↔
(∀ w, C w → ∀ d, d < M.n → M.I k w d = true) ∧
(∀ w, C w → ∀ d, d < M.n → (M.I k w d && M.I j w d) = true → M.I k' w d = true) := bysimp [QModel.qdef, QModel.ppre, QModel.pstat]
Minor typo: case (g): P used both for presupposition P and whole restrictor
Q5typo Theorem 2, case (g): P is used both for the presupposition P and for the whole restrictor
Location: Section 5.3, Theorem 2, case (g), p. 351-352 PDF p.27
Paper text
1. If Transp(C′, F′), then C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [P(d) ⇒ R(d)] (as in Lemma 1).
Suggested replacement (Theorem 2, case (g), Part (i), item 1)
1. If Transp(C′, F′), then C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [(P and P′)(d) ⇒ R(d)] (as in Lemma 1).
Paper text
2. If C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [P(d) ⇒ R(d)], then Transp(C′, F′) (immediate).
Suggested replacement (Theorem 2, case (g), Part (i), item 2)
2. If C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [(P and P′)(d) ⇒ R(d)], then Transp(C′, F′) (immediate).
Paper text
because C′[F′] ≠ #, and thus C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [P(d) ⇒ R(d)]
Suggested replacement (Theorem 2, case (g), Part (ii), last line)
because C′[F′] ≠ #, and thus C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [(P and P′)(d) ⇒ R(d)]
What the paper does, and why it fails
For F′ = (Qi P̲P′. R̲R′), ‘P’ means the presupposition of the restrictor in ∀d P(d), but in ∀d [P(d) ⇒ R(d)] (case (b)) it means the whole restrictor. Read with P the presupposition, the second condition is too strong: together with ∀d P(d) it would say ∀d R(d).
What the change does
The second condition is now Heim’s (21): every individual satisfying both the presupposition and the assertion of the restrictor, (P and P′)(d), satisfies R. This is the condition proved in Lean (qdef_both, lemma1_ii).
Anything else affected?No other change: the correct condition is what is proved and used; Theorem 2 is unaffected. Case (b) just above (‘the size of the extension of P is constant’) can stay: there P is the whole restrictor.
Text note: In the paper P̲ and R̲ are underlined presupposition triggers; underlining is not reproduced here.
theorem qdef_both (k j k' j' : ρ) (C : WSet W) :
M.qdef (.trig k j) (.trig k' j') C ↔
(∀ w, C w → ∀ d, d < M.n → M.I k w d = true) ∧
(∀ w, C w → ∀ d, d < M.n → (M.I k w d && M.I j w d) = true → M.I k' w d = true) := bysimp [QModel.qdef, QModel.ppre, QModel.pstat]
theorem lemma1_ii (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ) (P : Pred ρ) (p : Nat)
(hp : ∀ w, C w → cnt M.n (M.pstat P w) = p)
(hline : ∃ b₁ b₂, b₁ ≤ p ∧ b₂ ≤ p ∧ M.f q (p - b₁) b₁ ≠ M.f q (p - b₂) b₂) :
ST M C q P k ↔ ∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.pstat P w d = true ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd hPd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hPd, hd'⟩
...
Paper text (symbols restored from the PDF)Consider the following scenario: -In w, there are exactly 2 P-individuals, one of whom satisfies R and one of whom doesn’t. -The sentence uttered is (Q P.R̲R′) with Q = less than three. Even though it is not the case that each P-individual satisfies R in w, Transparency is trivially satisfied with respect to w because for any predicative expression γ, w ⊨ (Q P. (R and γ)) ⇔ (Q P. γ)
Statement2 P-individuals, Q = less than three: Transp holds trivially, Heim's presupposition fails, NT violated
Lean statementless_than_three_scenario (model expressive, restrictor size constant = 2); not_nt_of_lt3 (general: all worlds <3 P-individuals ⇒ NT fails)
Paper text (symbols restored from the PDF)Suppose that C = {w, w′, w″}, where w is the world mentioned earlier in which there are exactly two P-individuals, while w′ and w″ are worlds that have exactly four P-individuals [...] Consider the sentence (Q P.R̲R′). As before, Transparency is satisfied in w [...]. Furthermore, Transparency is also satisfied in w′ and w″ because in these worlds each P-individual satisfies R. Contrary to the case we considered in (i), however, this situation is not ruled out by Non-Triviality:
StatementC={w,w',w''}, restrictor sizes 2,4,4: NT and Transp hold but Heim fails
Lean statementconstancy_needed (NT ∧ Transp ∧ ¬qdef ∧ ¬∃p constant, expressive model, any Y)
Paper text (symbols restored from the PDF)(29) Non-Triviality Corollary Let Q_i be a generalized quantifier with the associated tree of numbers f_i. Consider a formula (Q_i G.H) evaluated in a Context Set C. Then: (i) If <C, (Q_i G . H)> satisfies Non-Triviality and if in C the domain of individuals is of constant finite size n, [...] {f_i(a, b): a, b ∈ ℕ and a+b ≤ n} = {0, 1}, (ii) If <C, (Q_i G . H)> satisfies Non-Triviality and if in C the extension of G is of constant finite size g, {f_i(a, b): a, b ∈ ℕ and a+b = g} = {0, 1}.
StatementNT (+ constant domain size n) ⇒ f not constant on {a+b ≤ n}; NT (+ constant restrictor size p) ⇒ not constant on {a+b = p}
theorem nt_corollary_i {C : WSet W} {q : κ} {P R : Pred ρ}
(h : (sys M).NT IsQ C (.leaf (.quant q P R))) :
∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b' := byobtain ⟨w₁, w₂, -, -, h1, h2⟩ := nt_leaf_values M h
refine ⟨cnt M.n (fun d => M.pstat P w₁ d && !M.pstat R w₁ d),
cnt M.n (fun d => M.pstat P w₁ d && M.pstat R w₁ d),
cnt M.n (fun d => M.pstat P w₂ d && !M.pstat R w₂ d),
cnt M.n (fun d => M.pstat P w₂ d && M.pstat R w₂ d), ?_, ?_, ?_⟩
· rw [qsem_args_le M P R w₁]; exact cnt_le _ _
· rw [qsem_args_le M P R w₂]; exact cnt_le _ _
· simp only [QModel.qsem] at h1 h2
rw [h1, h2]; simp
theorem nt_corollary_ii {C : WSet W} {q : κ} {P R : Pred ρ} {p : Nat}
(h : (sys M).NT IsQ C (.leaf (.quant q P R))) (hp : ∀ w, C w → cnt M.n (M.pstat P w) = p) :
∃ b₁ b₂, b₁ ≤ p ∧ b₂ ≤ p ∧ M.f q (p - b₁) b₁ ≠ M.f q (p - b₂) b₂ := byobtain ⟨w₁, w₂, hw₁, hw₂, h1, h2⟩ := nt_leaf_values M h
have e1 := qsem_args_le M P R w₁
have e2 := qsem_args_le M P R w₂
rw [hp w₁ hw₁] at e1
rw [hp w₂ hw₂] at e2
refine ⟨cnt M.n (fun d => M.pstat P w₁ d && M.pstat R w₁ d),
cnt M.n (fun d => M.pstat P w₂ d && M.pstat R w₂ d), byomega, byomega, ?_⟩
simp only [QModel.qsem] at h1 h2
have a1 : p - cnt M.n (fun d => M.pstat P w₁ d && M.pstat R w₁ d) =
cnt M.n (fun d => M.pstat P w₁ d && !M.pstat R w₁ d) := byomegahave a2 : p - cnt M.n (fun d => M.pstat P w₂ d && M.pstat R w₂ d) =
cnt M.n (fun d => M.pstat P w₂ d && !M.pstat R w₂ d) := byomegarw [a1, a2, h1, h2]
simp
Paper text (symbols restored from the PDF)Consider the sentence (Q P.R̲R′) with Q = infinitely many. We claim that as long as P^w−R^w is finite, any world w guarantees that for any predicative expression γ and for any sentence completion β, (i) w ⊨ (Q P. (R and γ)) β ⇔ (Q P. γβ
Statementif P^w − R^w is finite then (Q P.(R and γ)) ⇔ (Q P.γ) at w for all γ
/-- **Footnote 12, sufficiency**: if `P^w ∖ R^w` is finite, Transparency holds at `w`. -/theorem transpInf_of_finite (P R : D → Prop) (h : Fin' (fun d => P d ∧ ¬ R d)) : TranspInf P R := byintro γ
constructor
· intro hi l
obtain ⟨x, hx, hxl⟩ := hi l
exact ⟨x, ⟨hx.1, hx.2.2⟩, hxl⟩
· intro hi l
obtain ⟨l0, hl0⟩ := h
obtain ⟨x, hx, hxl⟩ := hi (l ++ l0)
have hxR : R x := byapply Classical.byContradiction
intro hR
exact hxl (List.mem_append_right _ (hl0 x ⟨hx.1, hR⟩))
exact ⟨x, ⟨hx.1, hxR, hx.2⟩, fun hm => hxl (List.mem_append_left _ hm)⟩
theorem not_transpInf_of_infinite (P R : D → Prop) (h : ¬ Fin' (fun d => P d ∧ ¬ R d)) :
¬ TranspInf P R := byintro ht
have h1 := (ht (fun d => ¬ R d)).2have hinf : Inf (fun d => P d ∧ ¬ R d) := byintro l
apply Classical.byContradiction
intro hn
apply h
exact ⟨l, fun x hx => Classical.byContradiction fun hxl => hn ⟨x, hx, hxl⟩⟩
have := h1 hinf []
obtain ⟨x, ⟨_, hR, hnR⟩, _⟩ := this
exact hnR hR
theorem transpInf_iff (P R : D → Prop) : TranspInf P R ↔ Fin' (fun d => P d ∧ ¬ R d) :=
⟨fun h => Classical.byContradiction fun hn => not_transpInf_of_infinite P R hn h,
transpInf_of_finite P R⟩
N2note Note (footnote 12): finiteness of Pw − Rw is exactly the condition for infinitely many
We claim that as long as Pw −Rw is finite, any world w guarantees that for any predicative expression γ and for any sentence completion β,
Suggested replacement (optional sentence at the end of footnote 12, after ‘This proves the right-to-left direction.’)
(delete)
Paper text
(insert)
Suggested replacement (optional; optional sentence at the end of footnote 12, after ‘This proves the right-to-left direction.’)
(The converse also holds: if Pw −Rw is infinite, there is a predicative expression γ for which (i) fails at w. So finiteness of Pw −Rw is exactly the condition for (i).)
What the paper does, and why it fails
Footnote 12 proves only the ‘if’ direction: if Pw − Rw is finite then (i) holds for all γ. It does not say what happens when Pw − Rw is infinite.
What the change does
No edit is needed. The optional sentence adds the converse, which is proved in Lean (transpInf_iff, not_transpInf_of_infinite).
Anything else affected?No other change: consistent with footnote 16 (Lean: footnote16); the finite-domain results are unchanged.
theorem transpInf_iff (P R : D → Prop) : TranspInf P R ↔ Fin' (fun d => P d ∧ ¬ R d) :=
⟨fun h => Classical.byContradiction fun hn => not_transpInf_of_infinite P R hn h,
transpInf_of_finite P R⟩
/-- **Footnote 12, sufficiency**: if `P^w ∖ R^w` is finite, Transparency holds at `w`. -/theorem transpInf_of_finite (P R : D → Prop) (h : Fin' (fun d => P d ∧ ¬ R d)) : TranspInf P R := byintro γ
constructor
· intro hi l
obtain ⟨x, hx, hxl⟩ := hi l
exact ⟨x, ⟨hx.1, hx.2.2⟩, hxl⟩
· intro hi l
obtain ⟨l0, hl0⟩ := h
obtain ⟨x, hx, hxl⟩ := hi (l ++ l0)
have hxR : R x := byapply Classical.byContradiction
intro hR
exact hxl (List.mem_append_right _ (hl0 x ⟨hx.1, hR⟩))
exact ⟨x, ⟨hx.1, hxR, hx.2⟩, fun hm => hxl (List.mem_append_left _ hm)⟩
theorem not_transpInf_of_infinite (P R : D → Prop) (h : ¬ Fin' (fun d => P d ∧ ¬ R d)) :
¬ TranspInf P R := byintro ht
have h1 := (ht (fun d => ¬ R d)).2have hinf : Inf (fun d => P d ∧ ¬ R d) := byintro l
apply Classical.byContradiction
intro hn
apply h
exact ⟨l, fun x hx => Classical.byContradiction fun hxl => hn ⟨x, hx, hxl⟩⟩
have := h1 hinf []
obtain ⟨x, ⟨_, hR, hnR⟩, _⟩ := this
exact hnR hR
Paper text(i) Infinitely many integers are unaware that they are lucky not to be the number 13. Heim’s theory predicts that the integers that are quantified over are all different from 13 (because all integers must satisfy the presupposition introduced by the nuclear scope unaware that. . .). We predict no such thing. [...] As it happens, in any world w, P^w−Q^w is a singleton, and it is thus a finite set. This predicts that Transparency should automatically be satisfied.
Not stated in the paper as such — related passage (symbols restored from the PDF)
Related passage in the paper—In both cases, we construct X^w by taking the union of (1) (a+b−1) elements of P^w, together with (2) one element of D^w − P^w — which is possible since by assumption w ⊨ ∃d (not P(d)). —In Case (i), we construct Y^w by taking b elements from (1).
Statementsubsets with prescribed intersection sizes exist
theorem realize_four (n : Nat) (P : Nat → Bool) (s₁ s₂ c₁ c₂ : Nat)
(hs : s₁ + s₂ ≤ cnt n P) (hc : c₁ + c₂ ≤ n - cnt n P) :
∃ X Y : Nat → Bool,
cnt n (fun x => P x && X x && !Y x) = s₁ ∧ cnt n (fun x => P x && X x && Y x) = s₂ ∧
cnt n (fun x => !P x && X x && !Y x) = c₁ ∧ cnt n (fun x => !P x && X x && Y x) = c₂ := bylet N : Nat → Bool := fun x => !P x
have hcomp : cnt n P + cnt n N = n := cnt_compl n P
let X : Nat → Bool := fun x => piece P 0 (s₁ + s₂) x || piece N 0 (c₁ + c₂) x
have hXP : ∀ x, (P x && X x) = piece P 0 (s₁ + s₂) x := byintro x
by_cases hp : P x = true
· have : piece N 0 (c₁ + c₂) x = false := bycases h : piece N 0 (c₁ + c₂) x
· rfl
· have := piece_sub N 0 _ x h; simp [N, hp] at this
simp [X, hp, this]
· have h1 : piece P 0 (s₁ + s₂) x = false := bycases h : piece P 0 (s₁ + s₂) x
· rfl
· have := piece_sub P 0 _ x h; simp_allsimp [hp, h1]
have hXN : ∀ x, (N x && X x) = piece N 0 (c₁ + c₂) x := byintro x
by_cases hp : P x = true
...
/-- Choose `Y` meeting two *disjoint* sets `U`, `V` in prescribed numbers of elements. -/theorem realize_two (n : Nat) (U V : Nat → Bool) (hd : ∀ x, ¬ (U x = true ∧ V x = true))
(u v : Nat) (hu : u ≤ cnt n U) (hv : v ≤ cnt n V) :
∃ Y : Nat → Bool, cnt n (fun x => U x && Y x) = u ∧ cnt n (fun x => V x && Y x) = v := byrefine ⟨fun x => piece U 0 u x || piece V 0 v x, ?_, ?_⟩
· have : cnt n (fun x => U x && (piece U 0 u x || piece V 0 v x)) = cnt n (piece U 0 u) := byapply cnt_congr; intro x _
have := hd x
by_cases hU : U x = true
· have hV : V x = false := by simpa [hU] using this
have : piece V 0 v x = false := bycases h : piece V 0 v x
· rfl
· have := piece_sub V 0 v x h; simp_allsimp [this, hU]
· simp [hU]
have := piece_sub U 0 u x
cases h : piece U 0 u x
· rfl
· simp_allrw [this, cnt_piece U 0 u (byomega)]
omega
· have : cnt n (fun x => V x && (piece U 0 u x || piece V 0 v x)) = cnt n (piece V 0 v) := byapply cnt_congr; intro x _
...
/-- Choose a subset of `S` (a set of individuals) of any size `k ≤ |S|`. -/theorem exists_subset (n : Nat) (S : Nat → Bool) (k : Nat) (hk : k ≤ cnt n S) :
∃ T : Nat → Bool, (∀ x, T x = true → S x = true) ∧ cnt n T = k := byrefine ⟨piece S 0 k, piece_sub S 0 k, ?_⟩
rw [cnt_piece S 0 k (byomega)]
omega
Paper text (symbols restored from the PDF)Lemma 1 Let Q_i be a generalized quantifier with the associated tree of numbers f_i. (i) Suppose that (a) throughout C, the domain of individuals is of constant finite size n, (b) any property over the domain can be expressed by some predicate, and (c) {f_i(a, b): a, b ∈ ℕ and a+b ≤ n} = {0, 1}. Then Transp(C, (Q_i P̲P′. R)) iff C ⊨ ∀d P(d).
Statementdomain constant size n, every property expressible, f non-constant on {a+b ≤ n} ⇒ Transp(C,(Q P̲P'.R)) ↔ C ⊨ ∀d P(d)
Lean statementlemma1_i : M.Expressive → (∃ a b a' b', a+b ≤ n ∧ a'+b' ≤ n ∧ f a b ≠ f a' b') → (RT M C q k ↔ ∀w∈C ∀d<n, I k w d)
Lean: Lemma1.lean:102 · proven-corrected (statement true; Case 2/Zone B of the paper's proof has a gap: Q2, repaired in find_step)
theorem lemma1_i (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ)
(htri : ∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b') :
RT M C q k ↔ ∀ w, C w → ∀ d, d < M.n → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
-- a world `w ∈ C` and an individual `d0 < n` with `¬ P(d0)`have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hd'⟩
obtain ⟨w, hw, d0, hd0, hP0⟩ := this
have hkn : cnt M.n (M.I k w) < M.n := byhave h1 := cnt_compl M.n (M.I k w)
have h2 : 0 < cnt M.n (fun x => !M.I k w x) :=
cnt_pos (fun x => !M.I k w x) hd0 (by simpa using hP0)
omegaobtain ⟨a, b, i, j, hia, hjb, hab, hij, hfne⟩ :=
find_step (M.f q) M.n (cnt M.n (M.I k w)) hkn htri
...
Q2proof gap Lemma 1(i), Case 2, Zone B: the ‘horizontal projection’ can fail; project along any step instead
Location: Section 5.2, Lemma 1(i), Case 2, p. 347 PDF p.23
Paper text
-If (a*, b*) is in Zone B, there is a point of the line a + b = |Pw| withthesamea-coordinateas(a*,b*)(this is the horizontal projection of (a*, b*) onto the line). Thus forsomec satisfying 0 < c ≤ |Dw−Pw|, fi(a*, b* − c) ≠ fi(a*, b*).
Suggested replacement (Lemma 1(i), Case 2, Zone B, first two sentences)
-If (a*, b*) is in Zone B, let c = a* + b* − |Pw| (so 0 < c ≤ |Dw−Pw|), and choose integers i, j with i ≥ 0, j ≥ 0, i + j = c, i ≤ a* and j ≤ b* (this is possible because a* + b* ≥ c). Then (a* − i, b* − j) is a point of the line a + b = |Pw| (if a* ≤ |Pw| one can take i = 0, which is the horizontal projection of (a*, b*) onto the line). Thus fi(a* − i, b* − j) ≠ fi(a*, b*).
Paper text
(1) (a* + b* − c) elements from Pw (thisispossiblebecause(a*,b*)isin Zone B, and thus b* − c ≥0), and
Suggested replacement (Lemma 1(i), Case 2, Zone B, construction of Xw)
(1) (a* + b* − c) elements from Pw (that is, all of Pw, since a* + b* − c = |Pw|), and
Paper text
We construct Yw by taking the union of (b* − c) elements from (1) and all c elements from (2). By construction, |(Xw ∩ Pw)−Yw| = a*, |Xw−Yw| = a*, |(Xw ∩ Pw) ∩ Yw| = b* − c, and |Xw ∩ Yw| = b*.
Suggested replacement (Lemma 1(i), Case 2, Zone B, construction of Yw and the four counts)
We construct Yw by taking the union of (b* − j) elements from (1) and j elements from (2). By construction, |(Xw ∩ Pw)−Yw| = a* − i, |Xw−Yw| = a*, |(Xw ∩ Pw) ∩ Yw| = b* − j, and |Xw ∩ Yw| = b*.
What the paper does, and why it fails
In Zone B (b* > |Pw|) the paper moves (a*, b*) horizontally to the line a + b = |Pw|, which needs a* ≤ |Pw|. If also a* > |Pw|, the horizontal move overshoots the line, and the claim ‘fi(a*, b* − c) ≠ fi(a*, b*)’ can be false. Example: |Pw| = 2, n = 8, f(a, b) = 1 iff a + b > 2, point (3, 3): no such c exists.
What the change does
The point is now reached by any combination of a horizontal step j and a vertical step i totalling c, which always exists. The construction of Xw and Yw is the same except that Yw takes b* − j elements from Pw and j from Dw−Pw, and the four counts are adjusted accordingly; Transparency is still falsified at w. Lemma 1(i) is proved in Lean with this repair (find_step, zoneB_repaired, lemma1_i).
Anything else affected?No other change: Lemma 1(i) is true as stated; Theorem 2 (case g) and the Remark after Lemma 1 are unaffected. The step for Case 1 needs the small-triangle correction of Q3.
Text note: The four counts at the end of the last edit are restored from the PDF (page 347); the text extraction loses the ‘| … | = ’ symbols.
Judgment call: the wording of this replacement is ours and not checked in Lean. The parametrisation by (i, j) is our presentation of the Lean repair (find_step); the Lean development proves the existence of a suitable step, not this exact wording.
theorem paper_zoneB_step_fails :
let f : Nat → Nat → Bool := fun a b => decide (2 < a + b)
f 33 ≠ f 00 ∧ (∀ a b, a + b ≤ 2 → f a b = f 00) ∧
¬ ∃ c, 0 < c ∧ c ≤ 3 ∧ c ≤ 8 - 2 ∧ f 3 (3 - c) ≠ f 33 := byintro f
refine ⟨bydecide, ?_, ?_⟩
· intro a b h; simp [f]; omega
· rintro ⟨c, h1, h2, h3, h4⟩
apply h4
simp only [f]
have : 2 < 3 + (3 - c) := byomegasimp [this]
theorem find_step (f : Nat → Nat → Bool) (n k : Nat) (hk : k < n)
(htri : ∃ a b a' b', a + b ≤ n ∧ a' + b' ≤ n ∧ f a b ≠ f a' b') :
∃ a b i j, i ≤ a ∧ j ≤ b ∧ a + b - (i + j) ≤ k ∧ i + j ≤ n - k ∧
f (a - i) (b - j) ≠ f a b := by
by_cases hA : ∃ a b, a + b ≤ k ∧ ((1 ≤ a ∧ f (a-1) b ≠ f a b) ∨ (1 ≤ b ∧ f a (b-1) ≠ f a b))
· -- Case 1 of the paper: a local step inside the small triangleobtain ⟨a, b, hab, h | h⟩ := hA
· exact ⟨a, b, 1, 0, h.1, byomega, byomega, byomega, by simpa using h.2⟩
· exact ⟨a, b, 0, 1, byomega, h.1, byomega, byomega, by simpa using h.2⟩
· -- Case 2: constant on the small trianglehave hc := const_of_no_step f k (fun a b hab =>
⟨fun h1 => Classical.byContradiction fun hne => hA ⟨a, b, hab, Or.inl ⟨h1, hne⟩⟩,
fun h1 => Classical.byContradiction fun hne => hA ⟨a, b, hab, Or.inr ⟨h1, hne⟩⟩⟩)
obtain ⟨a1, b1, a2, b2, h1, h2, hne⟩ := htri
have : ∃ a b, a + b ≤ n ∧ f a b ≠ f 00 := by
by_cases e : f a1 b1 = f 00
...
/-- ... while the corrected argument (`find_step`) does find a refuting pair for that `f`. -/theorem zoneB_repaired :
∃ a b i j, i ≤ a ∧ j ≤ b ∧ a + b - (i + j) ≤ 2 ∧ i + j ≤ 8 - 2 ∧
(fun a b => decide (2 < a + b)) (a - i) (b - j) ≠ (fun a b => decide (2 < a + b)) a b :=
find_step (fun a b => decide (2 < a + b)) 82 (byomega) ⟨0, 0, 3, 3, byomega, byomega, bydecide⟩
theorem lemma1_i (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ)
(htri : ∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b') :
RT M C q k ↔ ∀ w, C w → ∀ d, d < M.n → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
-- a world `w ∈ C` and an individual `d0 < n` with `¬ P(d0)`have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hd'⟩
...
Q3typo Lemma 1(i), Case 1: the bound a+b ≤ n should be a+b ≤ |Pw|
Location: Section 5.2, Lemma 1(i), Case 1, p. 346 PDF p.22
Paper text
(i) for some (a, b) for which a+b ≤ n with a ≥ 1, fi(a − 1, b) ≠ fi(a, b), or (ii) for some (a, b) for which a+b ≤ n with b ≥ 1, fi(a, b − 1) ≠ fi(a, b)
Suggested replacement
(i) for some (a, b) for which a+b ≤ |Pw| with a ≥ 1, fi(a − 1, b) ≠ fi(a, b), or (ii) for some (a, b) for which a+b ≤ |Pw| with b ≥ 1, fi(a, b − 1) ≠ fi(a, b)
What the paper does, and why it fails
Case 1 assumes that fi is not constant on the smaller triangle (a+b ≤ |Pw|), and the argument that follows (negating (i) and (ii) would make fi constant on that triangle) is about that triangle. But (i) and (ii) are stated for points with a+b ≤ n, the larger triangle, which does not match, and the construction takes a+b−1 elements from Pw, which needs a+b ≤ |Pw|.
What the change does
The change points in (i) and (ii) are now found inside the smaller triangle, as in the sentence that justifies the claim and as the construction of Xw and Yw requires.
Anything else affected?No other change: this is what the proof actually uses, and Lemma 1(i) is proved in Lean (lemma1_i).
Text note: Wording is verbatim; symbols lost in the text extraction (⊨, ⊭, ⇔, superscripts, underlining, Greek letters, primes) were restored from the PDF.
theorem lemma1_i (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ)
(htri : ∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b') :
RT M C q k ↔ ∀ w, C w → ∀ d, d < M.n → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
-- a world `w ∈ C` and an individual `d0 < n` with `¬ P(d0)`have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hd'⟩
...
N1note Note: the Constancy and Non-Triviality hypotheses of Theorem 2 could be weakened
Suppose that (i) the domain of individuals is of constant finite size over C, and (ii) the extension of each restrictor that appears in F is of constant size over C, and (iii) <C, F> satisfies Non-Triviality
Suggested replacement (optional remark after the statement of Theorem 2)
(delete)
Paper text
(insert)
Suggested replacement (optional; optional remark after the statement of Theorem 2)
Remark. Hypothesis (ii) is only used for clauses whose nuclear scope carries a presupposition trigger (Lemma 1(ii)); Lemma 1(i) needs only Non-Triviality and constant domain size. Non-Triviality is only used for the clauses actually involved.
What the paper does, and why it fails
Theorem 2 assumes constant restrictor sizes and Non-Triviality for the whole formula, although the proof uses them clause by clause.
What the change does
No edit is needed. The optional remark records that the theorem could be sharpened.
Anything else affected?No other change: it is an observation about the structure of the proof (Lemma 1(i) versus 1(ii)); no claim of the paper changes.
theorem lemma1_i (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ)
(htri : ∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b') :
RT M C q k ↔ ∀ w, C w → ∀ d, d < M.n → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
-- a world `w ∈ C` and an individual `d0 < n` with `¬ P(d0)`have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hd'⟩
...
theorem lemma1_ii (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ) (P : Pred ρ) (p : Nat)
(hp : ∀ w, C w → cnt M.n (M.pstat P w) = p)
(hline : ∃ b₁ b₂, b₁ ≤ p ∧ b₂ ≤ p ∧ M.f q (p - b₁) b₁ ≠ M.f q (p - b₂) b₂) :
ST M C q P k ↔ ∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.pstat P w d = true ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd hPd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hPd, hd'⟩
...
Paper text (symbols restored from the PDF)Lemma 1 Let Q_i be a generalized quantifier with the associated tree of numbers f_i. [...] (ii) Suppose that (a) throughout C, the extension of P is of constant finite size p, (b) any property over the domain can be expressed by some predicate, and (c) {f_i(a, b): a, b ∈ ℕ and a+b = p} = {0, 1}. Then Transp(C, (Q_i P . R̲R′)) iff C ⊨ ∀d [P(d) ⇒ R(d)].
Statementrestrictor of constant size p, every property expressible, f non-constant on {a+b = p} ⇒ Transp(C,(Q P.R̲R')) ↔ C ⊨ ∀d[P(d)⇒R(d)]
Lean statementlemma1_ii (restrictor P may itself carry underlined material; P(d) = its static value)
theorem lemma1_ii (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ) (P : Pred ρ) (p : Nat)
(hp : ∀ w, C w → cnt M.n (M.pstat P w) = p)
(hline : ∃ b₁ b₂, b₁ ≤ p ∧ b₂ ≤ p ∧ M.f q (p - b₁) b₁ ≠ M.f q (p - b₂) b₂) :
ST M C q P k ↔ ∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.pstat P w d = true ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd hPd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hPd, hd'⟩
obtain ⟨w, hw, d0, hd0, hPd0, hRd0⟩ := this
have hpw := hp w hw
-- b = |P ∩ R| < phave hsplit : cnt M.n (M.pstat P w) =
cnt M.n (fun d => M.pstat P w d && M.I k w d) +
cnt M.n (fun d => M.pstat P w d && !M.I k w d) := cnt_split M.n (M.pstat P w) (M.I k w)
have hpos : 0 < cnt M.n (fun d => M.pstat P w d && !M.I k w d) :=
cnt_pos (fun d => M.pstat P w d && !M.I k w d) hd0 (bysimp [hPd0]; simpa using hRd0)
...
Minor typo: case (g): P used for both presupposition and restrictor
Q5typo Theorem 2, case (g): P is used both for the presupposition P and for the whole restrictor (details above)
N1note Note: the Constancy and Non-Triviality hypotheses of Theorem 2 could be weakened (details above)
Paper text (symbols restored from the PDF)Lemma 2 Suppose that <C, F> satisfies Non-Triviality. Then if <C′, F′> is accessed by <C, F>, <C′, F′> satisfies Non-Triviality as well.
StatementNT is inherited by all pairs accessed by ⟨C,F⟩
Lean statementAccessed; Sys.lemma2 : NT C₀ F₀ → Accessed C₀ F₀ C F → NT C F
/-- Paper, Section 5.3: `Accessed S C₀ F₀ C F` iff `⟨C, F⟩` is accessed by `⟨C₀, F₀⟩`. -/inductive Accessed (S : Sys W L) (C₀ : WSet W) (F₀ : Fm L) : WSet W → Fm L → Prop
| refl : Accessed S C₀ F₀ C₀ F₀
| neg {C G} : Accessed S C₀ F₀ C (.neg G) → Accessed S C₀ F₀ C G
| conjL {C G H} : Accessed S C₀ F₀ C (.conj G H) → Accessed S C₀ F₀ C G
| conjR {C G H} : Accessed S C₀ F₀ C (.conj G H) → S.Def G C →
Accessed S C₀ F₀ (S.Upd G C) H
| disjL {C G H} : Accessed S C₀ F₀ C (.disj G H) → Accessed S C₀ F₀ C G
| disjR {C G H} : Accessed S C₀ F₀ C (.disj G H) → S.Def G C →
Accessed S C₀ F₀ (fun v => C v ∧ ¬ S.Upd G C v) H
| condL {C G H} : Accessed S C₀ F₀ C (.cond G H) → Accessed S C₀ F₀ C G
| condR {C G H} : Accessed S C₀ F₀ C (.cond G H) → S.Def G C →
Accessed S C₀ F₀ (S.Upd G C) H
theorem lemma2 (S : Sys W L) {q : L → Prop} {C₀ : WSet W} {F₀ : Fm L}
(h0 : S.NT q C₀ F₀) :
∀ {C : WSet W} {F : Fm L}, Accessed S C₀ F₀ C F → S.NT q C F := byintro C F h
induction h with
| refl => exact h0
| neg _ ih => exact nt_neg S ih
| conjL _ ih => exact nt_conjL S ih
| disjL _ ih => exact nt_disjL S ih
| condL _ ih => exact nt_condL S ih
| @conjR C G H _ hd ih =>
have := nt_conjR S ih
rw [← upd_eq_TS S G C hd] at this
exact this
| @condR C G H _ hd ih =>
have := nt_condR S ih
rw [← upd_eq_TS S G C hd] at this
exact this
| @disjR C G H _ hd ih =>
have := nt_disjR S ih
have e' : (fun v => C v ∧ ¬ S.Upd G C v) = (fun w => C w ∧ S.eval G w = false) := byfunext v; apply propext; rw [upd_eq_TS S G C hd]; simp only [TS]; cases S.eval G v <;> simprw [e']
exact this
Minor typo: Lemma 2: justify w in C'[G] using only Heim dynamic semantics (proof gap)
Q6proof gap Lemma 2: justify ‘w ∈ C′[G]’ using only Heim’s dynamic semantics
Location: Section 5.3, Lemma 2, cases (iii)b, (iv)b, (v)b, p. 349-350 PDF p.25
Paper text
It follows that G is true at w (otherwise the left-handside and theright-handsideofthebiconditionalwouldbothbefalse),andby similar reasoning G is true at w′.
Suggested replacement (Lemma 2, case (iii)b, after the sentence below)
Since C′[G] is defined here, C′[G] = {w ∈ C′: w ⊨ G} (this follows from the dynamic semantics in (21) alone, by induction on G, and does not use Transparency or Theorem 2); hence w, w′ ∈ C′[G].
Paper text
It follows that G is true at w (otherwise the left-handside and theright-handsideofthebi-conditionalwouldbothbetrue),andby similar reasoning G is true at w′.
Suggested replacement (Lemma 2, case (v)b, after the sentence below)
Since C′[G] is defined here, C′[G] = {w ∈ C′: w ⊨ G} (this follows from the dynamic semantics in (21) alone, by induction on G, and does not use Transparency or Theorem 2); hence w, w′ ∈ C′[G].
Paper text
It follows that C[(not G)] ⊭ α A γ ⇔ α T γ
Suggested replacement (Lemma 2, case (iv)b, just before the sentence ‘It follows that C[(not G)] ⊭ α A γ ⇔ α T γ …’)
Since C′[(not G)] is defined here, C′[(not G)] = {w ∈ C′: w ⊭ G} (again by the dynamic semantics in (21) alone), so w, w′ ∈ C′[(not G)].
What the paper does, and why it fails
Cases (iii)b, (iv)b and (v)b conclude that C′[G] (or C′[(not G)]) refutes the property of α A because the two worlds w, w′ satisfy G (or not G). This tacitly uses that a world of C′ satisfying G is in C′[G], which is Theorem 2(ii) for G, proved only later. It looks circular.
What the change does
The inserted sentence cites the fact directly: whenever C′[G] is defined, C′[G] = {w ∈ C′: w ⊨ G}. This is a property of Heim’s dynamic semantics alone (Lean: upd_eq_TS, proved independently of Transparency), so there is no circularity.
Anything else affected?No other change: Lemma 2 is proved in Lean using upd_eq_TS; Theorem 2 is unaffected.
Text note: Wording is verbatim; symbols lost in the text extraction (⊨, ⊭, ⇔, superscripts, underlining, Greek letters, primes) were restored from the PDF.
Judgment call: the wording of this replacement is ours and not checked in Lean. The inserted sentences are our wording. The fact they cite (upd_eq_TS) is proved in Lean for the propositional and quantificational clauses; the ‘by induction on G’ is the same induction as for Theorem 1(ii).
theorem upd_eq_TS (S : Sys W L) : ∀ (F : Fm L) (C : WSet W), Def S F C → Upd S F C = TS S F C := byintro F
induction F with
| leaf l =>
intro C h
exact S.lupd_static l C h
| neg F ih =>
intro C h
have h1 := ih C h
funext w
apply propext
simp only [Upd, h1, TS, eval_neg]
cases S.eval F w <;> simp
| conj F G ihF ihG =>
intro C ⟨h1, h2⟩
have e1 := ihF C h1
...
theorem lemma2 (S : Sys W L) {q : L → Prop} {C₀ : WSet W} {F₀ : Fm L}
(h0 : S.NT q C₀ F₀) :
∀ {C : WSet W} {F : Fm L}, Accessed S C₀ F₀ C F → S.NT q C F := byintro C F h
induction h with
| refl => exact h0
| neg _ ih => exact nt_neg S ih
| conjL _ ih => exact nt_conjL S ih
| disjL _ ih => exact nt_disjL S ih
| condL _ ih => exact nt_condL S ih
| @conjR C G H _ hd ih =>
have := nt_conjR S ih
rw [← upd_eq_TS S G C hd] at this
exact this
| @condR C G H _ hd ih =>
have := nt_condR S ih
...
R32confirmed (typo)
Lemma 1 + NT for a clause
Paper: Remark after Lemma 1 / step (g), p.345, 351 PDF p.21
Paper text (symbols restored from the PDF)(g) F′ = (Q_i G. H) Suppose that <C′, F′> is accessed by <C, F>. Since <C, F> satisfies Non-Triviality, by Lemma 2 <C′, F′> does as well. Furthermore, it was shown in Lemma 1 that if <C′, F′> satisfies Non-Triviality, (a) Transp(C′, (Q_i P̲P′. R) ) iff C′ ⊨ ∀d P(d) (b) If the size of the extension of P is constant over C, Transp(C′, (Q_i P . R̲R′)) iff C′ ⊨ ∀ d [P(d) ⇒ R(d)]
Statementunder NT and Constancy, Transp(C,(Q P.R)) ↔ Heim's definedness
theorem quant_leaf (hexp : M.Expressive) (C : WSet W) (q : κ) (P R : Pred ρ)
(hNT : (sys M).NT IsQ C (.leaf (.quant q P R)))
(hconst : ∃ p, ∀ w, C w → cnt M.n (M.pstat P w) = p) :
(sys M).Transp C (.leaf (.quant q P R)) ↔ M.qdef P R C := byobtain ⟨p, hp⟩ := hconst
have htri := nt_corollary_i M hNT
have hline := nt_corollary_ii M hNT hp
rw [transp_quant]
constructor
· rintro ⟨h1, h2⟩
refine ⟨?_, ?_⟩
· intro w hw d hd
cases P with
| plain k => rfl
| conj k j => rfl
| trig k j => exact (lemma1_i M hexp C q k htri).1 (h1 k j rfl) w hw d hd
· intro w hw d hd hPd
cases R with
| plain k => rfl
| conj k j => rfl
| trig k j => exact (lemma1_ii M hexp C q k P p hp hline).1 (h2 k j rfl) w hw d hd hPd
· rintro ⟨d1, d2⟩
refine ⟨?_, ?_⟩
· rintro k j rfl
...
Minor typo: step (g): P used for both presupposition and restrictor
Q5typo Theorem 2, case (g): P is used both for the presupposition P and for the whole restrictor (details above)
Paper text (symbols restored from the PDF)Theorem 2 Let C be a Context Set and let F be a formula. Suppose that (i) the domain of individuals is of constant finite size over C, and (ii) the extension of each restrictor that appears in F is of constant size over C, and (iii) <C, F> satisfies Non-Triviality. Then for every < C′, F′ > which is accessed by <C, F> (including <C, F> itself): (i) Transp(C′, F′) iff C′[F′] ≠ #. (ii) If C′[F′] ≠ #, C′[F′] = {w ∈ C′: w ⊨ F′}.
Statementhypotheses: (i) constant domain size, (ii) constant restrictor sizes, (iii) NT
Counterexamples.lean:179 — lines 179–202 · open file
theorem theorem2_needs_expressiveness :
let M := exprModel
let C : WSet Bool := fun _ => True
let F : Fm (QLeaf Unit (Fin 3) Unit) := .leaf (.quant () (.trig 01) (.plain 2))
ConstRestr M C F ∧ (sys M).NT IsQ C F ∧ ¬ M.Expressive ∧
(sys M).Transp C F ∧ ¬ (sys M).Def F C := byintro M C F
refine ⟨?_, ?_, exprModel_not_expressive, ?_, ?_⟩
· intro l hl q P R hlq
simp [F, Fm.leaves] at hl
subst hl
cases hlq
exact ⟨1, byintro w _; cases w <;> decide⟩
· intro π l hπ _
obtain ⟨rfl, rfl⟩ := Sys.plug_leaf_eq hπ
refine ⟨.hole, rfl, ⟨true, trivial, ?_⟩, ⟨false, trivial, ?_⟩⟩ <;>
simp [Ctx.plug, Sys.eval, evalF, sys, QModel.qsem, M, exprModel, QModel.pstat, cnt] <;> decide
· show (sys exprModel).Transp _ _
rw [transp_quant]
refine ⟨?_, (fun k j h => bycases h)⟩
intro k j h
cases h
intro m Y w _
rcases Y with a | ⟨a, b⟩ | ⟨a, b⟩
...
Q1false statement Theorem 2: add the hypothesis that every property over the domain can be expressed by a predicate
Suppose that (i) the domain of individuals is of constant finite size over C, and (ii) the extension of each restrictor that appears in F is of constant size over C, and (iii) <C, F> satisfies Non-Triviality.
Suggested replacement
Suppose that (i) the domain of individuals is of constant finite size over C, and (ii) the extension of each restrictor that appears in F is of constant size over C, and (iii) <C, F> satisfies Non-Triviality, and (iv) any property over the domain can be expressed by some predicate.
What the paper does, and why it fails
Theorem 2 lists three hypotheses, but its proof (case (g)) relies on Lemma 1, whose hypothesis (b) says that any property over the domain can be expressed by some predicate. Without it the theorem is false: with two worlds, two individuals, and only predicates true of individual 0, Transparency holds for (Q P̲P’. R) although individual 1 violates the presupposition, so C[F] = #.
What the change does
The theorem now carries the same expressiveness hypothesis as Lemma 1, which the proof of case (g) needs. The corrected theorem is proved in Lean (theorem2, with M.Expressive).
Anything else affected?Also affects: the informal statements of the result, in the abstract and in Section 6 (‘the equivalence holds under the conditions of Constancy and Non-Triviality’), should mention expressiveness too (or point to the assumption of Section 2.1 that the language is quite expressive). Theorem 1 (propositional), Lemma 1 and Lemma 2 are unchanged.
theorem theorem2_needs_expressiveness :
let M := exprModel
let C : WSet Bool := fun _ => True
let F : Fm (QLeaf Unit (Fin 3) Unit) := .leaf (.quant () (.trig 01) (.plain 2))
ConstRestr M C F ∧ (sys M).NT IsQ C F ∧ ¬ M.Expressive ∧
(sys M).Transp C F ∧ ¬ (sys M).Def F C := byintro M C F
refine ⟨?_, ?_, exprModel_not_expressive, ?_, ?_⟩
· intro l hl q P R hlq
simp [F, Fm.leaves] at hl
subst hl
cases hlq
exact ⟨1, byintro w _; cases w <;> decide⟩
· intro π l hπ _
obtain ⟨rfl, rfl⟩ := Sys.plug_leaf_eq hπ
refine ⟨.hole, rfl, ⟨true, trivial, ?_⟩, ⟨false, trivial, ?_⟩⟩ <;>
...
theorem theorem2 (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) :
∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') := byintro C' F' hacc
refine ⟨?_, fun hd => (sys M).upd_eq_TS F' C' hd⟩
refine (sys M).lift (C₀ := C) (F₀ := F) ?_ F' C' hacc
intro C'' l hl
have hNT' := (sys M).lemma2 hNT hl
obtain ⟨hsub, hleaf⟩ := hl.sub
rw [Sys.transp_leaf]
cases l with
| atom i => simp [sys]
| trig a b =>
simp only [sys]
...
Paper text (symbols restored from the PDF)Theorem 2 Let C be a Context Set and let F be a formula. Suppose that (i) the domain of individuals is of constant finite size over C, and (ii) the extension of each restrictor that appears in F is of constant size over C, and (iii) <C, F> satisfies Non-Triviality. Then for every < C′, F′ > which is accessed by <C, F> (including <C, F> itself): (i) Transp(C′, F′) iff C′[F′] ≠ #. (ii) If C′[F′] ≠ #, C′[F′] = {w ∈ C′: w ⊨ F′}.
Statement(i)-(iii) + every property expressible ⇒ for every accessed ⟨C',F'⟩: Transp(C',F') ↔ C'[F'] ≠ # and C'[F'] = {w∈C': w⊨F'}
Lean statementtheorem2 (hexp : M.Expressive) C F (ConstRestr M C F) (NT IsQ C F) : ∀ C' F', Accessed C F C' F' → (Transp C' F' ↔ Def F' C') ∧ (Def F' C' → Upd F' C' = TS F' C')
theorem theorem2 (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) :
∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') := byintro C' F' hacc
refine ⟨?_, fun hd => (sys M).upd_eq_TS F' C' hd⟩
refine (sys M).lift (C₀ := C) (F₀ := F) ?_ F' C' hacc
intro C'' l hl
have hNT' := (sys M).lemma2 hNT hl
obtain ⟨hsub, hleaf⟩ := hl.sub
rw [Sys.transp_leaf]
cases l with
| atom i => simp [sys]
| trig a b =>
simp only [sys]
constructor
· intro h w hw
have := h (.conj (.leaf (.atom a)) (sys M).top) (sys M).top ⟨(sys M).top, rfl, rfl⟩ w hw
simpa [Sys.eval, evalF, sys, (sys M).top_true] using this
· rintro h φ₁ φ₂ ⟨γ, rfl, rfl⟩ w hw
simp [Sys.eval, evalF, h w hw]
| quant q P R =>
have hc : ∃ p, ∀ w, C'' w → cnt M.n (M.pstat P w) = p := by
...
Q1false statement Theorem 2: add the hypothesis that every property over the domain can be expressed by a predicate
Suppose that (i) the domain of individuals is of constant finite size over C, and (ii) the extension of each restrictor that appears in F is of constant size over C, and (iii) <C, F> satisfies Non-Triviality.
Suggested replacement
Suppose that (i) the domain of individuals is of constant finite size over C, and (ii) the extension of each restrictor that appears in F is of constant size over C, and (iii) <C, F> satisfies Non-Triviality, and (iv) any property over the domain can be expressed by some predicate.
What the paper does, and why it fails
Theorem 2 lists three hypotheses, but its proof (case (g)) relies on Lemma 1, whose hypothesis (b) says that any property over the domain can be expressed by some predicate. Without it the theorem is false: with two worlds, two individuals, and only predicates true of individual 0, Transparency holds for (Q P̲P’. R) although individual 1 violates the presupposition, so C[F] = #.
What the change does
The theorem now carries the same expressiveness hypothesis as Lemma 1, which the proof of case (g) needs. The corrected theorem is proved in Lean (theorem2, with M.Expressive).
Anything else affected?Also affects: the informal statements of the result, in the abstract and in Section 6 (‘the equivalence holds under the conditions of Constancy and Non-Triviality’), should mention expressiveness too (or point to the assumption of Section 2.1 that the language is quite expressive). Theorem 1 (propositional), Lemma 1 and Lemma 2 are unchanged.
theorem theorem2_needs_expressiveness :
let M := exprModel
let C : WSet Bool := fun _ => True
let F : Fm (QLeaf Unit (Fin 3) Unit) := .leaf (.quant () (.trig 01) (.plain 2))
ConstRestr M C F ∧ (sys M).NT IsQ C F ∧ ¬ M.Expressive ∧
(sys M).Transp C F ∧ ¬ (sys M).Def F C := byintro M C F
refine ⟨?_, ?_, exprModel_not_expressive, ?_, ?_⟩
· intro l hl q P R hlq
simp [F, Fm.leaves] at hl
subst hl
cases hlq
exact ⟨1, byintro w _; cases w <;> decide⟩
· intro π l hπ _
obtain ⟨rfl, rfl⟩ := Sys.plug_leaf_eq hπ
refine ⟨.hole, rfl, ⟨true, trivial, ?_⟩, ⟨false, trivial, ?_⟩⟩ <;>
...
theorem theorem2 (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) :
∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') := byintro C' F' hacc
refine ⟨?_, fun hd => (sys M).upd_eq_TS F' C' hd⟩
refine (sys M).lift (C₀ := C) (F₀ := F) ?_ F' C' hacc
intro C'' l hl
have hNT' := (sys M).lemma2 hNT hl
obtain ⟨hsub, hleaf⟩ := hl.sub
rw [Sys.transp_leaf]
cases l with
| atom i => simp [sys]
| trig a b =>
simp only [sys]
...
Q4btypo Proof of Theorem 2, case (f): ‘this entails that’ must be followed by ‘not’
Location: Section 5.3, proof of Theorem 2, case (f), p. 351 PDF p.27
Paper text
By the Transparency Lemma (part (b)), this entails that Transp(C′, (if G. H)).
Suggested replacement
By the Transparency Lemma (part (b)), this entails that not Transp(C′, (if G. H)).
What the paper does, and why it fails
In case (f) the proof has just shown that not Transp(C′, G) and must conclude that not Transp(C′, (if G. H)), as in cases (d) and (e). As printed, it concludes the opposite, Transp(C′, (if G. H)).
What the change does
The sentence now draws the negative conclusion that the argument needs (the contrapositive of Transparency Lemma (b)).
Anything else affected?No other change: the case is used correctly in the rest of the proof; it is formalized as transp_cond and theorem2.
Text note: Wording is verbatim; symbols lost in the text extraction (⊨, ⊭, ⇔, superscripts, underlining, Greek letters, primes) were restored from the PDF.
theorem transp_cond (S : Sys W L) (C : WSet W) (G H : Fm L) :
S.Transp C (.cond G H) ↔ S.Transp C G ∧ S.Transp (S.TS G C) H := byconstructor
· intro h
constructor
· intro π l hπ π' hc φ₁ φ₂ hv w hw
have := h (.condL π H) l (bysimp [Ctx.plug, hπ]) (.condL π' S.bot)
⟨π', S.bot, rfl, hc⟩ φ₁ φ₂ hv w hw
simpa [Ctx.plug, S.bot_false] using this
· intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
have := h (.condR G π) l (bysimp [Ctx.plug, hπ]) (.condR G π')
⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
simpa [Ctx.plug, hwG] using this
· intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
cases π <;> simp [Ctx.plug] at hπ
case condL π1 r =>
...
theorem theorem2 (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) :
∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') := byintro C' F' hacc
refine ⟨?_, fun hd => (sys M).upd_eq_TS F' C' hd⟩
refine (sys M).lift (C₀ := C) (F₀ := F) ?_ F' C' hacc
intro C'' l hl
have hNT' := (sys M).lemma2 hNT hl
obtain ⟨hsub, hleaf⟩ := hl.sub
rw [Sys.transp_leaf]
cases l with
| atom i => simp [sys]
| trig a b =>
simp only [sys]
...
Q5typo Theorem 2, case (g): P is used both for the presupposition P and for the whole restrictor
Location: Section 5.3, Theorem 2, case (g), p. 351-352 PDF p.27
Paper text
1. If Transp(C′, F′), then C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [P(d) ⇒ R(d)] (as in Lemma 1).
Suggested replacement (Theorem 2, case (g), Part (i), item 1)
1. If Transp(C′, F′), then C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [(P and P′)(d) ⇒ R(d)] (as in Lemma 1).
Paper text
2. If C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [P(d) ⇒ R(d)], then Transp(C′, F′) (immediate).
Suggested replacement (Theorem 2, case (g), Part (i), item 2)
2. If C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [(P and P′)(d) ⇒ R(d)], then Transp(C′, F′) (immediate).
Paper text
because C′[F′] ≠ #, and thus C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [P(d) ⇒ R(d)]
Suggested replacement (Theorem 2, case (g), Part (ii), last line)
because C′[F′] ≠ #, and thus C′ ⊨ ∀d P(d) and C′ ⊨ ∀d [(P and P′)(d) ⇒ R(d)]
What the paper does, and why it fails
For F′ = (Qi P̲P′. R̲R′), ‘P’ means the presupposition of the restrictor in ∀d P(d), but in ∀d [P(d) ⇒ R(d)] (case (b)) it means the whole restrictor. Read with P the presupposition, the second condition is too strong: together with ∀d P(d) it would say ∀d R(d).
What the change does
The second condition is now Heim’s (21): every individual satisfying both the presupposition and the assertion of the restrictor, (P and P′)(d), satisfies R. This is the condition proved in Lean (qdef_both, lemma1_ii).
Anything else affected?No other change: the correct condition is what is proved and used; Theorem 2 is unaffected. Case (b) just above (‘the size of the extension of P is constant’) can stay: there P is the whole restrictor.
Text note: In the paper P̲ and R̲ are underlined presupposition triggers; underlining is not reproduced here.
theorem qdef_both (k j k' j' : ρ) (C : WSet W) :
M.qdef (.trig k j) (.trig k' j') C ↔
(∀ w, C w → ∀ d, d < M.n → M.I k w d = true) ∧
(∀ w, C w → ∀ d, d < M.n → (M.I k w d && M.I j w d) = true → M.I k' w d = true) := bysimp [QModel.qdef, QModel.ppre, QModel.pstat]
theorem lemma1_ii (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ) (P : Pred ρ) (p : Nat)
(hp : ∀ w, C w → cnt M.n (M.pstat P w) = p)
(hline : ∃ b₁ b₂, b₁ ≤ p ∧ b₂ ≤ p ∧ M.f q (p - b₁) b₁ ≠ M.f q (p - b₂) b₂) :
ST M C q P k ↔ ∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.pstat P w d = true ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd hPd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hPd, hd'⟩
...
N1note Note: the Constancy and Non-Triviality hypotheses of Theorem 2 could be weakened
Suppose that (i) the domain of individuals is of constant finite size over C, and (ii) the extension of each restrictor that appears in F is of constant size over C, and (iii) <C, F> satisfies Non-Triviality
Suggested replacement (optional remark after the statement of Theorem 2)
(delete)
Paper text
(insert)
Suggested replacement (optional; optional remark after the statement of Theorem 2)
Remark. Hypothesis (ii) is only used for clauses whose nuclear scope carries a presupposition trigger (Lemma 1(ii)); Lemma 1(i) needs only Non-Triviality and constant domain size. Non-Triviality is only used for the clauses actually involved.
What the paper does, and why it fails
Theorem 2 assumes constant restrictor sizes and Non-Triviality for the whole formula, although the proof uses them clause by clause.
What the change does
No edit is needed. The optional remark records that the theorem could be sharpened.
Anything else affected?No other change: it is an observation about the structure of the proof (Lemma 1(i) versus 1(ii)); no claim of the paper changes.
theorem lemma1_i (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ)
(htri : ∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b') :
RT M C q k ↔ ∀ w, C w → ∀ d, d < M.n → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
-- a world `w ∈ C` and an individual `d0 < n` with `¬ P(d0)`have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hd'⟩
...
theorem lemma1_ii (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ) (P : Pred ρ) (p : Nat)
(hp : ∀ w, C w → cnt M.n (M.pstat P w) = p)
(hline : ∃ b₁ b₂, b₁ ≤ p ∧ b₂ ≤ p ∧ M.f q (p - b₁) b₁ ≠ M.f q (p - b₂) b₂) :
ST M C q P k ↔ ∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true := byconstructor
· intro h
apply Classical.byContradiction
intro hne
have : ∃ w, C w ∧ ∃ d, d < M.n ∧ M.pstat P w d = true ∧ M.I k w d ≠ true := byapply Classical.byContradiction
intro hh
apply hne
intro w hw d hd hPd
apply Classical.byContradiction
intro hd'
exact hh ⟨w, hw, d, hd, hPd, hd'⟩
...
Paper text (symbols restored from the PDF)In this counter-example, however, it is crucial that the extension of P does not have the same size in w (|P^w| = 2) and in w′ and w″ (|P^w′| = |P^w″| = 4). We will see that that this property is indeed essential to construct the problematic examples, and that when Non-Triviality is combined with the requirement (=Constancy) that the size of the extension of each restrictor be fixed throughout the Context Set, the equivalence with Heim’s theory can indeed be achieved.
/-- (32a) is exactly Heim's `if not F, G`. -/theorem unlessA_is_if_not :
(unlessA_def v i0 F G C ↔ (sys v i0).Def (.cond (.neg F) G) C) ∧
unlessA_upd v i0 F G C = (sys v i0).Upd (.cond (.neg F) G) C := ⟨Iff.rfl, rfl⟩
theorem unless_variants_agree_trigfree (hF : TrigFree F) (hG : TrigFree G) :
unlessA_def v i0 F G C ∧ unlessB_def v i0 F G C ∧ unlessC_def v i0 F G C ∧
unlessD_def v i0 F G C ∧ unlessD_upd v i0 F G C = unlessA_upd v i0 F G C := byhave dF := trigFree_def v i0 F hF
have dG := trigFree_def v i0 G hG
refine ⟨⟨dF C, dG _⟩, ⟨dF C, dG _⟩, ⟨dF C, dG C⟩, ⟨dG C, dF _⟩, ?_⟩
have hU : ∀ (H : PFm ι), TrigFree H → ∀ (D : WSet W), (sys v i0).Upd H D = (sys v i0).TS H D :=
fun H hH D => (sys v i0).upd_eq_TS H D (trigFree_def v i0 H hH D)
have hFn : TrigFree (.neg F : PFm ι) := hF
unfold unlessD_upd unlessA_upd
funext w; apply propext
simp only [hU F hF, hU G hG, hU _ hFn, Sys.TS, Sys.eval_neg]
cases (sys v i0).eval F w <;> cases (sys v i0).eval G w <;> simp <;> grind
theorem unlessD_paper_is_wrong :
∃ (v : Unit → Bool → Bool) (C : WSet Unit) (F G : PFm Bool), TrigFree F ∧ TrigFree G ∧
unlessD_upd_paper v true F G C ≠ unlessA_upd v true F G C := byrefine ⟨fun _ i => !i, fun _ => True, at_ false, at_ true, trivial, trivial, ?_⟩
-- letter `false` is true, letter `true` is false: F true, G falseintro h
have := congrFun h ()
simp [unlessD_upd_paper, unlessA_upd, Sys.Upd, sys, at_] at this
Q7false statement Rule (32)d for ‘unless’: the update should remove C[(not G)][(not F)]; (32)b,c need a caveat
Location: Section 6.1, rules (32)a-d, p. 352 PDF p.28
Paper text
d. C[unless F, G] = # iff C[G] = # or (C[G] ≠ # and C[(not G)][F] = #). If ≠ #, C[unless F, G] = C − C[(not G)][F]
Suggested replacement
d. C[unless F, G] = # iff C[G] = # or (C[G] ≠ # and C[(not G)][F] = #). If ≠ #, C[unless F, G] = C − C[(not G)][(not F)]
Further edits
Paper text
b. C[unless F, G] = # iff C[F] = # or C[F][G] = # If ≠ #, ... (as in (a)).
Suggested replacement (Rule (32)b)
b. C[unless F, G] = # iff C[F] = # or C[F][G] = # If ≠ #, C[unless F, G] = C − C[(not F)][(not G)] (as in (a); this update is defined only if C[(not F)][G] ≠ #, which the condition above does not guarantee).
Paper text
c. C[unless F, G] = # iff C[F] = # or C[G] = # If ≠ #, ... (as in (a)).
Suggested replacement (Rule (32)c)
c. C[unless F, G] = # iff C[F] = # or C[G] = # If ≠ #, C[unless F, G] = C − C[(not F)][(not G)] (as in (a); this update is defined only if C[(not F)][G] ≠ #, which the condition above does not guarantee).
What the paper does, and why it fails
The update of (32)d removes C[(not G)][F], the worlds where G is false and F is true. So for trigger-free F, G it yields ‘if F then G’ (worlds where F implies G), not the content of ‘unless F, G’ (F or G). This contradicts the paper’s claim that all four rules agree when F and G have no triggers. In (32)b,c the update is only said to be ‘as in (a)’, but (a)’s update needs C[(not F)][G] ≠ #, which the definedness conditions of (b) and (c) do not ensure.
What the change does
The corrected (32)d removes the worlds where both G and F are false, C[(not G)][(not F)], which is F or G. The four rules now agree on trigger-free F, G, as the text says. For (b) and (c) the caveat makes explicit that the update may be undefined.
Anything else affected?No other change: the definedness conditions, hence the predictions discussed for (33), are unchanged. The (33) predictions and the comparison with ‘if not’ rest on (32)a (Lean: unless_33, transp_unless_eq_if_not, unless_variants_agree_trigfree).
Text note: Wording is verbatim; symbols lost in the text extraction (⊨, ⊭, ⇔, superscripts, underlining, Greek letters, primes) were restored from the PDF.
Judgment call: the wording of this replacement is ours and not checked in Lean. For (32)b,c the paper itself hints at the problem (‘could potentially be ruled out by requiring …’); We only made the ‘(as in (a))’ explicit rather than changing the definedness conditions, which would change the predictions discussed for (33).
theorem unlessD_paper_is_wrong :
∃ (v : Unit → Bool → Bool) (C : WSet Unit) (F G : PFm Bool), TrigFree F ∧ TrigFree G ∧
unlessD_upd_paper v true F G C ≠ unlessA_upd v true F G C := byrefine ⟨fun _ i => !i, fun _ => True, at_ false, at_ true, trivial, trivial, ?_⟩
-- letter `false` is true, letter `true` is false: F true, G falseintro h
have := congrFun h ()
simp [unlessD_upd_paper, unlessA_upd, Sys.Upd, sys, at_] at this
theorem unless_variants_agree_trigfree (hF : TrigFree F) (hG : TrigFree G) :
unlessA_def v i0 F G C ∧ unlessB_def v i0 F G C ∧ unlessC_def v i0 F G C ∧
unlessD_def v i0 F G C ∧ unlessD_upd v i0 F G C = unlessA_upd v i0 F G C := byhave dF := trigFree_def v i0 F hF
have dG := trigFree_def v i0 G hG
refine ⟨⟨dF C, dG _⟩, ⟨dF C, dG _⟩, ⟨dF C, dG C⟩, ⟨dG C, dF _⟩, ?_⟩
have hU : ∀ (H : PFm ι), TrigFree H → ∀ (D : WSet W), (sys v i0).Upd H D = (sys v i0).TS H D :=
fun H hH D => (sys v i0).upd_eq_TS H D (trigFree_def v i0 H hH D)
have hFn : TrigFree (.neg F : PFm ι) := hF
unfold unlessD_upd unlessA_upd
funext w; apply propext
simp only [hU F hF, hU G hG, hU _ hFn, Sys.TS, Sys.eval_neg]
cases (sys v i0).eval F w <;> cases (sys v i0).eval G w <;> simp <;> grind
Paper text (symbols restored from the PDF)(33) Unless John didn’t come, Mary will know that he is here. (33) seems to presuppose that if John came, he is here. This is exactly the prediction made by (32)a: since the unless-clause contains no presupposition trigger, the presupposition is that C[(not F)][G] ≠ # with F = John didn’t come and G = John is here.
Statement(a): "if John came, he is here"; (b): "if John didn't come ..."; (c),(d): "John is here"; Transparency gives (a)
theorem unless_33 (c h h' : ι) (C : WSet W) :
(unlessA_def v i0 (at_ c) (tr_ h h') C ↔ ∀ w, C w → v w c = false → v w h = true) ∧
(unlessB_def v i0 (at_ c) (tr_ h h') C ↔ ∀ w, C w → v w c = true → v w h = true) ∧
(unlessC_def v i0 (at_ c) (tr_ h h') C ↔ ∀ w, C w → v w h = true) ∧
(unlessD_def v i0 (at_ c) (tr_ h h') C ↔ ∀ w, C w → v w h = true) ∧
((sys v i0).Transp C (.cond (.neg (at_ c)) (tr_ h h')) ↔
∀ w, C w → v w c = false → v w h = true) := byhave hT := transp_atomic v i0
refine ⟨?_, ?_, ?_, ?_, ?_⟩
· simp only [unlessA_def, Sys.Def, Sys.Upd, sys, at_, tr_]
constructor
· rintro ⟨-, h⟩ w hw hc; exact h w ⟨hw, bysimp [hc]⟩
· intro h; exact ⟨trivial, fun w ⟨hw, hn⟩ => h w hw (bysimp_all)⟩
· simp only [unlessB_def, Sys.Def, Sys.Upd, sys, at_, tr_]
constructor
· rintro ⟨-, h⟩ w hw hc; exact h w ⟨hw, hc⟩
· intro h; exact ⟨trivial, fun w ⟨hw, hn⟩ => h w hw hn⟩
· simp only [unlessC_def, Sys.Def, sys, tr_]
exact ⟨fun h => h.2, fun h => ⟨trivial, h⟩⟩
· simp only [unlessD_def, Sys.Def, sys, tr_]
exact ⟨fun h => h.1, fun h => ⟨h, trivial⟩⟩
· rw [theorem1_i]
simp only [Sys.Def, Sys.Upd, sys, at_, tr_]
constructor
...
Paper textFor the Transparency theory, the explanation is immediate. Unless has essentially the same syntax and the same bivalent contribution as if-not, and therefore it should have the same projection behavior.
Statementsame projection
Lean statementtransp_unless_eq_if_not : Transp C (F or G) ↔ Transp C (if (not F) . G)
Lean: Deviants.lean:206 · confirmed (for the static content F ∨ G; unless itself is not added to the syntax)
theorem transp_unless_eq_if_not (F G : PFm ι) (C : WSet W) :
(sys v i0).Transp C (.disj F G) ↔ (sys v i0).Transp C (.cond (.neg F) G) := byrw [caseE, caseF, caseC]
constructor <;> rintro ⟨h1, h2⟩ <;> refine ⟨h1, ?_⟩
· have : (fun w => C w ∧ (sys v i0).eval F w = false) = (sys v i0).TS (.neg F) C := byfunext w; apply propext; simp only [Sys.TS, Sys.eval_neg]; cases (sys v i0).eval F w <;> simprw [← this]; exact h2
· have : (fun w => C w ∧ (sys v i0).eval F w = false) = (sys v i0).TS (.neg F) C := byfunext w; apply propext; simp only [Sys.TS, Sys.eval_neg]; cases (sys v i0).eval F w <;> simprw [this]; exact h2
Paper text(34) Context We are discussing a soccer match with Frenchmen on both teams. -Team A includes 4 Frenchmen, who have all decided to retire. [...] -Team B includes 2 Frenchmen, only one of whom has decided to retire. [...] No matter what happens, less than 3 Frenchmen of the winning team will reconsider their decision to retire. Heim’s prediction is that in every world of the Context Set, every Frenchman of the winning team has decided to retire. We make no such prediction
Statementin each world either every P-individual has decided or fewer than 3 P-individuals: Transp holds; Heim predicts failure
Lean statementsoccer_example (W = {A wins, B wins}, 6 individuals)
Paper textThe prediction is entirely general: if two combinations of connectives have the same syntax and the same bivalent contribution, they should have the same projective behavior. Dynamic semantics makes no such prediction.
Statementsame syntax + same bivalent contribution ⇒ same projection
Lean statementtrue by construction (Transp mentions only syntax and static semantics); instance R38
Paper textGlobal accommodation occurs when a presupposition is not satisfied in the initial Context Set, which is thus modified so as to prevent the sentence from being infelicitous.
Statementinformal
Lean statement–
not formalized (informal proposal, no formal claim)
Why not formalized: An informal proposal about how accommodation works in Heim's and in the Transparency framework; the paper states no precise claim, so there is nothing to formalize without first inventing a definition.
R42not formalized
Meta-constraint on the lexicon (Shan/Heim), linear vs processing order, DRT
Paper textThus there might be a 'meta-constraint' on the lexicon that requires that, say, the Context Change Potential of and should guarantee equivalence with Transparency.
Statementresearch suggestions
Lean statement–
not formalized (open questions, not claims)
Why not formalized: A research suggestion (from Shan and Heim) with no formal statement in the paper. It could be formalized once a precise notion of 'admissible Context Change Potential' is fixed.
R43not formalized
Empirical data (1), (3), (4), (7); Stalnaker's (i)-(iii)
Paper text(1) a. The king of Moldavia is powerful. b. Moldavia is a monarchy and the king of Moldavia is powerful. c. If Moldavia is a monarchy, the king of Moldavia is powerful. (1)a presupposes (incorrectly) that Moldavia has a king. But the examples in (1)b–c presuppose no such thing; they only presuppose that if Moldavia is a monarchy, it has a king
Statementjudgments; historical background
Lean statement–
not formalized (empirical/historical)
Why not formalized: Empirical judgments and historical background (Stalnaker's assumptions (i)-(iii) are used as definitions elsewhere, but the empirical data are not formal claims).
A1suggested new result
Exact world-by-world characterization of Transparency for a quantified clause
Statement to add (Section 5.2, as a strengthening/restatement placed right after Lemma 1 (pp. 345-348), and again in the discussion of Constancy and Non-Triviality in Section 5.1 / Section 6.5 (soccer example, p. 354-5).)
Assume every property of individuals is expressible. For a context C and a clause with a trigger in the nuclear scope, Transp(C, (Qi P. R̲R')) holds iff for every w ∈ C, either P^w ⊆ R^w (Heim's presupposition is satisfied at w) or f_i is constant on the line {(a,b) : a+b = |P^w|}. Likewise, Transp(C, (Qi P̲P'. R)) holds iff for every w ∈ C, either every individual satisfies P at w or f_i is constant on the whole triangle {(a,b) : a+b ≤ n}. In particular Transp and Heim's presupposition come apart on ⟨C,F⟩ exactly when some world violates Heim's condition and every world that does so has f_i constant on the relevant line (or triangle). Neither the constancy of |P^w| nor Non-Triviality is needed for this.
Why it is useful
It turns Lemma 1's two sufficient conditions into an exact 'if and only if', and shows that the 'constant restrictor size' hypothesis only serves to make the non-constancy of f uniform across worlds. It also explains in one line why the less-than-three and soccer scenarios diverge from Heim.
Proof idea
The 'if' directions are immediate: under Heim's condition the trigger conjunct is redundant, and when f is constant on the line the two counts give the same value. For 'only if', restrict the context to a single world w (Transparency is preserved by shrinking C), and if f is not constant on the line (triangle) at w apply Lemma 1(ii) (Lemma 1(i)) to that one-world context, where the restrictor size is trivially constant.
FidelityHigh for fidelity: it is a direct corollary of the already-verified Lemma 1 (lemma1_i, lemma1_ii) via the single-world trick, stated for the same clause fragment and the same Expressive hypothesis. The 'come apart' sentence is an informal reading of the pointwise iff. Limited to the formalized clause types (P, P̲P', (P and P') predicates).
theorem rt_pointwise (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ) :
RT M C q k ↔ ∀ w, C w →
((∀ d, d < M.n → M.I k w d = true) ∨ TriConst (M.f q) M.n) := byconstructor
· intro h w hw
by_cases hl : TriConst (M.f q) M.n
· exact Or.inr hl
· lefthave hne : ∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b' := byapply Classical.byContradiction
intro hn
apply hl
intro a b a' b' h1 h2
apply Classical.byContradiction
intro hne
exact hn ⟨a, b, a', b', h1, h2, hne⟩
...
/-- Transparency of a full quantificational clause, world by world. -/theorem transp_quant_pointwise (hexp : M.Expressive) (C : WSet W) (q : κ) (P R : Pred ρ) :
(sys M).Transp C (.leaf (.quant q P R)) ↔
(∀ k j, P = .trig k j → ∀ w, C w →
((∀ d, d < M.n → M.I k w d = true) ∨ TriConst (M.f q) M.n)) ∧
(∀ k j, R = .trig k j → ∀ w, C w →
((∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true) ∨
LineConst (M.f q) (cnt M.n (M.pstat P w)))) := byrw [transp_quant]
constructor
· rintro ⟨h1, h2⟩
exact ⟨fun k j hP => (rt_pointwise M hexp C q k).1 (h1 k j hP),
fun k j hR => (st_pointwise M hexp C q P k).1 (h2 k j hR)⟩
· rintro ⟨h1, h2⟩
exact ⟨fun k j hP => (rt_pointwise M hexp C q k).2 (h1 k j hP),
fun k j hR => (st_pointwise M hexp C q P k).2 (h2 k j hR)⟩
A2suggested new result
Theorem 2 without Constancy and Non-Triviality (local non-degeneracy version)
Statement to add (Section 5.3, immediately after the statement of Theorem 2 (p. 350), as a remark or a stronger theorem; the last sentence of the abstract/Section 6 ('under Constancy and Non-Triviality') could then say the hypotheses can be weakened to a purely local condition on the quantifier.)
Theorem 2′. Suppose every property of individuals is expressible, and that for every clause (Qi P. R) in an accessed pair ⟨C', F'⟩ accessed by ⟨C, F⟩: (a) if P carries a trigger, f_i is not constant on {(a,b) : a+b ≤ n}; (b) if R carries a trigger, f_i is not constant on {(a,b) : a+b = |P^w|} for every w ∈ C'. Then for every accessed ⟨C', F'⟩: Transp(C',F') iff C'[F'] ≠ #, and if C'[F'] ≠ # then C'[F'] = {w ∈ C' : w ⊨ F'}. Theorem 2 (with expressiveness) is the special case where (ii) constant restrictor size and (iii) Non-Triviality give (a) and (b) via the Non-Triviality Corollary and Lemma 2. The converse fails: the hypotheses of Theorem 2′ do not imply constant restrictor size (Q = no, n = 2, restrictor of size 2 in one world and 1 in the other, F = (no P. R̲R')).
Why it is useful
It removes the need for Lemma 2 (inheritance of Non-Triviality by accessed pairs) and for the global Constancy hypothesis, and covers examples with varying restrictor size (like the soccer scenario) where Theorem 2 as stated does not apply. It also makes the hypotheses checkable clause by clause.
Proof idea
The connective steps of Theorem 2 (cases (c)-(f)) are unchanged. At a quantified leaf, A1 gives Transparency as a world-by-world condition; non-degeneracy rules out the 'f constant' escape at every world, leaving exactly Heim's definedness condition. Non-degeneracy is a property of f and of |P^w| only, so it is trivially inherited by shrinking contexts. Theorem 2's hypotheses imply it by the Non-Triviality Corollary and Lemma 2.
FidelityHigh for the formal statement as formalized (same fragment as theorem2, same accessed-pair machinery). The non-degeneracy hypothesis is stated on accessed clauses only, as in the paper's Lemma 2 setting. The strictness example uses predicate letters that are the properties themselves (so expressiveness is trivial) and a two-world, two-individual model.
/-- Lemma 1 for a clause under `NonDeg` alone. -/theorem quant_leaf' (hexp : M.Expressive) (C : WSet W) (q : κ) (P R : Pred ρ)
(hnd : NonDeg M C q P R) :
(sys M).Transp C (.leaf (.quant q P R)) ↔ M.qdef P R C := byobtain ⟨hn1, hn2⟩ := hnd
rw [transp_quant_pointwise M hexp]
constructor
· rintro ⟨h1, h2⟩
refine ⟨?_, ?_⟩
· intro w hw d hd
cases P with
| plain k => rfl
| conj k j => rfl
| trig k j =>
rcases h1 k j rfl w hw with h | h
· exact h d hd
...
theorem theorem2' (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(hnd : NondegAcc M C F) :
∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') := byintro C' F' hacc
refine ⟨?_, fun hd => (sys M).upd_eq_TS F' C' hd⟩
refine (sys M).lift (C₀ := C) (F₀ := F) ?_ F' C' hacc
intro C'' l hl
rw [Sys.transp_leaf]
cases l with
| atom i => simp [sys]
| trig a b =>
simp only [sys]
constructor
· intro h w hw
...
/-- Theorem 2's hypotheses (ii), (iii) imply `NondegAcc`. -/theorem nondegAcc_of_NT (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) : NondegAcc M C F := byintro C'' q P R hacc
have hNT' := (sys M).lemma2 hNT hacc
obtain ⟨hsub, hleaf⟩ := hacc.sub
obtain ⟨p, hp⟩ := hconst _ (hleaf _ (bysimp [Fm.leaves])) q P R rflhave hp' : ∀ w, C'' w → cnt M.n (M.pstat P w) = p := fun w hw => hp w (hsub w hw)
obtain ⟨a, b, a', b', h1, h2, hne⟩ := nt_corollary_i M hNT'
obtain ⟨c₁, c₂, g1, g2, hne'⟩ := nt_corollary_ii M hNT' hp'
refine ⟨fun k j _ hc => hne (hc a b a' b' h1 h2), fun k j _ w hw hc => ?_⟩
rw [hp' w hw] at hc
exact hne' (hc c₁ c₂ g1 g2)
/-- The corrected Theorem 2 is a corollary of `theorem2'`. -/theorem theorem2_via_theorem2' (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
(hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) :
∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') :=
theorem2' M hexp C F (nondegAcc_of_NT M C F hconst hNT)