结构证明论

前言

本书源于我们对于无收缩规则的相继式演算的迷恋. 本书的第一部分, 从第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直至现在被称为无收缩规则的相继式演算系统. 这些逻辑学家之中的每一位都添加了一些基本的发现, 直至宝石诞生. 在当前这个阶段我们只能暗示如下: 存在一种组织证明原理的方式使得我们可以从要证明的定理出发, 然后通过分析以受引导的方式将其分为更简单的部分. 所谓的宝石正是这"受引导的方式"; 也就是说, 如果我们确定了最后的推导规则是什么, 那么最后一步的前提也就唯一确定了. 接着, 我们继续分析这些前提, 等等等等. Gentzen的基本发现可以被重述为一个证明可以安排为这样的形式, 每一步推导的前提总是比它的结论简单. (更精确地说, 也可能前提并不比结论更复杂.)

给定一个声称的定理, 问题在于它是可证的还是不可证的. 在第一种情况下, 任务是找到一个证明. 在第二种情况下, 任务是表明没有证明可以存在. 那么, 我们该如何证明不可证性呢? 这种证明的可能很大程度上依赖于拥有正确种类的演算, 而这些证明可以具有各种各样的形式: 在最简单的情况下, 我们可以遍历所有的规则, 然后发现它们的结论都不具备所声称的定理的形式. 对于特定的一类定理而言, 我们可以表明对于要证明的定理而言分析的顺序无关紧要. 每一分析步骤都会导向更为简单的前提, 因此这个过程必然终止. 根据其停下来的方式, 我们可以判断结论是否真的是一个定理, 抑或不是. 在其他情况下, 可能会出现前提至少和结论一样复杂的情形, 那么在试图找到证明的时候我们可能会无限进行下去.

第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$ . 联结词是由给定命题构造新命题的二元函数. 函数 $&$ 之于两个参数 $A$ 和 $B$ 的应用将给出作为值的命题 $& (A, B)$ , 类似的陈述对于 $\lor$ 和 $\supset$ 也是一样的. 函数式的结构通常被中缀记号与括号的舍弃所掩藏, 例如对于 $& (A, B)$ 记 $A & B$ , 诸如此类. 这将产生纯粹函数式记号所没有的歧义, 例如 $A & B \supset C$ 可能是 $& (A, \supset (B, C))$ , 也可能是 $\supset (& (A, B), C)$ . 正如之前所提及的, 对于前者我们总是记 $A & (B \supset C)$ , 对于后者我们就记 $A & B \supset C$ . 一般情况下, 合取与析取比推出结合得更为紧密. 附录A更详细地解释了从范畴文法的角度如何处理逻辑语言.

两种方法, 不论是符号序列的归纳定义还是藉由函数式应用的表达式生成, 都没有揭示逻辑语言的特别之处. 如今的逻辑语言是作为数学的非形式化语言的抽象出现的. 这个方向的第一个工作是由Frege完成的, 其发明了谓词逻辑的语言. 据Frege所言, 这个语言意在成为一个以算术为范式的用于纯粹思想的公式语言. 之后Peano和Russell进一步建立了符号化 (symbolism), 带有形式化数学语言的目的. 这些逻辑学先驱试图给出逻辑学是什么的定义, 逻辑学与数学有何不同, 以及是否后者可以归约为前者, 抑或是相反的方向是否可行.

从实际角度来看对于逻辑语言是什么存在着清晰的理解: 主要的逻辑语言就是命题逻辑和谓词逻辑的语言. 然后, 存在着许多其他的逻辑语言与它们有着或多或少的联系. 从这个角度来看, 逻辑学本身是逻辑学家所研究和建立的东西. 任何对于逻辑和逻辑语言的一般定义都应该尊重这种情况.

逻辑语言的一个本质方面在于它们是形式语言, 或者很容易变成形式语言, 计算机科学的建立使得这一方面变得愈发重要. 逻辑语言和编程语言之间存在着许多联系; 实际上, 在近来的某些发展里逻辑语言和编程语言融为一体了, 见附录B的解释.

