盲点: 逻辑学讲义

本书可谓是逻辑学家Jean-Yves Girard的思想之大成.

第1章 存在 vs. 本质

第1.1节 存在和本质的对立

Kubrick著名的电影2001的开场简直就是智慧的创生, 其来自于从外太空坠落的巨石, 又被赐予了一群愚笨的猴子, 那时它们还无法对付狮子, 野猪, 等等. 我们观察到:

1. 伟大的银河族 (great galactics)控制着这智慧, 其像病毒一样传播, 但是这个族群在其幼生期必然也像某种猴子一样, 因此...
2. (电影里的)智慧被视为一种绝对的属性, 独立于经验, 独立于互动, 就像是在某种预先存在的硬件之上实现的软件. 若是这巨石落在Galápagos之上的话, 爬虫或许就会统治世界: 开启乌龟时代...

对于这样一种解释的反应是明显且本能性的: 人们认为这是启发性的还是愚蠢的, 取决于他是本质主义者还是存在主义者.

第1.2节 本质主义和存在主义计划

第1.2.1小节 集合论

第1.2.2小节 Hilbert的计划 (the hilbertian project)

Hilbert纲领, 基本上刻画于1920年左右, 对应于数学的形式主义视角. 这种方式经常被简化为数学是纯粹的symbol pushing, 其意义并不比象棋游戏更多, 唯一重要的只是游戏规则的一致性. 不过, 这种挑衅不应该按照字面理解: Hilbert形式主义的背后是复杂的思考, 即便这种思考是归约主义式的. 尽管完全没有质疑集合论的旨趣, Hilbert对待集合论本质主义的方式却与集合论本身的精神背道而驰, 特别是在无限的方面. 以下是Hilbert想法的一个未经认证的版本. {译注: 大概就是作者并不能自信地声明这就是Hilbert的本意.}

1. 我们关于无限的直觉是具有误导性的; 人们讨论对象, 而人们并没有看见它们. 与之相对的是, 推理 (表达以逻辑形式化) 是真实可感的. 因此, 我们必须要明白什么是一个证明, 在其最数学的方面之下, 即形式化的; 诚然, 也就是理解它有什么用.
2. 一个证明产生一个定理$A$, 其可以在另一个证明之中(作为引理)重用, 根据类似于Modus Ponens的规则:$$\frac{AA\Rightarrow B}{B}\text{.}$$接着$B$可以作为引理用来产生$C$ (给定$B\Rightarrow C$的话), 如此可以继续下去; 这没有带来什么新的东西, 诚然如此, Modus Ponens的一个变种可以产生$$\frac{A\Rightarrow BB\Rightarrow C}{A\Rightarrow C}\text{,}$$换言之, 我们本可以在$A$和$A\Rightarrow C$之间作出一个Modus Ponens而直接得到$C$.

第1.2.3小节 Brouwer的计划

与Poincaré反对形式主义者的批评 (有时不那么公平, 但总是切中要害) 同出一源, Brouwer提出了一种对于无限的反逻辑主义的重新解读. 如今人们可以辨认出Brouwer和Hilbert的共同之处, 但是我们必须承认, 1920年代他们的关系相当紧张, 类似于牧师Don Camillo (Brouwer) 和共产主义市长Peppone (Hilbert) 之间的对立, 不过没有丝毫隐藏的同情, 障碍在于科学主义. 顺便值得一提的是, Brouwer所建立的学派, 即直觉主义, 主张直觉先于语言. Brouwer并没有拒绝无限 (与Hilbert的有限主义相对, Hilbert只将无限视为一种说话方式(façon de parler)), 但是他拒绝了无限的最Thomist (actual) 的方面; 特别是集合论以及人们可以逐点逐值定义实变量函数的想法. 一些原则在有限的论域之中是有效的, 但是在无限的情形之下不再成立, 典型的例子是排中律$A\vee \neg A$. 对于tertium non datur(意即没有第三种情况,即排中律)的通常澄清是一个公式$A$具有一个真值 (为真或者为假). 然而, 尽管人们可以在有限情形之下计算一个真值, 没有算法可以处理无限多步的验证: 这就是为什么Brouwer说无限的情形是可疑的. 这种方式是相当现代的, 意即真性 (truth) 并不独立于方法, 协议, 验证而存在; 我们应该将其与量子物理联系起来, 并忘掉主观主义, 甚至是唯我论, 有时Brouwer陷入了这歧途.

我们之后将有机会重访直觉主义, 通过线性逻辑, 其主要作为直觉主义(逻辑)的对称化版本出现. 让我们总结这次短暂的与Brouwer的相遇以两个(想象中的)对于Hilbert的驳论.

Modus Ponens:

Tertium non datur: Hilbert接受了排中律; 并非是出于他相信$A$具有一个预先存在的真值, 而是因为这简化了情况: 一种性质, 其什么也不意味, 但也没有代价. 从技术上说, 这种论证是可行的. 的确, 我们知道 (自1932: ) 经典逻辑可以被忠实地翻译为直觉主义逻辑: 每个地方 (everywhere)加上双重否定就足够了. 特别地, 排中律, 一旦被翻译为$\neg \neg (A\vee \neg A)$, 其就变成直觉主义可证的了, 因而添加这个就不再是有风险的了.

第1.3节 Gödel和自此之后

第1.3.1小节 失败和衰落

第1.A节 本质主义 vs. Plato主义 (platonism)

