自然数上与公式上的归纳法

摘要

命题逻辑的公式有无穷多个，任何关于全部公式的断言，都需要一种不靠逐个检查的方法。本课分两层构建这种方法。第一层是自然数上的归纳法，有简单形式和强形式，后者可由前者推出；第二层是对公式复杂度的归纳，即结构归纳，它由对长度的强归纳加以论证。借助它证明圆圈与圆盘的语言的权重引理（每个公式的权重为 $+1$ ，每个非空的真按词前缀的权重至多为 $0$ ），由此推出没有一个公式是另一个公式的真前缀，再由此推出唯一可读性：每个复合公式都只以一种方式分解为它的首个圆盘和它的两个成分。最后，唯一可读性为公式上的递归定义（长度、变元个数与联结圆盘个数、子公式、深度）以及在一个子公式处代入一个公式提供了依据。

学习目标

用简单归纳法和强归纳法证明自然数的性质，验证基始，并找出错误归纳的漏洞。
以变元和唯一的形成规则为仅有的情形，用对复杂度的归纳证明所有公式都具有某一性质。
证明权重引理，并由此推出没有一个公式是另一个公式的真前缀，以及每个复合公式都具有唯一可读性。
用递归定义公式上的函数（长度、深度、子公式、代入），并用归纳法证明它们之间的关系。

关于所有公式的断言

在关于命题逻辑的语言的一课中，公式由两个符号 $\sigO$ 和 $\sigI$ （我们称之为圆圈和圆盘）以及唯一一条形成规则构造出来。公式有无穷多个，许多重要的断言涉及全部公式：每个公式都以圆盘结尾，没有一个公式能以两种方式读出，每个公式中的变元都比联结圆盘多一个。这样的断言不是所研究语言中的公式，而是关于这个语言的陈述，用元语言（辅以数学记号的汉语）表述；因此，它们的证明不是形式系统内部的推演，而是以形式系统为对象的普通数学推理。正因如此，这类证明被称为元理论证明或外部证明。

然而，无论验证多少例子，都不能证明一个关于无穷多个对象的断言。由此可知，需要一条原理，使人能从有限次验证得出某一性质在无穷多种情形下成立的结论。这条原理就是归纳法。它先在自然数上介绍，因为那里最为熟悉；然后在公式上介绍，那里它依赖于前者。同一工具将在元理论单元中证明演绎系统的可靠性与完备性。