Skip to content

Commit 4edf4f2

Browse files
lizixi-0x2Fclaude
lizixi-0x2F
and
claude
committed
完成下卷全部九章（ch14-ch22）正式发布
- 新增 ch18 因果结构的形式化（三层阶梯、SCM、do-calculus、d-分离、反事实） - 新增 ch19 复杂度作为推理的几何（P/NP、NP完全、停机问题、Oracle分离） - 新增 ch20 启发式的形式合同（可采纳性、一致性、近似比、PAC学习） - 新增 ch21 学习作为逆推断（Kolmogorov复杂度、MDL、泛化=压缩） - 新增 ch22 自指与涌现（Curry-Howard对应、不动点、依赖类型、AI推理边界） - 串联叙事主线：改写 ch14-ch17 各章悬而未决，焊死章节间逻辑接驳 - 改写 ch16 开头：从哥德尔余温直接引出收缩规则的质疑 - 全九章插入兔狲教授评（共20条），风格：直接、有态度、对懒惰思维不客气 - 更新 README 下卷状态 🔨→✅，对齐实际章节标题 - 更新 sidebar config 章节标题与正文一致 Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 7f5f84e commit 4edf4f2

File tree

11 files changed

+1439
-29
lines changed

11 files changed

+1439
-29
lines changed

‎README.md‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -61,15 +61,15 @@ https://datawhalechina.github.io/reasoning-kingdom
6161

