leanified/CoreReader/Logic.lean

返回主张速览 · 声明与证明

哲学 0.2.1 · 已考虑的 Core 0.1.2。阅读视图来自本仓库公开的目标清单、读者稿和 Lean 文件；页面布局不改变其中的判定。

展开 Lean 与逐行解读 · 185 行

Lean逐行解读

L1namespace CoreReader.Logic

打开命名空间 CoreReader.Logic，使后续声明获得这一模块限定名。

L3/- A claim denotes the worlds in which its content holds. -/

说明 Claim 的预定范围。对应声明涉及：主张是从给定世界类型到命题的函数，不预设现实解释。 该注释用于解释，不是证明前提。

L4abbrev Claim (W : Type) := W → Prop

引入类型缩写 Claim。主张是从给定世界类型到命题的函数，不预设现实解释。

L5/- A theory is a collection of simultaneously held claims. -/

说明 Theory 的预定范围。对应声明涉及：理论用谓词选择同时持有的主张，不要求有限语法。 该注释用于解释，不是证明前提。

L6abbrev Theory (W : Type) := Claim W → Prop

引入类型缩写 Theory。理论用谓词选择同时持有的主张，不要求有限语法。

L7/- A model satisfies every member of the whole theory. -/

说明 Models 的预定范围。对应声明涉及：世界满足理论，指理论选择的每个主张都在此世界成立。 该注释用于解释，不是证明前提。

L8def Models {W : Type} (t : Theory W) (w : W) : Prop := ∀ p, t p → p w

定义 Models。世界满足理论，指理论选择的每个主张都在此世界成立。

L9/- Semantic entailment quantifies over all models. -/

说明 Entails 的预定范围。对应声明涉及：在所有理论模型中结论都成立；无模型时蕴涵可空真。 该注释用于解释，不是证明前提。

L10def Entails {W : Type} (t : Theory W) (p : Claim W) : Prop := ∀ w, Models t w → p w

定义 Entails。在所有理论模型中结论都成立；无模型时蕴涵可空真。

L11/- Satisfiability requires an actual witness. -/

说明 Satisfiable 的预定范围。对应声明涉及：要求存在实际世界及其满足全部理论主张的证明。 该注释用于解释，不是证明前提。

L12def Satisfiable {W : Type} (t : Theory W) : Prop := ∃ w, Models t w

定义 Satisfiable。要求存在实际世界及其满足全部理论主张的证明。

L13/- Assumptions, meanings and scope are distinct components; questions remain explicit. -/

说明 Context 的预定范围。对应声明涉及：分别保存附加假设、问题含义和适用范围。 该注释用于解释，不是证明前提。

L14structure Context (W Q : Type) where

声明数据接口 Context。分别保存附加假设、问题含义和适用范围。

L15  assumptions : Theory W

保存真实的上下文假设理论，与所持理论分开。

L16  meaning : Q → Claim W

把每个问题解释为针对每个世界的命题。

L17  scope : Claim W

保存选择被接纳应用范围的谓词。

L18/- Admissible worlds satisfy held claims, assumptions and scope jointly. -/

说明 Admissible 的预定范围。对应声明涉及：同一世界同时满足持有理论、上下文假设和范围。 该注释用于解释，不是证明前提。

L19def Admissible {W Q : Type} (t : Theory W) (c : Context W Q) (w : W) : Prop :=

定义 Admissible。同一世界同时满足持有理论、上下文假设和范围。

L20  Models t w ∧ Models c.assumptions w ∧ c.scope w

要求同一世界同时满足两个理论及上下文范围。

L21/- A negative judgment denies the very same question under the same meaning. -/

说明 Consequence 的预定范围。对应声明涉及：在同一上下文全部可接受世界中，要求指定问题的正或负结论。 该注释用于解释，不是证明前提。

L22def Consequence {W Q : Type} (t : Theory W) (c : Context W Q) (q : Q) (positive : Bool) : Prop :=

定义 Consequence。在同一上下文全部可接受世界中，要求指定问题的正或负结论。

