axiom

(Updated: )

Formal System

定义

一个形式系统 由符号集 , 合式公式集 , 公理集 和推理规则集 组成

  1. 符号集 : 包括变量, 逻辑符号, 函数符号等

  2. 合式公式集 : 指符号集中的符号按照一定的语法规则构造出的公式集

    由于没有语法集, 合式公式集就包含了所有的语法

  3. 公理集 : 合式公式集的一些不需要证明, 假设为真的公式

  4. 推理规则集 : 形式系统中从一个或多个已知公式 (前提) 推导出新公式 (结论) 的规则

    一些常见的推理规则:

    • Modus Ponens：从 和 推出 , 如

      我是雏草姬, 如果一个人是雏草姬那这个人一定关注了永雏塔菲, 推出 我一定关注了永雏塔菲

句法推导与语义蕴含

句法推导

从公理集 出发, 按照推理规则 (如 Modus Ponens) 经过有限步演绎, 可以构造出公式 , 记为

“推出” 纯粹是形式操作, 不涉及真值, 只是符号串的操作

语义蕴含

一个结构 满足一个公式 , 记作 , 意思是把公式 放到结构 的解释规则下去看, 结果是真的

例如, 在自然数结构 里, 公式 是真的, 所以该结构满足这个公式

对于公理集 , 我们定义

含义为: 在所有模型 中, 如果 , 即所有 中的公式在模型 都为真, 那么 也成立

这是真值意义上为真

形式语言与形式演绎系统

, 即字母表和语法, 组成形式语言

, 即公理和推理规则, 组成形式演绎系统

自然推理系统与公理推理系统

自然推理系统

公理集为空, 则这个形式系统为自然推理系统

推导从前提/假设出发, 仅依赖推理规则 (如反证法等)

公理推理系统

公理集不为空, 则这个形式系统为自然推理系统

推导从公理出发, 推出的为定理

一致性, 可靠性和完备性

一致性 Consistency

不可同时证明 与 则为一致, 或者说不可证明

如果不一致, 则一切公式都可以被推出, 此为爆炸原理

即 , 我们要证明, 对于任意公式 , 有

这里用了两个推理规则:

  1. 析取引入 (Disjunction Introduction)

    如: 我喜欢千早爱音, 所以我喜欢奶龙或我喜欢千早爱音

  2. 析取三段论 (Disjunctive Syllogism)

    例如: 我喜欢奶龙或我喜欢千早爱音, 且我不喜欢奶龙, 所以我喜欢千早爱音

那么已知 使用析取引入,

已知 使用析取三段论,

所以能推出所有结论

可靠性 Soundness

凡可证必为真,

可靠必一致, 一致不一定可靠

因为如果不一致, 则 且

由于可靠性, 且

但是一个模型对一个公式只能给出真或假

所以矛盾, 可靠一定一致

完备性 Completeness

凡为真必可证,

在足够强的算术系统中, 一致 不完备, 这即为哥德尔第一不完备定理的内容

Gdel’s Incompleteness Theorem

一些不可证明的问题

停机问题, 罗素悖论, 说谎者悖论

这些问题基本有个共同的形式: “我与我自己矛盾”

哥德尔第一不完备定理

我们想要构造一个公式, 使得其在一致的算术系统 中无法证明自己, 同时为真

公理系统的条件

具体地, 这个系统要满足下面条件:

  1. 一致性
  2. 可表示性: 系统可以证明所有原始递归关系
  3. 递归可枚举性: 系统的公理集是递归可枚举的

思路

具体地, 我们要构造 , 表示在 下无法证明哥德尔数为 的公式

这里的 表示 可证明的 “可证明谓词”

这个可证明谓词有一个性质: 如果 , 那么

即可以证明 就可以证明 是可以证明的

有关这个性质的证明, 给出 是原始递归关系, 可以被可表示的算术系统证明, 因为 可以只涉及基本运算来验证 是否为 的证明的哥德尔数

那么

这里用了一个推理规则:

  • 存在化规则:

由于 , 所以存在 使得 为真

由于可表示性,

由存在化规则,

即

那么假设 , 则

同时由于 , 那么

即得到一对矛盾, 系统不一致, 与一致的前提矛盾

从而 无法证明

如果要证明 是无法反驳的, 需要引入 一致

假设 , 则 , 即存在一个 是 的证明的哥德尔数

但是由上面结论, 无法证明 , 因此对于任意的 都不能成为 的证明的哥德尔数

所以矛盾, 得到 无法反驳

至此 无法被证明 (且无法被反驳), 则无法判定, 同时 为真, 即不完备

  • 这里给出的不是一个严格的论述, 需要参考哥德尔原论文

哥德尔数

具体地, 我们需要一个编码方式, 将符号与运算符组成的公式编码为一个自然数, 这个编码叫做哥德尔数

由于系统有递归可枚举性, 这个编码是可以存在的

可以参考 TCS 笔记: 可数当且仅当可编码, 可数与可枚举是一个意思

编码方式参考 这里

由于 对应的哥德尔数是 , 所以考虑 无法证明哥德尔数是的公式

其中 表示在公式 中将所有哥德尔数为 的符号替换成 后计算得到的哥德尔数

那么记 无法证明哥德尔数是的公式

可以看到, 无法证明哥德尔数是的公式

所以 无法证明哥德尔数是的公式

这个 就是我们要构造的东西

哥德尔第二不完备定理

上面的论述说明, 如果我们形式化哥德尔第一不完备定理, 则系统 可以自证这个定理

具体地, 定义

那么

假设 , 那么

这儿说明 可以被证明

但是由第一定理, 不可被证明, 所以矛盾

因此 , 即 不能自证其一致性

连续统假设 Continuum Hypothesis

哥德尔构造了一个模型, 证明了 , 即 作为公理成立, 无法在 时反驳

Cohen 构造了另一个模型, 证明了 , 即 无法证明

所以在 公理系统中, 由于多模型的存在, 无法判定