6262
| 章节 | 简介 | 状态 |
6363
| :---- | :---- | :----: |
64-
| [第14章：形式系统——推理的语法](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter14/) | 命题、推断规则、公理、证明；句法与语义的根本分离 | ✅ |
64+
| [第14章：形式系统——给推理一个地基](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter14/) | 命题、推断规则、公理、证明；句法与语义的根本分离 | ✅ |
6565
| [第15章：一致性与完备性——形式系统的两堵墙](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter15/) | 哥德尔两个不完备定理：真与可证永远不会完全重合 | ✅ |
66-
| [第16章：线性逻辑与资源——每个假设只能用一次](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter16/) | 去掉收缩规则，推理变成资源管理 | 🔨 |
67-
| [第17章：概率作为逻辑的扩张——真值从 {0,1} 到 [0,1]](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter17/) | Cox公理：理性信念的唯一相容表示就是概率论 | 🔨 |
68-
| [第18章：因果结构的形式化——三层阶梯与 do-calculus](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter18/) | Pearl因果阶梯的形式化：观测、干预、反事实 | 🔨 |
69-
| [第19章：复杂度作为推理的几何——问题的内在结构](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter19/) | 推导树深度=时间复杂度；停机问题与哥德尔重新相遇 | 🔨 |
70-
| [第20章：启发式的形式合同——"差不多对"的精确定义](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter20/) | 可采纳性、一致性、PAC学习：近似推理的数学保证 | 🔨 |
71-
| [第21章：学习作为逆推断——泛化是压缩的另一种说法](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter21/) | Kolmogorov复杂度、MDL原理：泛化=压缩 | 🔨 |
72-
| [第22章：自指与涌现——当推理系统推理关于自身](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter22/) | Curry-Howard对应、不动点定理、Transformer的形式猜想 | 🔨 |
66+
| [第16章：线性逻辑与资源——每个假设只能用一次](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter16/) | 去掉收缩规则，推理变成资源管理 | ✅ |
67+
| [第17章：概率作为逻辑的扩张——真值从 {0,1} 到 [0,1]](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter17/) | Cox公理：理性信念的唯一相容表示就是概率论 | ✅ |
68+
| [第18章：因果结构的形式化——三层阶梯与 do-calculus](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter18/) | Pearl因果阶梯的形式化：观测、干预、反事实 | ✅ |
69+
| [第19章：复杂度作为推理的几何——为什么有些推理根本不能被加速](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter19/) | 推导树深度=时间复杂度；停机问题与哥德尔重新相遇 | ✅ |
70+
| [第20章：启发式的形式合同——"差不多对"的精确数学定义](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter20/) | 可采纳性、一致性、PAC学习：近似推理的数学保证 | ✅ |
71+
| [第21章：学习作为逆推断——泛化是压缩的另一种说法](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter21/) | Kolmogorov复杂度、MDL原理：泛化=压缩 | ✅ |
72+
| [第22章：自指与涌现——当推理系统开始推理关于自身](https://datawhalechina.github.io/reasoning-kingdom/volume2/chapter22/) | Curry-Howard对应、不动点定理、Transformer的形式猜想 | ✅ |
7373

7474
## 贡献者名单
7575

‎docs/.vitepress/config.mts‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -67,15 +67,15 @@ export default defineConfig({
6767
{
6868
text: '下卷：推理的形式演绎',
6969
items: [
70-
{ text: '第14章：形式系统——推理的语法', link: '/volume2/chapter14/' },
70+
{ text: '第14章：形式系统——给推理一个地基', link: '/volume2/chapter14/' },
7171
{ text: '第15章：一致性与完备性——形式系统的两堵墙', link: '/volume2/chapter15/' },
7272
{ text: '第16章：线性逻辑与资源——每个假设只能用一次', link: '/volume2/chapter16/' },
7373
{ text: '第17章：概率作为逻辑的扩张——真值从 {0,1} 到 [0,1]', link: '/volume2/chapter17/' },
7474
{ text: '第18章：因果结构的形式化——三层阶梯与 do-calculus', link: '/volume2/chapter18/' },
75-
{ text: '第19章：复杂度作为推理的几何——问题的内在结构', link: '/volume2/chapter19/' },
76-
{ text: '第20章：启发式的形式合同——"差不多对"的精确定义', link: '/volume2/chapter20/' },
75+
{ text: '第19章：复杂度作为推理的几何——为什么有些推理根本不能被加速', link: '/volume2/chapter19/' },
76+
{ text: '第20章：启发式的形式合同——"差不多对"的精确数学定义', link: '/volume2/chapter20/' },
7777
{ text: '第21章：学习作为逆推断——泛化是压缩的另一种说法', link: '/volume2/chapter21/' },
78-
{ text: '第22章：自指与涌现——当推理系统推理关于自身', link: '/volume2/chapter22/' },
78+
{ text: '第22章：自指与涌现——当推理系统开始推理关于自身', link: '/volume2/chapter22/' },
7979
]
8080
}
8181
],

‎docs/volume2/chapter14/index.md‎

Lines changed: 29 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,10 @@
2626

2727
形式化的目的不是让语言变得难看，而是**消除歧义**。我们需要一套符号，每个符号只有一个含义，由定义给出，不依赖语境，不依赖常识。
2828

29+
::: info 兔狲教授评
30+
常识不是数学，这句话说得很好。但别以为形式化就是把常识翻译成符号。形式化是在强迫你承认：你那些"显然"里藏着多少从没想清楚的东西。符号只是逼你原形毕露的工具，不是答案本身。就这样。
31+
:::
32+
2933
---
3034

3135
## 14.2 命题：推理的原材料
@@ -44,6 +48,10 @@
4448

4549
这些符号的含义由精确的规则给出，不是约定俗成的。$P \to Q$ 的意思不是"$P$ 导致 $Q$"，不是"$P$ 在时间上先于 $Q$"，而只是：**不存在 $P$ 为真而 $Q$ 为假的情况**。这个定义可能比你的直觉更冷酷——"如果月亮是方的，那么 2 + 2 = 5"在这个定义下是真命题——但正是这种冷酷让数学推理成为可能。
4650

51+
::: info 为什么接受这个反直觉的定义？
52+
逻辑连接词不是在描述因果，而是在**约束推断的合法性**。$P \to Q$ 的问题是：如果你接受了 $P$，你是否被迫也要接受 $Q$？只有在 $P$ 为真、$Q$ 为假时，答案才是否定的——所以那是唯一要排除的情况。前件为假时，蕴含式不构成任何约束，整体视为真。代价是"真命题"不再等于"有意义的命题"。这个代价，数学家认为值得付。
53+
:::
54+
4755
---
4856

4957
## 14.3 形式系统：给推理划定游戏规则
@@ -76,10 +84,18 @@ $$\frac{P \to Q \qquad P}{Q}$$
7684

7785
这意味着什么？它意味着一台机器——不理解数学，不知道"真"是什么意思，只会做符号匹配——可以验证任何形式证明的正确性。现代定理证明助手（Lean、Coq、Isabelle）正是这样工作的：你写证明，机器检查符号。
7886

87+
::: info 验证 vs. 发现
88+
注意这里的非对称性。**验证**一个证明是机械的，多项式时间可完成——只需逐步检查每条推断规则是否合法。**发现**一个证明是另一回事：没有通用算法能在任意情形下保证找到证明（第15章会说明这是不可能的）。这个不对称性贯穿整个可计算性理论，也是"NP问题"令人困惑的根源之一。
89+
:::
90+
7991
这不是数学的终结，而是数学的一个深刻特性：**数学真理是可以被机械验证的**。我们不必依赖权威，不必信任直觉，只需要检查符号串。
8092

8193
当然，想出证明的过程——发现正确的推断路径——不是机械的，也许永远不会是。但验证是机械的，这一点已经足够深刻。
8294

95+
::: info 兔狲教授评
96+
这里容易飘。"机器可以验证证明"不等于"机器理解了证明"。验证是对符号串做模式匹配，和"理解"没有关系。把"可机械验证"当成数学的荣耀来讲，你得先想清楚你在夸的到底是什么。验证的是形式，不是意义。
97+
:::
98+
8399
---
84100

85101
## 14.5 上下文：假设的簿记
@@ -100,6 +116,14 @@ $\Gamma \vdash A$ 读作：在假设集 $\Gamma$ 下，$A$ 可被推导出来。
100116

101117
这三条规则在经典逻辑里是理所当然的——资源无限，顺序无关。但第16章会拿走收缩规则，这一改动会让整个逻辑的性质发生根本变化：每个假设恰好只能用一次，推理变成了资源管理。
102118

119+
::: info 兔狲教授评
120+
大多数人学了十年逻辑，从来不知道自己一直在默默使用这三条规则。这不是额外知识，这是你推理的地基。你连地基是什么都不知道，就在上面盖楼——盖出来的东西你自己都不知道为什么能站。名字的缺席，不等于它们不存在。
121+
:::
122+
123+
::: info 这三条规则为什么值得命名？
124+
因为它们并不是"逻辑本身"，而是**关于逻辑的元选择**——选择了它们，你得到经典逻辑；拒绝它们中的某一条，你得到不同的逻辑体系。大多数数学课完全不提这三条规则，因为在经典语境下它们从不违反。但正是这种"不言而喻"掩盖了逻辑的可选择性。形式系统能做的事情之一，就是让这些隐藏的选择变得可见。
125+
:::
126+
103127
---
104128

105129
## 14.6 语义：符号背后的含义
@@ -139,6 +163,10 @@ $\Gamma \vdash A$ 读作：在假设集 $\Gamma$ 下，$A$ 可被推导出来。
139163

140164
这个层级有一个规律：越强的系统，表达能力越大，但自我验证的能力越小。命题逻辑简单到可以穷举检查自身；皮亚诺算术强大到连自身的一致性都无法证明。强大有强大的代价。这个代价，正是下一章要算清楚的账。
141165

166+
::: info 为什么"更强"会带来自我验证的失能？
167+
直觉上：一个足够强的系统能谈论自己，而一旦能谈论自己，就能构造关于自身的悖论性陈述。弱的系统无法表达"我自己的命题"，所以不会遇到这个问题。这就像语言一样——越表达能力丰富的语言，越容易产生自指悖论；简单的形式语言，恰恰因为无法自我指涉而安全。哥德尔发现的不是数学的缺陷，而是表达能力的内在代价。
168+
:::
169+
142170
---
143171

144172
## 悬而未决
@@ -147,7 +175,7 @@ $\Gamma \vdash A$ 读作：在假设集 $\Gamma$ 下，$A$ 可被推导出来。
147175

148176
**公理的选择是客观的吗？** 不同的公理集合给出不同的数学宇宙。选择公理——ZFC 里最有争议的公理——并非"显然"正确，数学家们为此争论了一个世纪。形式化把这个争论变得更清晰了，但并没有解决它。
149177

150-
**证明的长度有意义吗？** 有些真命题的最短证明长得惊人——比它们的内容复杂得多。这暗示着证明的复杂度和命题本身的复杂度之间有某种深刻的关系。这个关系在第19章展开。
178+
**这台机器可靠吗？完备吗？** 我们建造了形式系统，描述了它的语言、公理、推断规则，也区分了句法和语义。但有一个问题我们一直没有正面回答：它证明出来的东西，都是真的吗？所有真的东西，它都能证明吗？这两个问题的答案，一个令人欣慰，另一个令人震惊。第15章正面处理它们。
151179

152180
---
153181

0 commit comments

Comments
 (0)