L23  ∀ w, Admissible t c w → if positive then c.meaning q w else ¬ c.meaning q w

对每个可接受世界量化；符号选择该问题的含义或其否定。

L24/- The consistency obligation prohibits both consequences at one comparison basis. -/

说明 Consistent 的预定范围。对应声明涉及：禁止同一问题的正反后果并存；问题类型为空时条件空真。 该注释用于解释，不是证明前提。

L25def Consistent {W Q : Type} (t : Theory W) (c : Context W Q) : Prop :=

定义 Consistent。禁止同一问题的正反后果并存；问题类型为空时条件空真。

L26  ∀ q, ¬ (Consequence t c q true ∧ Consequence t c q false)

对每个问题，禁止同一上下文中正反后果的合取。

L27/- An inhabited joint interpretation prevents opposite semantic consequences. -/

说明 consequenceConsistency 的预定范围。对应声明涉及：用显式可接受世界同时实例化正反后果，导出矛盾，得到上下文一致性。 该注释用于解释，不是证明前提。

L28theorem consequenceConsistency {W Q : Type} (t : Theory W) (c : Context W Q)

陈述经检查的结果 consequenceConsistency。用显式可接受世界同时实例化正反后果，导出矛盾，得到上下文一致性。

L29    (inhabited : ∃ w, Admissible t c w) : Consistent t c := by

假定整个上下文具有可接受见证，得出其一致性；开始证明。

L30  intro q h

引入任意问题 q，以及假定的同一上下文中正反后果对 h。

L31  obtain ⟨w, hw⟩ := inhabited

从显式非空前提 inhabited 提取共同可接受世界 w，以及它满足整套理论、假设与范围的证明 hw。

L32  exact (h.2 w hw) (h.1 w hw)

在同一 w 与 hw 处应用 h 的两部分；否定后果与肯定后果矛盾。

L33/- Empty and singleton theories provide concrete semantic contexts. -/

说明 emptyTheory 的预定范围。对应声明涉及：不选择任何主张，故每个世界都是模型。 该注释用于解释，不是证明前提。

L34def emptyTheory {W : Type} : Theory W := fun _ => False

定义 emptyTheory。不选择任何主张，故每个世界都是模型。

L35def singleton {W : Type} (p : Claim W) : Theory W := fun q => q = p

定义 singleton。只选择与指定主张相等的谓词。

L36def union {W : Type} (a b : Theory W) : Theory W := fun p => a p ∨ b p

定义 union。以成员关系的析取合并两个理论。

L37theorem modelsSingleton {W : Type} (p : Claim W) (w : W) : Models (singleton p) w ↔ p w := by

陈述经检查的结果 modelsSingleton。证明满足单一主张理论等价于该主张在当前世界成立。 后续策略块证明这一显式类型。

L38  constructor

将满足单一主张理论与满足该主张的等价关系拆为两个蕴含。

L39  · intro h; exact h p rfl

把假定的单元素理论模型 h 应用于 p；p 的成员关系由自反相等成立。

L40  · intro h q hq; cases hq; exact h

任取被选择的主张 q，单元素成员关系将 q 与 p 等同；代入这一等式并返回 p 已成立的前提 h。

L41theorem modelsUnion {W : Type} (a b : Theory W) (w : W) :

陈述经检查的结果 modelsUnion。证明同一世界满足理论并集等价于同时满足两部分。

L42    Models (union a b) w ↔ Models a w ∧ Models b w := by

陈述同一世界满足理论并集，当且仅当它满足两个组成理论。

L43  constructor

分别证明满足并集与同时满足两个理论之间的正反方向。

L44  · intro h; exact ⟨fun p hp => h p (Or.inl hp), fun p hp => h p (Or.inr hp)⟩

把成员证明嵌入左或右析取，将并集模型 h 分别限制到两个理论。

L45  · rintro ⟨ha,hb⟩ p (hp|hp); exact ha p hp; exact hb p hp

拆出两个组成理论的模型，将并集成员关系分为两种情况，并在同一主张与世界上使用对应模型。

