简介Hilbert and Ackermann’s Principles of Theoretical Logic - Stanley Burris的读书笔记

一，简介Principles of Theoretical Logic

《 Principles of Theoretical Logic》是阿克曼和希尔伯特在1928年写的一本关于逻辑的书。它是第一本以初级和严谨的方式介绍现在被称为一阶逻辑的书。

二，Stanley Burris的读书笔记（March 13, 2001）

希尔伯特在1917-1922年期间开设了以下关于逻辑和基础的课程：

Principles of Mathematics 1917/1918年冬季学期

Logic Calculus 1920年冬季学期

Foundations of Mathematics 1921/22年冬季学期

在这些讲座的准备和最终撰写过程中，他得到了伯纳斯的大量帮助。这些材料后来被阿克曼重新加工成希尔伯特和阿克曼的《 Principles of Theoretical Logic》（1928）一书。该书旨在作为数理逻辑的介绍，以及希尔伯特和伯纳斯即将出版的书（主要致力于一阶数论的研究）。在120页中，他们涵盖了：

Chap. I: the propositional calculus,

Chap. II: the calculus of classes,

Chap. III: (many-sorted) first-order logic of relations (without equality), and

Chap. IV: the higher order calculus of relations (without equality).

第一章：命题计算

第二章：类的计算

第三章：（无等价）关系的（many-sorted）一阶逻辑，以及

第四章：（无等价）关系的高阶计算

让我们对这些章节的每一章做一些评论。

第一章讨论了基本连接词 ∧, ∨, ⇒ , ⇐⇒ , ¬ (他们使用的符号是 &, ∨, ⇒ , ≈, ˉ), 交换律、关联律和分配律，以及减少所需连接词的数量。他们说（第9页）：

作为一种好奇，让我们注意到，正如Sheffer所显示的，我们可以用一个逻辑符号就能搞定。

这比怀特海和罗素在《 Principia Mathematica》第二版中所说的谢弗（Sheffer）将命题逻辑还原为一个单一的二元连接词是他们第一版出现以来逻辑学中最重要的发展，更接近现在对谢弗的发现的重视。事实上，怀特海和罗素在《数学原理》中加入了必要的文字，将他们基于∨和¬的发展还原为谢弗竖线（Sheffer stroke）。

接下来，希尔伯特和阿克曼展示了如何将命题置于合取或析取的范式中，并展示了如何用它来描述有限命题集的所有结果。然后他们讨论了如何确定一个陈述是重言式（他们说是普遍有效），还是可满足的。

他们在命题计算的公理化方面遵循《 Principia》，利用Bernays（1926）的工作将公理清单从5个减少到4个。 在谈到与公理方法相关的问题时（《Theoretical Logic》第29页），他们说：

在出现的问题中，最重要的是一致性、独立性和完备性的问题。

在注意到人们可以精确地推导出他们系统中的重言式之后，我们提出了这个命题计算的这些问题的解决方案，这是由于Bernays（1926）。完备性结果是加强版本，即在公理中加入任何非重言式都允许推导出矛盾，从而推导出所有命题公式。

第二章对类计算的简要处理实际上是一元谓词的一阶逻辑的非公理版本，这个系统比传统的类计算有相当大的表现力，人们可以用它来表述亚里士多德的 Syllogisms。

第三章以康德的一句名言开始：

- 值得注意的是，到目前为止，它[逻辑学]还未能[超越亚里士多德]向前迈出一步，因此，从表面上看，它似乎是封闭的、竞争的。

然后他们谈论亚里士多德的逻辑：

- 它在任何地方都是失败的，因为它要给几个对象之间的关系提供一个符号表示 - - - 而这种情况几乎在所有复杂的判断中都存在。（《Theoretical Logic》，第44页）

他们开发的一阶系统使用关系和常数符号，但等价不是逻辑的一部分。此外，他们的关系是many-sorted的，在他们的例子和形式化的逻辑中都是如此（《理论逻辑》，第45、53、70页）。在第二版（1937年）中，形式化的版本是one-sorted的，但例子仍然是many-sorted的；并给出了一个使用单域谓词的技术，以从many-sorted转换到one-sorted（《Theoretical Logic》，第105页）。

作为如何在他们的形式系统中表达数学的一个例子，他们转向（one-sorted）自然数，使用两个二元关系符号=和F（代表后承）以及常数符号1，并写出三个属性：

i. ∀x∃y[F(x,y)∧∀zF(x,z) ⇒ y=z] 

ii. ¬∃xF(x,1)