(b) 推理规则: 推理规则具有这样的形式: 如果是 $A$ 和 $B$ (成立)的情形, 那么也是 $C$ (成立)的情形. 因此, 它们并不在命题上操作, 而是在断言上操作. 我们通过给一个命题 $A$ 添加点什么东西来得到一个断言, 即一个断言语气 (assertive mood), 例如 $A$ (成立)的情形 (it is the case that $A$ ). Frege使用断言符号 $⊢ A$ 来指明这一点, 然而通常命题和断言的区分是保持隐式的. 规则似乎是从给定的命题流向新的命题.

在Hilbert风格的系统里 (其也被称为公理系统 (axiomatic system)), 我们拥有许多基本的断言形式, 例如 $⊢ A \supset A \lor B$ 和 $⊢ A \supset (B \supset A)$ . 这些形式的每个实例都可以被断言, 而在命题逻辑的情况下, 这里只有一条推理规则, 其具有形式 $\frac{⊢ A \supset B ⊢ A}{⊢ B}$ 推导从公理的实例开始, 经由规则不断分解, 直至抵达想要的结论.

在自然演绎系统里, 这里只有推理规则, 外加推动推导开始的假设, 例如 $\frac{⊢ A ⊢ B}{⊢ A & B} \frac{\begin{matrix} [⊢ A] \\ ⋮ \\ ⊢ B \end{matrix}}{⊢ A \supset B}$ 第一条规则的实例是单步推理, 并且如果前提由某些假设所推导出来, 那么结论依赖于相同的假设. 而在第二条规则里, 竖着的点指明了一个从 $⊢ A$ 到 $⊢ B$ 的推导, 假设 $⊢ A$ 在推理线处被解除 (discharge), 如方括号所指示的那样, 于是推理线上面的 $⊢ B$ 依赖于 $⊢ A$ 而下面的 $⊢ A \supset B$ 则并不依赖.

在相继式演算系统中, 并不存在会被解除的临时假设, 但是会显式列出被推导出来的断言所依赖的假设. 可推导性这个关系 (在自然演绎里的参照是这些竖着的点), 是形式语言的一个显式部分, 并且相继式演算可以视为可推导性关系的一种形式理论.

这三种类型的系统里, 第一种这个公理系统由于只有一条推理规则而拥有一些良好的性质. 然而, 实际使用公理方法近乎于不可能, 因为找到作为起点的公理实例太过困难了. 第二种类型的系统对应于在数学里进行推理的通常方式, 带有很好的结构感觉. 第三种类型的系统使得对于证明的结构的最为深远的分析成为可能, 但是实际使用需要一些练习. 另外, 以下事情在自然演绎和相继式演算中都是可能发生的:

两个规则系统是等价的, 如果两个系统能够推导出相同的断言, 但是对于每个系统添加相同的规则可能导致等价性的破坏.

这种模块性的缺乏不会在公理性的Hilbert风格系统中出现. {译注: 所谓规则系统, 大概公理(模式)被视为了无前提的规则.}

一旦某个逻辑推理的规则系统建立好了, 我们就可以从形式化的角度来看待它. 可以省略断言符号, 而推理规则不过就是在一个或者若干公式下面书写某个公式的方法, 这里要求前者应该具有规则的前提的形式. 在一种对于逻辑的完备形式化中, 命题的构成 (formation) 也会被呈现为命题构成规则的应用. 例如, 合取的构成是以下规则的应用: $\frac{A : Prop B : Prop}{A & B : Prop}$ 推理规则可以和命题构成规则以相同的方式形式化: 它们可以被表示为函数, 其接受前提的形式证明作为参数, 然后给出结论的一个形式证明作为值. 一个函数式范畴的层次结构由此获得以至于所有的命题构成规则和推理规则的实例都经由函数式应用而显现. 这将会导致构造类型论 (constructive type theory), 附录B有更详细的描述.

