把形式系统讲明白

哥德尔不完备性探索器

一个更清晰的交互页面，用来解释形式系统、公理、推导、一致性，以及为什么不完备性会出现。

这个页面真正做的是什么

这是一个玩具级形式系统模拟器。它不会直接证明哥德尔定理，而是帮助你看清楚：公理如何发挥作用、推导如何扩展，以及为什么“继续加公理”也不能神奇地消除不完备性。

公理数 0
已知命题 0
已推出定理 0
证明深度 0
一致性 Consistent

推导时间线

0

下面每一步要么是起始公理，要么是玩具推理引擎自动推出的新命题。

下一批可推出命题

这些是当前公理和已有命题之下，模拟器下一步还能推出的内容。

一句话理解形式系统

形式系统以公理为起点，用推理规则推出定理。真正关键的问题不只是“能推出什么”，还包括“在不破坏一致性的前提下，哪些东西永远推不出来”。

哥德尔的关键一步

哥德尔把公式和证明编码成数字，再构造出一个等价于“我在这个系统里不可证”的句子。如果系统是一致的，那么这个句子在系统内部就不能被证明，但在预期语义下它却是真的。

这个模拟器能做什么，不能做什么

这个页面实现的是一个很小的规则引擎，用来帮助你观察公理如何扩展一个理论。它并没有实现完整的一阶算术、哥德尔编码或真正的证明检查，所以它是概念桥梁，不是证明助手。

建议你这样玩

  • 从“0 ∈ ℕ”和后继公理开始，逐步观察自然数命题如何长出来。
  • 添加 P → Q，再添加 P，看看肯定前件如何推出 Q。
  • 同时添加 P 与 ¬P，观察系统如何被标记为不一致。