iii. ∀x[x≉ 1 ⇒ ∃y(F(y,x)∧∀z(F(z,x) ⇒ y≈x))].

他们的形式系统如下：

1. 命题变量X,Y, · · ·

2. 对象变量 x, y, · · · 

3. 关系符号F( ),G( ), · · ·

4. 连接词：∨ 和 ¬ (X ⇒ Y 表示 ¬X ∨ Y )

5. 定量词：∀ 和 ∃ (他们用 (x) 表示 ∀x, 用 (Ex) 表示 ∃x)

6. 公理：

X ∨ X ⇒ X

X ⇒ X ∨ Y

X ∨ Y ⇒ Y ∨ X

(X ⇒ Y) ⇒ [Z∨X ⇒ Z∨Y] ∀xF(x) ⇒ F(x)

F(x) ⇒ ∃xF(x).

7. 推理的规则：替代规则

modus ponens

φ ⇒ ψ(x) 

φ ⇒ ∀xψ(x) (只要x在φ中不是自由的)

ψ(x) ⇒ φ 

∃xψ(x) ⇒ φ

最后两个公理的简单形式和最后一个推理规则是由伯纳斯提出的。利用这个系统，他们展示了一些基本的事实，比如每一个公式都可以用prenex形式表示。

然后他们转向了他们指定的重要问题。使用单元素论域，他们表明上述公理系统是一致的（记得弗雷格的系统是不一致的）。然后他们说（《Theoretical Logic》，第65页）：

- 在这种情况下，我们绝对不能保证以符号形式引入的假设（对其解释没有异议）能保持可推导公式系统的一致性。例如，在我们的计算中加入数学公理是否会导致每个公式的可证明性，这是一个没有答案的问题。这个问题的难度对数学具有核心意义，但与我们刚刚处理的问题的难度不可同日而语 - - - 。为了成功地对这个问题发起攻击，希尔伯特（D. Hilbert）发展了一个特殊的理论。

阿克曼给出了上述系统在更强意义上不完整的证明（Theoretical Logic，第66-68页），即他们表明∃x F (x) ⇒∀ xF (x)和它的否定是不可推导的。然后说以下几点（Theoretical Logic, p. 68）。

该公理系统是否完备，即可以推导出所有在每个领域都有效的逻辑公式，这仍是一个未解决的问题。只能根据经验说明，这个公理系统在应用中一直是充分的。公理的独立性还没有被研究过。

在使用这个系统的一些例子之后，他们在第三章的第11节转向了判定问题。我们引用（《Theoretical Logic，第72页）：

- 根据最后一个例子所描述的方法，人们可以把一阶计算特别适用于理论的公理化处理··· 。

- 一旦逻辑形式主义建立起来，人们就可以期待对逻辑公式的系统性的、可以说是计算性的处理是可能的，这将在某种程度上对应于代数中的等式理论。

- 我们在命题计算中遇到了一个发达的逻辑代数。那里解决的最重要的问题是逻辑表达的普遍有效性和可满足性。这两个问题都被称为判定问题···。

这两个问题是相互对立的。如果一个表达式不是普遍有效的，那么它的否定就是可满足的，反之亦然。

一阶逻辑的判定问题现在呈现出来了 - - - 。我们可以把自己限制在命题变量不出现的情况下 ----。

- 如果我们知道一个过程，在给定一个逻辑表达式的情况下，允许确定其有效性和可满足性，那么判定问题就解决了。

- 判定问题的解决对于所有议题的理论都具有根本的重要性，这些议题的定理能够从有限多的公理中逻辑地导出 - - - 。

(Theoretical Logic, p. 74)

我们想说明的是，为了解决判定问题，将给出一个过程，通过这个过程，原则上可以确定nonderivability，尽管这个过程的困难会使实际使用成为空想——。

(Theoretical Logic, p. 77)

--- 判定问题被指定为数理逻辑的主要问题。

--- 在一阶逻辑中，发现一般的判定程序仍然是一个困难的未解决的问题 ——。

在第三章的最后一节中，他们给出了L ̈owenheim对只涉及单数关系符号的一阶语句的判定程序，即表明只需检查所有大小小于或等于2k的域即可，其中k是语句中一元谓词符号的数量。因此（第80页)

. . . 假设一个逻辑命题的有效性或可满足性等同于一个关于域的大小的陈述。

在最一般的意义上，如果我们有一个程序来确定每个逻辑表达式对哪些域有效或可满足，我们就可以说判定问题已经解决了。

我们也可以提出一个更简单的问题，即一个给定的表达式何时对所有领域有效，何时无效。在判定过程的帮助下，这就足以回答基于公理的主题的某一给定语句是否可以从公理中得到证明。