证明论的观念在于逻辑学是关于正确论证推理的理论. 推理被分析(分解)为最为基本的步骤, 而这些基本步骤的正确性可以得到轻易的控制. 而且, 推理的语义澄清是可复合的, 藉由单独的推理步骤的澄清以及推理步骤的组合方式而实现.

复合推理由基本推理步骤的复合所合成 (synthesize). 一个推理规则系统是用来给出推导 (derivation)的概念的一个归纳性的形式化的定义的. 然后, 可推导性意味着一个推导的存在性. 一个给定推导的正确性可以机械地藉由其归纳定义进行控制, 但是推导的寻找通常就是一件完全不同的事情了.

第1.2节自然演绎

自然演绎体现了逻辑联结词和量词的操作性或者说计算性含义. 含义的解释是基于断言相应形式的命题的直接根据 (immediate grounds)给出的. 可以有其他的不那么直接的根据, 但是这种根据应该要能够归约至前者, 这是为了使得一致 (coherent) 的操作语义成为可能. BHK条件 (BHK代表Brouwer-Heyting-Kolmogorov) 基于命题的直接可证明性给出了命题逻辑的逻辑联结词的解释, 其可以表述如下:

$A & B$ 的一个直接证明由命题 $A$ 的一个证明和命题 $B$ 的一个证明构成.
$A \lor B$ 的一个直接证明由命题 $A$ 的一个证明或命题 $B$ 的一个证明构成.
$A \supset B$ 的一个直接证明由根据存在命题 $A$ 的一个证明的假设而来的命题 $B$ 的一个证明构成. {译注: 更多的人喜欢将其表述成将命题 $A$ 的证明转换为命题 $B$ 的证明的函数.}
$⊥$ 的一个直接证明是不可能的.

在第三种情形下, 我们只是假定存在

A

的一个证明, 但是结论

A \supset B

的证明并不依赖于这个假设, 其只是为了将

B

的证明归约为对于

A

的一个证明而临时作成的. 这里的证明是一个非形式化的概念. 我们会逐渐将其替代为一个给定规则系统中的可推导性的形式概念.

现在我们可以将作用于断言的推理规则的想法精确化, 即一个断言得到保证如果存在一个可用的证明. 因此在形式化层面, 推理规则作用于前提的推导上, 产生作为值的对于结论的一个推导. 从BHK解释的角度, 我们抵达了如下的引入规则 (introduction rule): $\frac{A B}{A & B} & I \frac{A}{A \lor B} \lor I_{1} \frac{B}{A \lor B} \lor I_{2} \frac{\begin{matrix} [A] \\ ⋮ \\ B \end{matrix}}{A \supset B} \supset I$ 断言符号我们就省略了. (很快这个符号还有其他用处.) 在最后一条规则里, 辅助的假设 $A$ 在推理时会被解除, 这是由方括号所指明的. 作为推出的引入规则的一个特别情形, 在 $B = ⊥$ 时, 其是否定的引入规则. $⊥$ 的话则没有引入规则.

对应于引入规则存在着消去规则 (elimination rule). 这些规则都有三种形式 (合取, 析取, 推出) 之一的命题作为主前提 (major premise). 存在着一般的原理帮助我们寻找消去规则: 我们要问在假定主前提已经有推导了的情况下, 还需要什么条件才能满足以下要求:

逆转原理 (inversion principle): 一切可从用于推导某个命题的直接证据中所推出的, 都必然可从这个命题推出.

对于合取

A & B

而言, 其直接证据是我们拥有一个对于

A

的推导和一个对于

B

的推导. 对于假定

A

和

B

则能推出的

C

, 那么我们根据逆转原理由此发现了消去规则

\frac{A & B \begin{matrix} [A, B] \\ ⋮ \\ C \end{matrix}}{C} & E

C

被推导所用的假设

A

和

B

在推理处被解除. 如果在一个推导里引入规则的前提

A

和

B

已经被推导出来, 而