L46/- The paired world records independent truth values for two questions. -/

说明 premiseP 的预定范围。对应声明涉及：要求布尔对的第一坐标为真。 该注释用于解释，不是证明前提。

L47def premiseP : Claim (Bool × Bool) := fun w => w.1 = true

定义 premiseP。要求布尔对的第一坐标为真。

L48def premiseRule : Claim (Bool × Bool) := fun w => w.1 = true → w.2 = true

定义 premiseRule。要求第一坐标为真时第二坐标也为真。

L49def premiseNotQ : Claim (Bool × Bool) := fun w => w.2 ≠ true

定义 premiseNotQ。要求第二坐标不为真。

L50def jointTheory : Theory (Bool × Bool) :=

定义 jointTheory。组合第一坐标事实、推论规则和第二坐标的否定。

L51  union (singleton premiseP) (union (singleton premiseRule) (singleton premiseNotQ))

通过嵌套理论并集，同时持有 P、P 蕴含 Q 的规则及非 Q。

L52/- Each premise has a model, but their joint implication makes the union unsatisfiable. -/

说明 jointConflict 的预定范围。对应声明涉及：三个单项各自有模型，联合后以P及P→Q反驳¬Q，证明无共同模型。 该注释用于解释，不是证明前提。

L53theorem jointConflict :

陈述经检查的结果 jointConflict。三个单项各自有模型，联合后以P及P→Q反驳¬Q，证明无共同模型。

L54    Satisfiable (singleton premiseP) ∧ Satisfiable (singleton premiseRule) ∧

前两个结论分别为 P 与蕴含规则提供模型。

L55    Satisfiable (singleton premiseNotQ) ∧ ¬ Satisfiable jointTheory := by

还要求非 Q 单独有模型，却否定整套联合理论具有模型。

L56  refine ⟨⟨(true,true), (modelsSingleton _ _).2 rfl⟩,

给 P 提供模型 (true,true)，用 modelsSingleton 将第一坐标相等转换为所需模型证明。

L57    ⟨(false,false), (modelsSingleton _ _).2 (by intro h; cases h)⟩,

给蕴含前提提供模型 (false,false)：其第一坐标为 false，假定它为 true 即矛盾。

L58    ⟨(false,false), (modelsSingleton _ _).2 (by intro h; cases h)⟩, ?_⟩

给非 Q 提供模型 (false,false)，留下联合不可满足分支待证。

L59  rintro ⟨w, hw⟩

假定存在联合模型 w 及证明 hw，以反驳其存在。

L60  have hp := hw premiseP (Or.inl rfl)

利用 P 在联合理论中的左侧成员关系，提取实际第一坐标事实。

L61  have hr := hw premiseRule (Or.inr (Or.inl rfl))

通过规则在嵌套并集中的成员关系，提取 P 蕴含 Q。

L62  have hn := hw premiseNotQ (Or.inr (Or.inr rfl))

在同一世界，从另一个嵌套并集分支提取非 Q。

L63  exact hn (hr hp)

将规则应用于 P 得到 Q，与已提取的非 Q 矛盾。

L64/- A retraction replaces the old singleton, rather than retaining both at the same time. -/

说明 revisionSlice 的预定范围。对应声明涉及：时刻零选择真世界，其他自然数时刻选择假世界。 该注释用于解释，不是证明前提。

L65def revisionSlice (time : Nat) : Theory Bool :=

定义 revisionSlice。时刻零选择真世界，其他自然数时刻选择假世界。

L66  singleton (fun w => w = (time == 0))

只选择一个主张：世界等于测试 time=0 所得布尔值。

L67/- The initial and revised slices have models; keeping both would create a conflict. -/

说明 revisionCanReverse 的预定范围。对应声明涉及：给旧新切片各自的模型，并以真与假不可相等证明二者联合冲突。 该注释用于解释，不是证明前提。

L68theorem revisionCanReverse :

陈述经检查的结果 revisionCanReverse。给旧新切片各自的模型，并以真与假不可相等证明二者联合冲突。

