提问

由有限数量的公理构成的公理系统，能够推导出多少定理？

回答

应该是无穷多的吧，但这种无穷多是什么等级的无穷多呢？

• 是和整数一样多的无穷多么？这种叫做 ℵ0，aleph-0
• 还是和实数一样多的无穷多？这种无穷多叫 ℵ1, aleph-1
• 或者更多？比实数还多，比如ℵ2，ℵ3……

常见公理系统

一个公理系统，通常由有限数量（甚至是尽量少的）公理、一些定义和一些推理规则构成。从公理出发，按照推理规则可以推理出各种定理。公理系统应当具有“完备性”和“可靠性”

• 完备性：是否所有的定理都可以由公理系统推导出来？
• 可靠性：非重言式或不成立的公式是否也可以推导出来？

罗素公理系统

比如罗素公理系统由4条公理构成

ZFC公理系统

这是现代数学的基础，一切从集合出发，一切也都是集合。

由10条公理构成，还有一个选择公理。

其中的Z是策梅洛Zermelo，我之前听过策梅洛是因为他还有一个很有趣的策梅洛定理，双人游戏，没有和局不靠运气不藏着掖着，则一定有必胜招。（二人的有限游戏中，如果双方皆拥有完全的信息，并且运气因素并不牵涉在游戏中，那先行或后行者当中必有一方有必胜/必不败的策略）

王浩算法

王浩算法也是一个公理系统。

H. Wang, "Toward Mechanical Mathematics," in IBM Journal of Research and Development, vol. 4, no. 1, pp. 2-22, Jan. 1960, doi: 10.1147/rd.41.0002. 全文

王浩算法中定义了“相继式”，就是两个公式串 alpha, beta，记作alpha s=> beta

王浩算法看起来比罗素公理系统优雅多了，只有一个公理，

如果公式串alpha 和 beta 的公式都只是命题变项A,B,..., alpha s=> beta是公理（为真）的充分必要条件是alpha和beta中至少含有一个相同的命题变项

还有10条无脑推理过程，非常适合计算机编程。1958年王浩用汇编语言写了算法，9分钟把罗素写了10年的Principia Mathematica中一阶逻辑部分的全部定理证明完了。

在网上可以找到用python写好的王浩算法

上面说的

• 命题变项，简单理解就是个字母，比如P、Q、R之类的东西，
• 相继式就是类似 P,Q,R s=> P,Q 的式子
• 相继式左边的叫前件，右边叫后件

P,Q,R s=> P,Q 这就是两边“至少含有一个相同的命题变项”的样子。它的意思就是 if (P and Q and R) then (P or Q)，如果左边的P and Q and R是真，那么必然有右边P or Q为真，还是挺显然的。

当然，实际的定理会更复杂一些，字母是放在各种逻辑运算之中的，需要把每个分离出来才能两边找到相同的命题变项。比如

\[(\neg Q \wedge (P \rightarrow Q)) \rightarrow \neg P \]

一些想法

由有限数量的公理构成的公理系统，能够推导出多少定理？

我觉得这个问题一定有先贤研究过，不确定是个简单的作业题水平，还是，需要发一篇论文的那种。但抱歉，我不是数学专业的，实在是不太会查数学方面的论文。关键词是什么我都还没找准。我一时还没有查到相关的论文。

用王浩算法推理

如果我们从王浩算法出发进行推理，来生成大量的定理。就只是把王浩算法反过来用，不是在alpha,beta中至少含有一个相同字母就证明了么，那么就可以先从{} s=> {} 开始，两侧加同样的字母（命题变项），然后再用10条推理规则给它变形，变形过程之中还可以再添加字母，再变形……

如果用数字来标记这些过程，比如

• 0~9：标记10条推理规则
• 10：在两侧增加一个之前没出现过的新字母
• 11：在两侧增加一个之前出现过的字母，是在推理过程中加入的第1号字母
• 12：在两侧增加一个之前出现过的字母，是在推理过程中加入的第2号字母
• ……
• 101：对alpha的第1个命题变项（经过变形的字母或者组合）使用规则，得到结果放在beta末尾，所使用的规则用下一个数字标记说明。
• 102：对beta的第1个命题变项（经过变形的字母或者组合）使用规则，得到结果放在alpha末尾，所使用的规则用下一个数字标记说明。
• 103：对alpha的第2个命题变项（经过变形的字母或者组合）使用规则，得到结果放在beta末尾，所使用的规则用下一个数字标记说明。
• 104：对beta的第2个命题变项（经过变形的字母或者组合）使用规则，得到结果放在alpha末尾，所使用的规则用下一个数字标记说明。
• ……

