相关博文

• 《GEB：哥德尔、埃舍尔、巴赫——集异璧之大成》读书笔记 - 序章

WJU形式系统

很好，开始讨论形式系统了，这将是哥德尔不完备定理的第一步。

这是一个WJU三个字符构成的字符串的形式系统，一开始系统以 WJ 为公理；从公理出发，有限次应用规则Ⅰ至Ⅳ所得的字符串，称为定理：

• 规则Ⅰ：如果一个归你所有的符号串结尾是J，则可以在其后面再加上一个U。
• 规则Ⅱ：如果你有Wx，那么Wxx也归你所有。
• 规则Ⅲ：如果JJJ出现在你的储备中的一个符号串里，那么你可以用U代替这个JJJ而得到一个新的符号串。
• 规则Ⅳ：如果UU出现在你的一个符号串中，你可以去掉它。

多数人解WU谜题的办法是：先相当盲目地推出一些定理，看一看得到的会是什么。很快地，他们就开始注意到他们产生出的定理的一些性质，人的智能就在此处起作用了。

感觉应该算是LeetCode里面大约medium的一道题，这次牛刀小试了一下古法编程，调试了几个bug之后终于写出来了WJU形式系统的枚举器，当然是作者所说的机械笨办法。利用广度优先搜索遍历证明树：

from collections import deque
import tqdm
import itertools
import sys

axiom = "WJ"

def generate_strings(axiom):
    q = deque([axiom])

    while True:
        theorem = q.popleft()

        if theorem[-1] == 'J':
            q.append(theorem + "U")
        q.append(theorem + theorem[1:])

        start_k = 0
        while True:
            i = theorem.find("JJJ", start_k)
            if i == -1:
                break
            q.append(theorem[:i] + "U" + theorem[i+3:])
            start_k = i + 1
        
        start_k = 0
        while True:
            i = theorem.find("UU", start_k)
            if i == -1:
                break
            q.append(theorem[:i] + theorem[i+2:])
            start_k = i + 1
        
        yield theorem

gen = generate_strings(axiom)
print(next(itertools.dropwhile(lambda x: x[1] != sys.argv[1], tqdm.tqdm(enumerate(gen)))))

我们在证明WJ，WJU，WJJJJJ，WJUUUUUU的时候还算顺利，虽然因为我维护了一个队列，很快内存就有点吃不消，但至少正常完成了。而跑WU的时候，被作者阴了一手，看来这个是真的证不出来（在swap内存耗尽前被我杀掉了）。

这个故事告诉我们，做甩手掌柜肯定不对，如作者所说，这就是“跳出系统”，反思这个证明的时候了，也即找到定理的“判定过程”。

AI这个理解我觉得比我的要更为准确。我一开始的错误理解，就是动用人类能力找到这棵证明树对于一类定理的路径。机械只会枚举，但人为，可以靠他的灵性主动找到那条路径。而原作者其实更多关注的是跳出系统（例如用模运算等降维打击方法），不拘泥于找到那条路径，显然更为契合这里的背景。

二部创想曲

阿基里斯追上乌龟之后，舒舒服服地坐在了龟背上。 “这么说，你已经到达我们这场赛跑的终点了，是吗？”乌龟说。“虽然比赛的路程是由无数段路程组成的，你还是跑到啦？我记得有个自作聪明的人证明过这是不可能做到的。”

这里的故事主要讲的是三段论。且不提我们不接受大前提、小前提，假设我们不接受从大前提、小前提到结论的这个步骤，会发生什么呢？

这件事看似荒谬，但如果我们回到WJU形式系统中去想：三段论本身就像一条操作字符串的规则，它属于这个系统的“推理规则”，而不是超脱于系统之外的东西。就像我们可以决定 WJU 系统里是否有规则Ⅰ ~ Ⅳ一样，我们也可以选择是否认可三段论这条规则。换句话说，任何形式系统都依赖于我们事先接受的公理和推导规则，不会自动“合理”。

只是，我们之所以采用它，是因为在通常的语义解释下，它能够可靠地从真前提保持到真结论，因此适合用来刻画人类的理性推理。

下一章，期待我们对于这类形式系统有更多的挖掘与更深刻的理解吧。