L69    Satisfiable (revisionSlice 0) ∧ Satisfiable (revisionSlice 1) ∧

要求时间切片 0 与 1 各自具有模型见证。

L70    ¬ Satisfiable (union (revisionSlice 0) (revisionSlice 1)) := by

否定两者同时并集的模型，而不否定各自见证。

L71  refine ⟨⟨true, (modelsSingleton _ _).2 rfl⟩,

给时间零的单元素理论提供 true 见证。

L72    ⟨false, (modelsSingleton _ _).2 rfl⟩, ?_⟩

给时间一提供 false 见证，留下同时持有两个切片不可能的证明。

L73  rintro ⟨w, hw⟩

假定一个世界同时满足两个时间切片。

L74  have hs := (modelsUnion _ _ _).1 hw

把并集模型拆为同一世界中的时间零与时间一模型。

L75  have hp := (modelsSingleton _ _).1 hs.1

从时间零单元素理论提取共同世界等于 true。

L76  have hn := (modelsSingleton _ _).1 hs.2

从时间一单元素理论提取同一世界等于 false。

L77  have bad : true = false := hp.symm.trans hn

经由同一世界合成两个等式，推出不可能的 true = false。

L78  cases bad

消去两个不同布尔构造子之间的不可能等式。

L79/- This basic question asks whether the represented switch is on. -/

说明 onQuestion 的预定范围。对应声明涉及：唯一Unit问题询问布尔世界是否为真。 该注释用于解释，不是证明前提。

L80def onQuestion : Unit → Claim Bool := fun _ w => w = true

定义 onQuestion。唯一Unit问题询问布尔世界是否为真。

L81def assumptionContext (b : Bool) : Context Bool Unit :=

定义 assumptionContext。固定问题与全范围，只改变选择世界的假设。

L82  ⟨singleton (fun w => w = b), onQuestion, fun _ => True⟩

通过假设选择世界 b，保留相同开启问题，并令范围允许所有世界。

L83def meaningContext (b : Bool) : Context Bool Unit :=

定义 meaningContext。固定真世界假设，只改变问题的等值含义。

L84  ⟨singleton (fun w => w = true), (fun _ w => w = b), fun _ => True⟩

保持真世界假设，改为询问与 b 相等；范围仍不受限。

L85def scopeContext (b : Bool) : Context Bool Unit :=

定义 scopeContext。固定空假设和问题，只由范围选择世界。

L86  ⟨emptyTheory, onQuestion, fun w => w = b⟩

使假设为空且问题固定，仅让范围选择世界 b。

L87/- Distinct assumptions, meanings and scopes each admit opposite judgments without same-context conflict. -/

说明 contextDifferences 的预定范围。对应声明涉及：分别改变假设、含义、范围得到相反判断；所有展示上下文都有明确可接受世界。 该注释用于解释，不是证明前提。

L88theorem contextDifferences :

陈述经检查的结果 contextDifferences。分别改变假设、含义、范围得到相反判断；所有展示上下文都有明确可接受世界。

L89    (Consequence emptyTheory (assumptionContext true) () true ∧

要求在真值假设下给出肯定答案。

L90      Consequence emptyTheory (assumptionContext false) () false) ∧

要求在假值假设下给出否定答案；两者上下文不同。

L91    (Consequence emptyTheory (meaningContext true) () true ∧

要求对含义为等于 true 的问题给出肯定答案。

L92      Consequence emptyTheory (meaningContext false) () false) ∧

当同一问题改为表示等于 false 时，要求否定答案。

L93    (Consequence emptyTheory (scopeContext true) () true ∧

要求在限制为 true 的范围内给出肯定答案。

L94      Consequence emptyTheory (scopeContext false) () false) ∧

要求在另一个限制为 false 的范围内给出否定答案。

L95    (∀ b, ∃ w, Admissible emptyTheory (assumptionContext b) w) ∧

对任一假设选择，要求实际可接受世界存在。

L96    (∀ b, ∃ w, Admissible emptyTheory (meaningContext b) w) ∧

