形式系统，算法杂谈

混沌

重度庄子上瘾者

未来简史最后的三问：

1，生物真的只是算法，而生命也真的只是数据处理吗？
2，智能和意识，究竟哪一个才更有价值？
3，等到无意识但具备高度智能的算法比我们更了解我们自己时，社会，政治和日常生活会有什么变化？

希尔伯特提出的23个问题中的第10个：能否通过有限步骤来判定不定方程是否存在有理整数解?

算法的朴素印象：关于计算过程的一串有限的，确定的指令。

我们先看哥尔不完备定理：

命题逻辑L的可靠性：从语法推论得出的结论，在对应的赋值中语义也是一样的。
命题逻辑L的完全性：从语义推论得出的结论，在与语法上的推论也是一样的。
在命题逻辑L的基础上加上量词和谓词变为一阶谓词逻辑
谓词逻辑K的可靠性：从语法推论得出的结论，在对应的赋值中语义也是一样的。
谓词逻辑K的完全性：从语义推论得出的结论，在与语法上的推论也是一样的。
先举例说明什么是语法推论：
L的公式集三条“公理”：

1， p\rightarrow (q\rightarrow p)

2， (p\rightarrow(q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow(p\rightarrow r))

3， \left( \neg p\rightarrow \neg q \right) \rightarrow (q\rightarrow p)

MP规则：

如果 p_{i} 和 p_{i} \rightarrow p_{k} 那么 p_{k}

p\rightarrow (q\rightarrow p) 及 (p\rightarrow(q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow(p\rightarrow r)) 以及恰当的推理规则可以得到 p\rightarrow p ，即， p\rightarrow p 是可证的。

(1) 根据代入规则，分别将公理 2 中的 p、q、r 替换为p， p\rightarrow p ，p，得： (p\rightarrow((p\rightarrow p)\rightarrow p))\rightarrow ((p\rightarrow (p\rightarrow p))\rightarrow(p\rightarrow p))
(2) 根据代入规则，分别将公理 1 中的 p、q 替换为p， p\rightarrow p ，得： p\rightarrow ((p\rightarrow p)\rightarrow p)
(3) 由 (1)、(2) 根据 MP 规则，得到： (p\rightarrow (p\rightarrow p))\rightarrow(p\rightarrow p)
(4) 根据代入规则，分别将公理 1 中的 p、q 替换为p，p，得到： p\rightarrow (p\rightarrow p)
(5) 由 (3)、(4) 根据 MP 规则得： p\rightarrow p ，即为所证。

语义推论：

p 的赋值是 1 的时候， p\rightarrow p 为真；

p 的赋值是 0 的时候， p\rightarrow p 也为真；

因此， p\rightarrow p 在所有赋值下都得到满足，即， p\rightarrow p 是重言式（永真式）。

语法系统中没有真，假的概念，只有代入，替换，MP 规则。

语义系统中没有证明，推演。

简单说语法系统中没有意义，只有符号，及相应的变化规则。而语义系统中符号有它的意义，有真与假等概念。就像在自然语言中，一句话语法上没问题，但是可能语义上有问题。比如“对是错”。而在L，K这种系统中意味着语法上没问题，语义上就没问题。如果语法上检查就非常简单了，不明白意思也可以检查，现在的计算机就特别适合，典型的如编译器，解释器，操作系统等。

但是当我们在K系统中加入了皮诺亚算法形式算法的定理后的系统 K_{n} 不再具备这种属性了。出现了语义上为真的，在形式体系 K_{n} 中却无法证明（不能证明为真，也不能证明为伪）的命题。

哥德尔第一不完备定理：任意一个包含一阶谓词逻辑与初等数论的形式系统，都存在一个命题，它在这个系统中既不能被证明为真，也不能被证明为否。

哥德尔第二不完备定理：如果系统S含有初等数论，当S无矛盾时，它的无矛盾性不可能在S内证明。

证明的过程还是相对麻烦的这里就不写了。思路大体就是在kn中创造了一个说谎者悖论。

1，在算术体系内 P(A, X) 表示形式系统中公式z(a)的哥尔德编码为A，如果公式集的哥德尔编码为X的可以证明z(x)就为1否则为0。语义上就是z是否可证。

2，可以证明 P(A, X) 是可表达的。那么我们在形式体系内构造出 f(a)=\forall x \neg p(a, x) 其语义就是哥德尔编码为A的公式不可证。

3，我们在算术体系内对 f(a) 进行哥德尔编码为 M 其对应在形式体系中为 m

4，将 m 代入公式 f(a)=\forall x \neg p(a, x) 得出 f(m)=\forall x \neg p(m, x)

如果 f(m) 可证那么 \forall x \neg p(m, x) ，我们记 f(m) 的一个证明的哥德尔数为 Y ，在形式体系内就有 p(m, y) ，与 \forall x \neg p(m, x) 矛盾。

如果 \neg f(m) 可证那么 \neg \forall x \neg p(m, x) ，那么就没有一个证明的哥德尔数 Y ，在形式系统中为 \forall x \neg p(m, x) ，与 \neg \forall x \neg p(m, x) 矛盾。

该定理揭示在多数情况下,例如在数论或者实分析中,永远不能找出公理的完整集合（递归集）.你可以在公理体系不断加入新的公理,甚至构成无穷的公理集合,但是这样的公理列表不再是递归的,不存在机械的判断方法判断加入的公理是否是该公理系统的一条公理.这对于计算机科学意义重大,在计算机语言中,一阶逻辑的定理是递归可枚举的,然而哥德尔第一不完备定理表明：无法编制这样的程序,通过递归的定理证明,可在有限时间内判断命题真假.

"我说的是假话"这句话在自然语言中语法上没问题，但是语义上出现了悖论，不为真也不为假。而哥德尔不完备定理就是如此，在公理集（递归集）强大到一定程度，这个形式系统就有可以表达语义层面能力，然后可以构造自我指涉类似“我在这个公理集下不可证”这样的句子（只要包含了算术的+，*本质是可以哥德尔编码的算术要求，以及递归的公理集就能构造出这样的句子），让“真”与“可证”出现一些与常识相背的情况（即“真”而不”可证“）。在语义体系中的”真“与语法体系中的”可证“不是同一个概念。”可证“即真，并非”真“就”可证“。

在N中的算术真理集TR，在Kn中的的可证公式集TH，及TH的补集 TH 的关系：

递归集 \in 递归枚举集 \in 算术集，而TR超出了算术集，TH是递归枚举集， TH 是算术集，所以真与可证是不同的概念。

另外：一元数论函数集合是不可数无穷大，而我们递归公理所产生的公式是可数无穷大，注定是绝大多数一元数论函数在递归公理中是无法表达的。

哥德尔打破的只是：希望用一组完备的递归公理集的形式系统，推导出全部的数学”真“。这意味的没有一劳永逸的事，我们永远需要不但的往公理集添加新的公理来适应我们的需要。不能像写完一个判断是否奇数算法就完事了，什么数来都可以算。而是永远要为了某些新的数据来扩充我们的算法。

与此相关的点：说谎者悖论，哥德尔不完备定理，塔斯基不可定义定理，图灵停机，递归集和可计算性理论等都联系在一起。

对于与算法相关联较为直观的就是图灵停机，可计算这些东西了。其实也就是计算机领域的哥德尔不完备定理。

比如我们可以写一个函数用检查输入的数是不是奇数：f(n)=n%2==1或者是不是平方数f(n)=n-sqrt(n)*2==0，但是我们可不可以写个函数来检查一段代码中有没有死循环呢？假设可以这个函数就是checkhalt(program, input)可以做到没有死循环就返回1否则返回0，那么现在我们特意设计一个新函数:

def bug(program):
	if checkhalt(program, program):