第2章 不完备性

第2.1节 技术性陈述

第2.1.1小节 定理的困难

第2.1.2小节 对角线论证

论证方式如下: 给定函数$g(z)$和$f(x,y)$, 我们构造$h(x)≔g(f(x,x))$; 如果碰巧$h$具有形式$h(x)=f(x,a)$, 那么我们就得到了$h(a)=f(a,a)=g(f(a,a))$; $b≔f(a,a)$是$g$的一个不动点, 这显然是意料之外的. 依据上下文, 我们可以推出各种各样的结果, 其中绝大多数都是悖论性的.

1. Cantor的paradox: $\mathbb{N}$和其幂集之间不存在双射. 如果$(X_n)$枚举了$\mathbb{N}$的子集, 并且定义$$f(m,n)≔\{\begin{array}{cc}1& ,m\in X_n\hfill \\ 0& ,\text{otherwise}\hfill \end{array}$$又定义$g(0)≔1,g(1)≔0$, 那么$g(b)=b$, 一个矛盾. {译注: 补充一下细节, 尽管可能人尽皆知. 根据序列$(X_n)$, 我们可以定义一个$\mathbb{N}$的子集$$Y≔\{m\in \mathbb{N}|m\notin X_m\}$$既然$(X_n)$枚举了$\mathbb{N}$的子集, 所以存在$a\in \mathbb{N}$满足$Y=X_a$, 那么$$f(x,a)=\{\begin{array}{cc}1& ,x\in X_a\hfill \\ 0& ,\text{otherwise}\hfill \end{array}=\{\begin{array}{cc}1& ,x\notin X_x\hfill \\ 0& ,x\in X_x\hfill \end{array}$$$$h(x)=g(f(x,x))=g\left(\{\begin{array}{cc}1& ,x\in X_x\hfill \\ 0& ,x\notin X_x\hfill \end{array}\right)=\{\begin{array}{cc}1& ,x\notin X_x\hfill \\ 0& ,x\in X_x\hfill \end{array}$$也就是说, $h(x)=f(x,a)$.}
2. Russell的antinomy: 相同的故事, $\mathbb{N}$被代之以所有集合之集合. 整数变成了任意的集合, 于是定义$$f(x,y)≔\{\begin{array}{cc}1& ,x\in y\hfill \\ 0& ,\text{otherwise}\hfill \end{array}$$而$g$和之前一样, 那么$a≔\{x|x\notin x\}$而$b≔a\in a$, 于是$a\in a\iff a\notin a$. {译注: 这里的$1$相当于真, $0$相当于假, $g$相当于否定. 以此解释, 1:相当于推出了$a\in X_a\iff a\notin X_a$.}
3. 程序的不动点: 如果$(f_n)$枚举了所有将$\mathbb{N}$送往$\mathbb{N}$的程序, 如果$g$是$f_n$中的一个, 那么前述构造可以产生$g$的一个不动点. 鉴于绝大多数函数并不具有不动点, 我们可以断言不动点往往对应于发散的计算. 典型地, 从$g(n)≔n+1$开始, $a=a+1=a+2=\cdots$, 这表明我们的确是在处理部分函数. {译注: 本来写的内容删掉了, 因为我感到存在细节问题. 对于这样一本被作者Jean-Yves Girard故意写得玄之又玄的书籍, 我只能对于缺失的细节妄加揣测. 似乎是这样, 这里的$f$是基于序列$(f_n)$的, 也就是$f(m,n)≔⟦f_n⟧(m)$. 然后, $h(x)≔⟦g⟧(f(x,x))≔⟦g⟧(⟦f_x⟧(x))$. 或许我们来到了可疑的一步, 作者大概认为存在$a\in \mathbb{N}$使得$h=⟦f_a⟧$, 于是$h(x)=⟦f_a⟧(x)=f(x,a)$. 那么, 可以推出$⟦g⟧(f(a,a))=h(a)=f(a,a)$, 即$⟦f_a⟧(a)$是$⟦g⟧$的一个不动点?}
4. $\lambda$演算的不动点: 如果$M$是一个$\lambda$项
5. 第一不完备性定理:

第2.1.3小节 编码

第3章 经典相继式: LK

第4章 直觉逻辑: LJ, NJ

第5章 函数式解释

第5.1节 证明作为函数

第5.1.1小节 证明的语义

第5.1.2小节 函数式解释

原子:

合取: $\theta$是$A\wedge B$的一个证明当且仅当$\theta$是一个序对$({\theta }_1,{\theta }_2)$, 其中${\theta }_1$是$A$的一个证明而${\theta }_2$是$B$的一个证明.

析取:

Implication: $\theta$是$A\Rightarrow B$的一个证明当且仅当$\theta$是一个应用, 其联系$A$的每个证明${\theta }^{\prime }$以$B$的一个证明$\theta ({\theta }^{\prime })$. {译注: 一般而言, 我们会将$\theta$称为一个函数.}

第5.1.3小节 盲点

这定义留下了一些盲点. 例如, 既然

第5.2节 纯$\lambda$演算

第5.3节 Curry-Howard同构

第6章 系统F

第6.1节 系统F

第7章 范畴论式解释

第8章 coherent空间

第9章 线性逻辑

第10章 perfection vs. imperfection

第11章 证明网

第12章 一个假设: 极化

第13章 设计和行为

第14章 Ludics: 重构