对任一问题含义，要求实际可接受世界存在。

L97    (∀ b, ∃ w, Admissible emptyTheory (scopeContext b) w) := by

对任一范围选择，要求实际可接受世界存在，并开始组合证明。

L98  have empty : ∀ w : Bool, Models emptyTheory w := by intro w p hp; cases hp

证明每个布尔世界都满足 emptyTheory，因为该理论的成员关系为 False。

L99  refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩, ⟨?_, ?_⟩, ?_, ?_, ?_⟩

拆分改变假设、含义和范围后的正反答案对，以及三类上下文的非空见证义务。

L100  · intro w h; change w = true; exact (modelsSingleton (fun x : Bool => x = true) w).1 h.2.1

在真值假设上下文中，从单元素上下文假设读出 w = true。

L101  · intro w h hp; have hn := (modelsSingleton _ _).1 h.2.1; cases hp.symm.trans hn

在假值假设上下文中，假定肯定答案会与单元素假设 w = false 矛盾。

L102  · intro w h; change w = true; exact (modelsSingleton (fun x : Bool => x = true) w).1 h.2.1

当问题含义为真值时，用固定的真世界假设确立肯定答案。

L103  · intro w h hn; have hp := (modelsSingleton _ _).1 h.2.1; cases hp.symm.trans hn

当问题含义变为假值时，假定该含义成立会与不变的真世界假设矛盾。

L104  · intro w h; exact h.2.2

在真值范围上下文中，范围组件本身给出所需肯定答案。

L105  · intro w h hp; cases hp.symm.trans h.2.2

在假值范围上下文中，肯定答案与同一世界的范围组件矛盾。

L106  · intro b; exact ⟨b, empty b, (modelsSingleton _ _).2 rfl, trivial⟩

对任一假设 b，世界 b 满足空的所持理论、该单元素假设与不受限范围。

L107  · intro b; exact ⟨true, empty true, (modelsSingleton _ _).2 rfl, trivial⟩

对任一问题含义 b，true 仍为见证，因为假设固定为 true 且范围不受限。

L108  · intro b; exact ⟨b, empty b, empty b, rfl⟩

对任一范围选择 b，世界 b 满足两个空理论，并通过相等满足所选范围。

L109/- Snapshots preserve identifiable adopted-form revisions even when semantic content agrees. -/

说明 Snapshot 的预定范围。对应声明涉及：保存同时持有理论、上下文和独立修订标识，不实现历史验证。 该注释用于解释，不是证明前提。

L110structure Snapshot (W Q : Type) where

声明数据接口 Snapshot。保存同时持有理论、上下文和独立修订标识，不实现历史验证。

L111  held : Theory W

在快照中保存同时持有主张的理论。

L112  context : Context W Q

以一个 Context 保存快照的假设、问题含义与范围。

L113  revisionIdentity : Nat

保存独立的自然数修订标识，不蕴含历史验证。

L114/- Semantic equivalence compares represented content, not its list ordering. -/

说明 SameContent 的预定范围。对应声明涉及：比较理论成员、附加假设成员及逐问题逐世界的含义和范围。 该注释用于解释，不是证明前提。

L115def SameContent {W Q : Type} (a b : Snapshot W Q) : Prop :=

定义 SameContent。比较理论成员、附加假设成员及逐问题逐世界的含义和范围。

L116  (∀ p, a.held p ↔ b.held p) ∧

要求两个快照中每个所持主张的成员关系一致。

L117  (∀ p, a.context.assumptions p ↔ b.context.assumptions p) ∧

要求每个上下文假设的成员关系一致。

L118  (∀ q w, a.context.meaning q w ↔ b.context.meaning q w) ∧

要求每个问题在每个世界具有等价含义。

L119  (∀ w, a.context.scope w ↔ b.context.scope w)

要求每个世界中的范围谓词等价。

L120/- The reporting norm covers both semantic change and independently identified revisions. -/