然后他们指出，我们不能寄希望于一个基于考察有限域的过程，就像在一元谓词计算中一样；但L ̈owenheim定理给出了一个强有力的类似物，即一个陈述在所有域中都有效，如果它在可数无限域中有效。然后，他们试图将判定问题与完备性问题联系起来（Theoretical Logic, p. 80）：

- 在每个领域都有效的公式的例子是那些从谓词计算中得到的公式。既然人们怀疑这个系统给出了所有这样的[有效]公式，那么人们就会通过对系统中可证明的公式的描述来接近判定问题的解决。

判定问题的一般解决方案，无论是第一种还是第二种提法，到现在还没有出现。P. Bernays和M. Schoenfinkel以及W. Ackermann已经对判定问题的特殊情况进行了研究和解决。

最后他们指出，L-̈owenheim表明，人们可以将注意力限制在一元或二元谓词上。

第四章一开始就试图说明，人们需要扩展一阶逻辑来处理基本的数学概念。这种扩展是通过允许关系符号的量化来实现的。然后，人们可以通过（《Theoretical Logic》，第83页）来表达完整的归纳：

[P(1)∧∀x∀y(P(x)∧Seq(x,y) ⇒ P(y))] ⇒ ∀xP(x) 

或者，说得更明确些。

我们可以把通用量词(P)放在公式的前面。

x和y之间的同一性，≡（x，y），由∀F F（x）⇐⇒F（y）定义。然后他们说（《Theoretical Logic》，第86页）。

这个一般判定问题（对于扩展逻辑）的解决不仅允许我们回答关于简单几何定理的可证明性的问题，而且至少在原则上，还可以判定一个任意数学语句的可证明性（resp. nonprovability）。

一阶计算对于少数特殊理论来说是不错的。但是一旦人们把理论的基础，特别是数学理论的基础作为研究对象----扩展计算就必不可少了。扩展计算的第一个重要应用是在数上。个体的数字被实现为谓词的属性，例如：

0(F) =: ¬∃xF(x)

1(F)=:∃x[F(x)∧∀y(F(y) =⇒≡(x,y))].

Φ是一个[cardinal]数的条件是

∀F ∀G [(Φ(F)∧Φ(G) =⇒ SC(F,G)∧(Φ(F)∧SC(F,G) =⇒ Φ(G))],

其中SC(F,G)表示在满足F的元素和满足G的元素之间有一个1对1的对应关系。在建立了定义和作为一个无限域的总结之后，他们说（注：怀特海和罗素）：

另外，特别有意思的是，数论公理成为逻辑上可以证明的定理。

他们在这个扩展计算中发展了集合理论，认为集合是单数谓词的扩展；因此两个谓词F和G决定了同一个集合，如果∀x F (x) ⇐⇒ G(x)成立，这被简写为Aeq(F, G)。那么，集合的属性对应于单数谓词P的单数预言，其中P在Aeq下是不变的。有序对的集合对应于二元谓词等等。在这种翻译下，一个数变成了域中个体的集合，即一个数是等同于一个给定集合的所有集合的集合。他们对集合理论的发展以联合、相交、有序集和有序集的定义而结束，他们说集合理论的所有通常的概念都可以在他们的系统中用符号表达。

在展示了关系的扩展计算的表达能力之后，他们转向了寻找公理和推理规则的问题。来自一阶逻辑的明显概括通过众所周知的悖论导致了矛盾。最后，他们概述了怀特海和罗素的ramified theory of types  （with its questionable axiom of reducibility），该理论允许人们给出概括一阶逻辑的公理和推理规则，避免了将悖论编码为矛盾的通常做法，并且强大到足以进行传统数学。在提到判定问题也适用于《原则》体系之后，该书的结尾是希尔伯特声称有一个扩展逻辑的发展，它将很快出现，它避免了可还原性公理的困难。

回顾这本书，我们发现它的目的是介绍形式系统，并举出例子。在第一章命题计算的发展之后，几乎没有真正的数理逻辑定理被证明或陈述；主要的例外是一阶单数关系逻辑的L ̈Owenheim判定过程的证明，以及L ̈Owenheim-Skolem定理的陈述。一阶集合理论甚至没有被提及。

参考文献：

https://www.math.uwaterloo.ca/~snburris/htdocs/WWW/PDF/hilbert.pdf

https://books.google.fr/books?id=45ZGMjV9vfcC&printsec=frontcover&hl=fr#v=onepage&q&f=fals

https://en.wikipedia.org/wiki/Principles_of_Mathematical_Logic