那么，我们就可以用一个数字串来表示一个用王浩算法推理出来的定理，比如{10，0，11，2，11，3，10，9，12，4}，

这样一个数字串似乎和有理数相似，所以用王浩算法推理出来的定理应该是和有理数等势的，也就是ℵ0

但是

如果每次都是新增一个新字母，用来标记推理过程的数字是有限的，只需要0-9和10，那我很有把握每一个推理出来的定理都是可数的，总数是ℵ0。

但如果可以新增已经出现过的字母，就需要对已经出现过的字母进行标记，更复杂的是，应用推理规则，需要有个“宾语”，指明对哪一项应用推理规则。你可以看出我在标号上有点力不从心。

于是这里面似乎出现了“幂集”：由该集合全部子集为元素构成的集合。给定集合S，它的幂集写作P(S)。一旦出现了幂集，就有可能有ℵ0^ℵ0，会产生ℵ1。

这里有可能有争辩，两个生成的定理很有可能是相同的，我觉得可能需要约定王浩算法生成的相继式如何算是“相等”，alpha中的各个命题变项当然可以换顺序，beta中的也可以换顺序。所以说相继式相等，我觉得可以定义为当且仅当set(alpha)和set(beta)相等。

但在描述相继式相等的时候，不应该应用任何推理规则，不能进行任何约简，因为如果应用推理规则，那么所有可证明的定理都能约简成{} =>{}，这种“相等”会传递到全集之中。

说起顺序，好像前面的编号系统中，可以化简一下，比如我们定义数字：

• 100：alpha中的命题变项末项移动到首项，
• 101：beta中的命题变项末项移动到首项，
  这样，就可以约定0-9，只是针对首项进行操作。也许可以缓解一些幂集的问题

用其他公理系统考虑

比如罗素，或者ZFC，或者其他随便什么公理数量有限的公理系统，我们可以把公理写作一个集合，比如A，那么

• 仅仅使用不多于1次这些公理得到的定理，不会少于P(A)
• 仅仅使用不多于2次这些公理得到的定理，不会少于P(P(A))
• 仅仅使用不多于3次这些公理得到的定理，不会少于P(P(P(A)))
• ……
• 仅仅使用不多于n次这些公理得到的定理，不会少于P^n (A)

这里面似乎又可能出现自然数集的幂集，可能会有ℵ0^ℵ0，会产生ℵ1。

上面都把似乎加粗了，因为我也不知道应该如何做严密的论证，只是感觉而已。

再回到王浩算法

这次不考虑标记的问题，如果我们从王浩算法去“生成”定理，那么所生成的每一条定理都是可以被证明的，因为必然可以反向使用每一个生成过程，最终回到{} => {}。

又因为王浩算法，显然可以用图灵机写出来。那么，

• 通过王浩算法生成的定理，不存在一条在王浩公理系统中不能证明也不能证伪的定理，也就是不存在哥德尔命题。
• 如果输入只有通过王浩算法生成的定理，似乎可以提前判定一定能够令该图灵机停机。

考虑到哥德尔不完备定理的证明方法用到的是对角线方法，和证明实数比整数多的方法相似，那么王浩算法生成的定理数量应当是小于实数的，也就是< ℵ1。那么，能够生成的定理数量，很有可能是ℵ0。

注意，上面强调了是生成的定理，当然会有一个定理无法使用王浩算法证明或者证伪，但这个定理是构造出来的，而不是生成出来的。

可能我还没有能够仔细理解哥德尔不完备定理，不过没有老师帮忙解读，要读懂数学论文还是难度挺大的。

为何生成定理

这是另一个好玩的想法，数学家们会卡在某一个定理的证明上几十年甚至上百年，也许可以反过来，我们可以从公理去生成好多好多定理，然后突然发现：这个长得好像xxx定理啊，或者，那个不就是yyy定理的描述吗，或者炼个什么LLM，喂给它一个由公理生成的字符串，它就“翻译”成一个定理，然后也许工程或者物理、化学中的某个难题轰的一声就解决了。罗素做的那十年题，就可以拿来当语料吧。

如果有讨论，请留言，但我确实没有能力判断您说的是否正确。
最好能够给我一篇现成的、经过同行评议过的数学文献，或者，一个Lean4的程序。