说明 TruthfulReport 的预定范围。对应声明涉及：内容或修订标识变化时必须报告真；不要求报告真必然有变化，也不检测变化。 该注释用于解释，不是证明前提。

L121def TruthfulReport {W Q : Type} (a b : Snapshot W Q) (reported : Bool) : Prop :=

定义 TruthfulReport。内容或修订标识变化时必须报告真；不要求报告真必然有变化，也不检测变化。

L122  (¬ SameContent a b ∨ a.revisionIdentity ≠ b.revisionIdentity) → reported = true

将如实报告定义为：内容不同或独立修订标识不同，就给出积极标记。

L123/- A real represented change and compliance entail an acknowledged change. -/

说明 semanticChangeMustBeReported 的预定范围。对应声明涉及：把给定变化证据应用于给定报告规范，得到报告为真。 该注释用于解释，不是证明前提。

L124theorem semanticChangeMustBeReported {W Q : Type} (a b : Snapshot W Q) (reported : Bool)

陈述经检查的结果 semanticChangeMustBeReported。把给定变化证据应用于给定报告规范，得到报告为真。

L125    (changed : ¬ SameContent a b ∨ a.revisionIdentity ≠ b.revisionIdentity)

假定实际发生变更：内容不同或修订标识不同。

L126    (h : TruthfulReport a b reported) : reported = true := h changed

假定报告义务，并应用于前述变更前提，得到 reported=true。

L127/- Reordering a two-claim presentation preserves the held theory extension. -/

说明 representationOrderIrrelevant 的预定范围。对应声明涉及：用析取交换律证明两个单项理论交换顺序不改变成员关系。 该注释用于解释，不是证明前提。

L128theorem representationOrderIrrelevant {W : Type} (p q : Claim W) :

陈述经检查的结果 representationOrderIrrelevant。用析取交换律证明两个单项理论交换顺序不改变成员关系。

L129    ∀ r, union (singleton p) (singleton q) r ↔ union (singleton q) (singleton p) r := by

对任意主张 r，交换 p 与 q 保持其单元素理论并集中的成员关系。

L130  intro r; exact or_comm

任取候选主张 r，利用析取交换性证明重排 p 与 q 后并集成员关系不变。

L131def contextSnapshot (c : Context Bool Unit) (revision : Nat := 0) : Snapshot Bool Unit :=

定义 contextSnapshot。将上下文包装成空持有理论的快照，默认修订标识为零。

L132  ⟨emptyTheory, c, revision⟩

构造所持主张为空、采用给定上下文及修订标识的快照。

L133/- Hiding each kind of contextual change violates the reporting interface; reporting alone supplies no truth guarantee. -/

说明 hiddenContextChangeRejected 的预定范围。对应声明涉及：分别拒绝隐瞒假设、含义、范围及标识变化，并说明报告变化不保证新假设为真。 该注释用于解释，不是证明前提。

L134theorem hiddenContextChangeRejected :

陈述经检查的结果 hiddenContextChangeRejected。分别拒绝隐瞒假设、含义、范围及标识变化，并说明报告变化不保证新假设为真。

L135    ¬ TruthfulReport (contextSnapshot (assumptionContext true)) (contextSnapshot (assumptionContext false)) false ∧

实际上下文假设从 true 变为 false 时，拒绝 false 报告。

L136    ¬ TruthfulReport (contextSnapshot (meaningContext true)) (contextSnapshot (meaningContext false)) false ∧

问题实际含义改变时，拒绝 false 报告。

L137    ¬ TruthfulReport (contextSnapshot (scopeContext true)) (contextSnapshot (scopeContext false)) false ∧

实际应用范围改变时，拒绝 false 报告。

L138    ¬ TruthfulReport (contextSnapshot (scopeContext true) 0) (contextSnapshot (scopeContext true) 1) false ∧

上下文不变但修订身份从 0 变为 1 时，拒绝 false 报告。

L139    (TruthfulReport (contextSnapshot (assumptionContext true)) (contextSnapshot (assumptionContext false)) true ∧

允许以 true 报告如实承认假设变化。

L140      ¬ Models (assumptionContext false).assumptions true) := by