C

又已经由

A

和

B

推导出来, 以下推导

\frac{\frac{\begin{matrix} ⋮ \\ A \end{matrix} \begin{matrix} ⋮ \\ B \end{matrix}}{A & B} & I \begin{matrix} [A, B] \\ ⋮ \\ C \end{matrix}}{C} & E

可以转换 (convert)为一个没有引入和消去规则的对于

C

的推导

\begin{matrix} \begin{matrix} \begin{matrix} ⋮ \\ A \end{matrix} & \begin{matrix} ⋮ \\ B \end{matrix} \end{matrix} \\ \begin{matrix} ⋮ \\ C \end{matrix} \end{matrix}

因此, 如果

& I

后面接着

& E

, 推导就可以被简化.

对于析取, 我们有两种情况. 要么 $A \lor B$ 是由 $A$ 所推导出来的而 $C$ 可由假设 $A$ 推导, 要么 $A \lor B$ 是由 $B$ 所推导出来的而 $C$ 可由假设 $B$ 推导. 考虑到两种情况都有可能, 我们发现了以下消去规则 $\frac{A \lor B \begin{matrix} [A] \\ ⋮ \\ C \end{matrix} \begin{matrix} [B] \\ ⋮ \\ C \end{matrix}}{C} \lor E$ 假定 $A$ 或 $B$ (其中至少一个)已经被推导出来了. 如果是前者, 并且如果 $C$ 可由 $A$ 推导且 $C$ 可由 $B$ 推导, 那么以下推导 $\frac{\frac{\begin{matrix} ⋮ \\ A \end{matrix}}{A \lor B} \lor I_{1} \begin{matrix} [A] \\ ⋮ \\ C \end{matrix} \begin{matrix} [B] \\ ⋮ \\ C \end{matrix}}{C} \lor E$ 可以转换为一个没有引入规则和消去规则的对于 $C$ 的推导 $\begin{matrix} \begin{matrix} ⋮ \\ A \end{matrix} \\ \begin{matrix} ⋮ \\ C \end{matrix} \end{matrix}$ 如果是后者 $B$ 已经被推导出来的情况, 那么可以转换为 $\begin{matrix} \begin{matrix} ⋮ \\ B \end{matrix} \\ \begin{matrix} ⋮ \\ C \end{matrix} \end{matrix}$ 又一次, 后面跟着相应消去的引入是可以从推导中移除的.

推出的消去规则更难找到. 推导 $A \supset B$ 的直接证据是根据假设 $A$ 而来的对于 $B$ 的假想 (hypothetical)推导. $C$ 可从这样一个推导地存在性所推导出来的事实可以表达为:

如果 $C$ 可由 $B$ 推出, 那么其已经可由 $A$ 推出.

这恰是由以下消去规则所完成的:

\frac{A \supset B A \begin{matrix} [B] \\ ⋮ \\ C \end{matrix}}{C} \supset E

除了主前提

A \supset B

之外,

\supset E

中存在着副前提 (minor premise)

A

. 如果

B

已经由

A

所推出,

C

已由

B

推出, 推导

\frac{\frac{\begin{matrix} [A] \\ ⋮ \\ B \end{matrix}}{A \supset B} \supset I \begin{matrix} ⋮ \\ A \end{matrix} \begin{matrix} [B] \\ ⋮ \\ C \end{matrix}}{C} \supset E

可由转换为一个没有引入和消去规则的由

A

得到

C

的推导, 即

\begin{matrix} \begin{matrix} ⋮ \\ A \end{matrix} \\ \begin{matrix} ⋮ \\ B \end{matrix} \\ \begin{matrix} ⋮ \\ C \end{matrix} \end{matrix}

最后, 我们有一个零元联结词

⊥

, 其没有引入规则. 鉴于推导

⊥

的直接证据为空, 我们得到了谬消去规则 (falsity elimination) (ex falso quodlibet) 作为逆转原理的一个受限情形, 其只有主前提

