结构证明论

前言

本书源于我们对于无收缩规则的相继式演算的迷恋. 本书的第一部分, 从第1章到第4章, 是基于这种演算的对于直觉主义谓词逻辑和古典谓词逻辑的介绍. 本书的第二部分, 从第5章到第8章, 主要呈现了我们自己的工作, 其利用了对于证明的控制, 而这是因为无收缩规则的演算才成为可能.

导引

结构证明论

数学证明的想法非常古老, 尽管精确的证明原则大概只是在过去数百年间才确定下来的. 证明论最初是基于只有一到两个推理规则的公理系统的. 这样的系统作为对于什么是可证明的形式呈现而言可能是有用的, 然而在公理系统中实际发现证明近乎是不可能的. 一个证明从公理的实例开始, 但是并不存在找出这些实例应该是什么的系统方法. 公理证明论最初由David Hilbert建立, 其目的在于研究数学公理系统的一致性, 相互独立性以及完备性.

结构证明论研究数学证明的一般结构和性质. 其由Gerhard Gentzen (1909-1945) 于1930年代初发现并在其1933年的博士论文Untersuchungen über das logische Schliessen中呈现. 在他的论文里, Gentzen给出了对于逻辑规则系统两种主要的形式化, 自然演绎和相继式演算. 前者意在提供定理证明实践的一种近似对应; 而后者, Gentzen通过这种形式化发现了其主要的结果, 其经常被引用为Gentzen的"Hauptsatz". 它是在说证明可以被转换为一种特定的"无切"形式, 而从这种形式可以得到关于证明的一般性结论, 例如规则系统的一致性.

Gentzen开始他的研究的年代发生了一件标志性的大事, 这是一项伟大但却令人费解的发现, 即1931年算术的Gödel不完备性定理: 已知的证明原则不足以推导出算术的一切; 而且, 没有单一的公理和规则系统可以满足此要求. Gentzen对于算术的证明论研究产生了序数证明论, 其主要任务在于研究包含无穷多证明原则的形式系统的演绎强度. 这一部分的证明论我们将不作讨论.

对于Gentzen在其博士论文中给出的两种形式的结构证明论, 自然演绎对于证明规则的处理仍然保持了显著的稳定性, 然而相继式演算却沿着各种不同的方向进行发展. 其中一种发展方向, 自Gentzen始经由Ketonen, Kleene, Dragalin, Troelstra直至现在被称为无收缩规则的相继式演算系统. 这些逻辑学家之中的每一位都添加了一些基本的发现, 直至宝石诞生. 在当前这个阶段我们只能暗示如下: 存在一种组织证明原理的方式使得我们可以从要证明的定理出发, 然后通过分析以受引导的方式将其分为更简单的部分. 所谓的宝石正是这"受引导的方式"; 也就是说, 如果我们确定了最后的推导规则是什么, 那么最后一步的前提也就确定了.

第1章从自然演绎到相继式演算

第1.1节逻辑系统

一个逻辑系统由一个形式语言和一个用于进行逻辑推理的公理和规则系统构成.

(a) 逻辑语言: 一个逻辑语言经常通过一集归纳语句被定义为合式公式. 想法在于形式语言的表达式是来源于某个给定的字母表的符号的特定序列, 由归纳定义生成. 另一种定义形式语言的方法是通过范畴文法. 这样的文法对于自然语言领域而言是众所周知的, 亦用于编程语言, 但在逻辑学中不那么常见.

在第一种方法下, 逻辑语言的表达式是由两种语句归纳定义的公式: 1. 陈述何为基本 (prime) 公式. 这些公式不包含其他公式作为其一部分. 2. 陈述何为复合 (compound) 公式. 这些公式由更简单的公式通过逻辑联结词构造, 并且其定义需要引用任意的公式, 以及说明这些公式是如何与逻辑联结词的符号放在一起以给出新的公式的. 给定一个公式, 我们可以找出其是如何由其他公式和逻辑联结词放在一起的. 或许括号对于唯一地指明复合的方式而言是必要的, 然后我们可以明白如何得到公式的各个部分, 直至抵达基本公式. 因此, 到最后, 所有公式都是由基本公式, 逻辑联结词和括号构成的.

我们将定义命题逻辑的语言:

基本公式是记作 $P, Q, R, \dots$ 的原子公式和记作 $⊥$ 的谬.
如果 $A$ 和 $B$ 是公式, 那么合取 $A & B$ , 析取 $A \lor B$ 和推论 $A \supset B$ 也是公式.

为了公式的unique readability, 公式的部分 (component) 应该被置于括号里, 然而在实践中, 若合取和析取是推论的部分, 括号则通常被省略. 往往

⊥

被当作原子公式, 但是在证明论中最好将其视为零元联结词. 否定

\sim A

和等价

A \supset\subset B

分别被定义为

\sim A = A \supset ⊥

和

A \supset\subset B = (A \supset B) & (B \supset A)

语言的表达式应该表达什么东西, 而不仅仅是以正确方式放在一起的来源于某个字母表的符号的序列. 在逻辑学中, 这样所表达的东西被称为命题. 往往人们并不说"由公式 $A$ 表达的命题", 而仅仅是说"命题 $A$ ". 在哲学中对于命题究竟是什么存在着长期的争辩. 当重心在逻辑学上, 而不是在哲学分析下的逻辑是什么上的时候, 我们以形式上的意义考虑表达式, 讨论公式.

在近来的文献中, 将表达式定义为符号序列被称为是具体句法. 往往从另一个角度看待表达式是有用的, 即抽象句法的角度, 如在范畴文法中. 范畴文法的基本想法在于语言的表达式拥有一种函数式结构 (functional structure). 例如, 英语句子 $John walks$ 可以藉由将不及物动词 $walk$ 表示为从名词词组范畴 $NP$ 到句子范畴 $S$ 的函数得到, 在通常的函数记号下即 $walk : NP \to S$ . $John$ 是范畴 $NP$ 的一个元素, 而将函数 $walk$ 应用于它则得到了作为值的 $walk (John)$ , 这是句子范畴 $S$ 的一个元素. 为了隐藏函数式的结构以生成原本的句子 $John walks$ , 更进一步的线性化是必要的. 在逻辑学和数学中, 这最后阶段产生的不同无足轻重. 自Frege始, 人们只考虑函数式结构的逻辑内容.

我们将简要从范畴文法的角度看看命题逻辑语言的定义. 存在一个命题的基本范畴, 记作 $Prop$ . 原子命题是作为参数 $P, Q, R, \dots$ 被引入的, 其无结构, 带有范畴化 $P : Prop, Q : Prop, R : Prop, \dots$ 谬也是类似的, $⊥ : Prop$ . 联结词是由给定命题构造新命题的二元函数.

结构证明论

前言

导引