但否定这些修订后的假世界假设在实际 true 处成立。

L141  have neq : (fun w : Bool => w = true) ≠ (fun w : Bool => w = false) := by

准备语义不等式：选择 true 与选择 false 的谓词是不同函数。

L142    intro h; have k := congrFun h true; have z : true = false := k.mp rfl; cases z

在 true 处计算假定的谓词相等，它会把自反成立转换为 true = false。

L143  refine ⟨?_, ?_, ?_, ?_, ?_⟩

拆出四种被拒绝的隐瞒变更，以及最后已报告但假设为假的实例。

L144  · intro h

假定隐瞒假设变化且报告为 false 仍满足 TruthfulReport，以反驳这一主张。

L145    have bad := h (Or.inl (by intro s; exact neq ((s.2.1 _).mp rfl)))

假定 SameContent 会使已改变的假设谓词相等；已知其不等，因此触发 TruthfulReport，迫使 false 标记为 true。

L146    cases bad

所需 true 报告与指定的 false 标记矛盾，因此结束这一隐瞒变更分支。

L147  · intro h

假定问题含义改变后仍可如实报告为未改变。

L148    have bad := h (Or.inl (by intro s; have z := (s.2.2.1 () true).mp rfl; cases z))

在唯一问题与 true 世界处，变化后的含义否定 SameContent；报告义务因而要求积极报告。

L149    cases bad

所需 true 报告与指定的 false 标记矛盾，因此结束这一隐瞒变更分支。

L150  · intro h

假定应用范围改变后仍能以 false 变更标记满足报告规则。

L151    have bad := h (Or.inl (by intro s; have z := (s.2.2.2 true).mp rfl; cases z))

在 true 处比较两个范围以否定 SameContent，再对这一真实范围变化应用报告义务。

L152    cases bad

所需 true 报告与指定的 false 标记矛盾，因此结束这一隐瞒变更分支。

L153  · intro h; have bad := h (Or.inr (by decide)); cases bad

不同修订身份本身就触发报告规则；即使没有内容变化，也与 false 报告矛盾。

L154  · refine ⟨fun _ => rfl, ?_⟩

构造始终积极的如实报告，另留下修订假设真实性的反证。

L155    intro h; have z := (modelsSingleton _ _).1 h; cases z

在实际世界 true 提取修订后的假世界假设；其不可能等式表明报告变更不使假设变真。

L156/- Two nonidentical resource objectives can share a feasible allocation. -/

说明 tensionWithoutContradiction 的预定范围。对应声明涉及：预算五同时满足不同上下界；预算零证明两约束谓词并不相同。 该注释用于解释，不是证明前提。

L157theorem tensionWithoutContradiction :

陈述经检查的结果 tensionWithoutContradiction。预算五同时满足不同上下界；预算零证明两约束谓词并不相同。

L158    (∃ budget : Nat, 4 ≤ budget ∧ budget ≤ 6) ∧

要求存在同时满足下界 4 与上界 6 的自然数预算。

L159    ¬ ((fun n : Nat => 4 ≤ n) = (fun n : Nat => n ≤ 6)) := by

还断言两个界限谓词不同，即使它们可以共同满足。

L160  refine ⟨⟨5, by decide, by decide⟩, ?_⟩

选择预算 5，检查两个数值界限，留下两个目标谓词不同的证明。

L161  intro h; have k := congrFun h 0; have bad : 4 ≤ 0 := k.mpr (by decide); cases bad

在预算 0 处，上界成立而下界不可能成立，因此两个目标谓词不相等。

L162/- Conflicting conclusions cannot be retained under the same consistency obligation. -/

说明 conflictRequiresChange 的预定范围。对应声明涉及：同题同条件正反后果违反一致性规范；不构造具体修复算法。 该注释用于解释，不是证明前提。

L163theorem conflictRequiresChange {W Q : Type} (t : Theory W) (c : Context W Q) (q : Q)