⊥

\frac{⊥}{C} ⊥ E

我们仍然还需要说明如何开始推导. 这是由假设规则 (rule of assumption)所完成的, 其允许我们从任意公式开始一个推导. 在一个推导树里, 这些公式的出现是假设, 或者更准确地说, 是开假设, 其既不是结论也没有被任何规则解除. 被解除的假设也被称为闭假设.

规则 $& E$ 和 $\supset E$ 通常只针对于特别情形而写下来, 对于 $& E$ 而言是 $C = A$ 和 $C = B$ 两种情况, 对于 $\supset E$ 而言是 $C = B$ 的情况, 如以下规则所阐明: $\frac{A & B}{A} & E_{1} \frac{A & B}{B} & E_{2} \frac{A \supset B A}{B} \supset E$ 这些特别的消去规则对应于更加受限的逆转原理, 其要求消去规则的结论应该是推导出命题的直接证据, 而不可以是这些证据的任意推论. 这里的前两条规则只是以合取的引入的前提作结. 第三条规则给出了从 $A$ 到 $B$ 的一步推导, 根据通常称作modus ponens的规则. 更受限的逆转原理对于澄清特别的消去规则是足够了, 但对于确定消去规则应该是什么还不行. 一个特定的例子是它对于 $⊥ E$ 什么也没有说.

特别的消去规则有着这样的性质, 其结论是它们的前提的直接子公式 (immediate subformula). 对于合取的引入, 相当于转了个方向: 前提是结论的直接子公式. 更进一步, 对于推出的引入而言, 推理线上方的公式是其结论的一个直接子公式. 可以证明使用合取与推出的引入以及特别的消去规则的推导, 可以被转换为一个规范形式 (normal form). 这个是通过迂回消解 (detour conversion)完成的, 即移除引入规则后面跟着相应的消去规则这种规则应用的情况. 在处于规范形式的带有特别消去规则的推导里, 首先是作出假设, 然后是使用消去规则, 最后是使用引入规则. 这种关于规范推导的简单图景, 即由消去规则从假设移动至直接子公式, 然后再由引入规则向着相反方向移动, 会因为析取的消去规则而失去. 然而, 当所有的消去规则都已一般形式表述时, 规范形式的自然演绎推导就能达成一致的子公式结构. 规范形式本身则是由以下性质所刻画的:

具有一般消去规则的自然演绎的一个推导处于规范形式, 如果所有的消去规则的主前提都是假设.

一般而言, 自然演绎系统不必保证可以转换至规范形式, 但是结构证明论的目的是找到这样的系统. 存在着一系列和规范形式相关的强度逐步递增的性质, 其中最弱的性质是规范形式的存在性. 这个性质所陈述的是如果一个公式

A

在某个系统中是可推导的, 那么也存在一个规范形式的对于

A

的推导. 接着, 我们有规范化 (normalization)的概念: 一个实际将任何给定推导转换为规范形式的过程. 接下来的概念是强规范化 (strong normalization): 对于非规范推导以任意顺序应用转换总会在一些步骤之后终止于一个规范形式的推导. 最后, 我们还有规范形式的唯一性的概念: 对于一个给定的推导进行规范化过程总是终止于相同的规范证明. 注意到这并不是说只存在一个公式的规范推导, 因为对于不同的非规范推导而言一般来说它会终止于不同的规范推导.

合取与析取的引入规则, 以及合取与推出的特别消去规则, 都是简单的单步推理. 剩下来的规则是schematic的, 带有垂直的点指出存在带有假设的推导. 这些假设的行为是由解除函数 (discharge function)所控制的: 每个假设都被分配了一个编号, 而假设的解除是由将编号写在推理线旁边所指明的. 更进一步, 解除是可选的, 即我们可以, 或者说有时不得不, 将一个假设留作开的, 即便它可以被解除.

以下一些例子将会刻画假设的管理, 并指出自然演绎推导的一些古怪之处.

结构证明论

前言

导引