陈述经检查的结果 conflictRequiresChange。同题同条件正反后果违反一致性规范；不构造具体修复算法。

L164    (positive : Consequence t c q true) (negative : Consequence t c q false) :

假定同一理论、上下文与问题具有两个相反后果。

L165    ¬ Consistent t c := fun h => h q ⟨positive,negative⟩

任何 Consistent 证明都禁止给定后果对；应用这一点否定一致性，并未构造修订。

L166/- A satisfiable theory can have a false assumption at a specified actual world. -/

说明 consistentFalse 的预定范围。对应声明涉及：理论有真世界模型，却在指定假世界不成立，区分可满足与实际真。 该注释用于解释，不是证明前提。

L167theorem consistentFalse : Satisfiable (singleton (fun w : Bool => w = true)) ∧

陈述经检查的结果 consistentFalse。理论有真世界模型，却在指定假世界不成立，区分可满足与实际真。

L168    ¬ Models (singleton (fun w : Bool => w = true)) false := by

否定实际 false 满足唯一主张为 world=true 的理论。

L169  refine ⟨⟨true, (modelsSingleton _ _).2 rfl⟩, ?_⟩

提供 true 作为单元素理论的模型，另行否定实际世界 false 满足该理论。

L170  intro h; have bad := (modelsSingleton _ _).1 h; cases bad

在 false 处满足单元素理论会迫使 false = true，产生不可能的布尔等式。

L171/- The explicitly asked on/off question is undecided by the empty but inhabited theory. -/

说明 consistentIncomplete 的预定范围。对应声明涉及：空理论有模型，但指定布尔问题及其否定都不被蕴涵。 该注释用于解释，不是证明前提。

L172theorem consistentIncomplete : Satisfiable (emptyTheory : Theory Bool) ∧

陈述经检查的结果 consistentIncomplete。空理论有模型，但指定布尔问题及其否定都不被蕴涵。

L173    ¬ Entails emptyTheory (fun w : Bool => w = true) ∧

具有见证的空理论不蕴含肯定的真世界答案。

L174    ¬ Entails emptyTheory (fun w : Bool => w ≠ true) := by

它也不蕴含否定的真世界答案；分别证明这两个失败。

L175  have empty : ∀ w : Bool, Models emptyTheory w := by intro w p hp; cases hp

证明每个布尔世界都满足 emptyTheory，因为该理论的成员关系为 False。

L176  refine ⟨⟨true, empty true⟩, ?_, ?_⟩

提供非空的空理论模型，留下肯定与否定蕴含两个反证。

L177  · intro h; have bad := h false (empty false); cases bad

假定蕴含 world=true，会在空理论模型 false 处失败。

L178  · intro h; exact h true (empty true) rfl

假定蕴含 world≠true，会在空理论模型 true 处失败。

L179/- A claim can share a model with a theory without following in every model. -/

说明 compatibilityNotEntailment 的预定范围。对应声明涉及：新增主张可以与原理论相容，但原理论仍不蕴涵该主张。 该注释用于解释，不是证明前提。

L180theorem compatibilityNotEntailment :

陈述经检查的结果 compatibilityNotEntailment。新增主张可以与原理论相容，但原理论仍不蕴涵该主张。

L181    Satisfiable (union emptyTheory (singleton (fun w : Bool => w = true))) ∧

要求存在使 emptyTheory 与肯定单元素主张共同成立的模型。

L182    ¬ Entails emptyTheory (fun w : Bool => w = true) := by

仍否定 emptyTheory 本身蕴含该肯定主张。

L183  refine ⟨⟨true, (modelsUnion _ _ _).2 ⟨?_, (modelsSingleton _ _).2 rfl⟩⟩,

用世界 true 见证空理论与肯定的单元素主张相容。

L184    consistentIncomplete.2.1⟩

复用已证的空理论不能蕴含肯定主张的结果。

L185  intro p hp; cases hp

完成模型见证：没有主张能够实际属于 emptyTheory。

L187end CoreReader.Logic

关闭命名空间 CoreReader.Logic；这不增加证明或前提。