我是逻辑学家-编程知识

我是逻辑学家

news/2025/3/12 8:19:01/文章来源:https://www.cnblogs.com/Troverld/p/18766619

\[\newcommand{\d}{\mathrm d} \newcommand{\N}{\mathbb N} \newcommand{\sube}{\subseteq} \newcommand{\sub}{\subset} \newcommand{\supe}{\supseteq} \newcommand{\sup}{\supset} \newcommand{\eps}{\epsilon} \newcommand{\vare}{\varepsilon} \newcommand{\cur}[1]{\left\{#1\right\}} \newcommand{\ip}[1]{\left<#1\right>} \newcommand{\getsto}{\leftrightarrow} \newcommand{\t}{\text} \newcommand{\c}{\mathcal} \newcommand{\vd}{\vdash} \newcommand{\ovl}{\overline} \newcommand{\To}{\Rightarrow} \newcommand{\Gets}{\Leftarrow} \newcommand{\GetsTo}{\Leftrightarrow} \newcommand{\T}{\mathtt T} \newcommand{\F}{\mathtt F} \]

I. Informal Statement Calculus

非正式命题逻辑 (Informal Statement Calculus) 研究 命题形式 (statement form)。命题形式的基本单元是 命题变量 (statement variable)，即取值可能为真或为假的变量。命题形式也可以是子命题形式用 逻辑联结词 (connective) 连接成的句子，其中逻辑联结词可以是 \(\sim,\land,\lor,\to,\getsto\) 等。【什么神人会用 \(\sim A\) 表示非 \(A\) 呵？不喜欢 LaTeX 导致的。下文使用 \(\lnot\)。】

一个 重言式 (tautology) 是对于变量的一切取值都恒真的命题形式。一个 矛盾式 (contradiction) 是恒假式。

对于命题形式 \(A,B\)，\(A\) 逻辑推出 (logically implies) \(B\) 如果 \(A\to B\) 是重言式，逻辑等价于 (logically equivalent) \(B\) 如果 \(A\getsto B\) 是重言式。

一些基础的推导规则例如：

肯定前件式 (modus ponens, MP)：如果 \(A\) 和 \(A\to B\) 均是重言式，则 \(B\) 亦然。
替代法则 (substitution rule)：令 \(A\) 是一个由命题变量 \(p_1,\dots,p_n\) 组合成的命题形式。如果 \(A\) 为重言式，则令 \(A_1,\dots,A_n\) 为任意命题形式，则任何将全体 \(p_1,\dots,p_n\) 的出现分别替换为 \(A_1,\dots,A_n\) 而得到的新命题形式 \(B\) 都是重言式。
De Morgan 律：

\[\bigvee\lnot A_i=\lnot\bigwedge A_i \\\bigwedge\lnot A_i=\lnot\bigvee A_i \]
\(\land,\lor\) 各自的结合律、交换律等。
如果 \(B\) 与 \(A\) 逻辑等价，则将 \(B'\) 中 \(B\) 的一次或多次出现替换成 \(A\) 而得到的命题形式 \(A'\)，其与 \(B'\) 逻辑等价。
对于一个仅由 \(\lnot,\land,\lor\) 确定的 受限命题形式 (restricted statement form) \(A\)，\(\lnot A\) 可以通过：
- 将全体 \(\lor\) 换成 \(\land\)、\(\land\) 换成 \(\lor\)。
- 将所有命题变量换成其逆。
而得到。证明归纳。

一切真值表都可以以受限命题形式给出。

析取范式 (disjunctive normal form) 是形如

\[\bigvee_{i=1}^n\left(\bigwedge_{j=1}^mQ_{ij}\right) \]

的命题形式，其中 \(Q_{ij}\) 是命题变量或其否定。

合取范式 (conjunctive normal form) 是形如

\[\bigwedge_{i=1}^n\left(\bigvee_{j=1}^mQ_{ij}\right) \]

的命题形式，其中 \(Q_{ij}\) 是命题变量或其否定。

任何非矛盾式的命题形式都与析取式逻辑等价，而非重言式都与合取式逻辑等价。

完备联结词集合 (adquate sets of connective) 是足矣组合一切真值表的联结词集合。\(\cur{\lnot,\land,\lor}\) 是完备的，\(\cur{\lnot,\lor},\cur{\lnot,\land},\cur{\lnot,\to}\) 同样都是完备的。\(\cur{\t{NAND}},\cur{\t{NOR}}\) 是大小为 \(1\) 的完备集合的例子。

一个 论证形式 (argument form) 是命题形式列，其中结尾的命题形式被称作结论 (conclusion)，而其它都是前提 (premise)。论证形式是 不合法 (invalid) 的，如果存在全体前提都取真但结论取假的赋值；反之则是合法 (valid) 的。

论证形式可以有 \(A_1,A_2,\dots,A_n;\therefore A\) 的记法，表示 \(A_1,\dots,A_n\) 是前提而 \(A\) 是结论。而其合法，当且仅当 \((A_1\land A_2\land\dots\land A_n)\to A\) 是重言式。

II. Formal Statement Calculus

形式（逻辑）系统 (Formal (Logical) System) 是一类系统的总称：

有一个符号构成的、可以包含无限多字符的字典。
有一个包含这些符号构成的有限串的集合，即 良构公式 (well-formed formula, wf.)。
一些特定的良构公式，称作公理 (axiom)。
一个有限集的推导规则。某条具体的推导规则，是可以从一个良构公式有限集出发，得到一个特定的良构公式，即该规则的直接推论 (direct consequence)。

从公理出发根据推导规则得到的所有东西都称作定理。

形式演绎系统 (formal deductive system，或称 L) 或 命题逻辑 (formal statement calculus) 首先是一个形式逻辑系统。

其字符集为全体形式变量 \(p_i\)，以及 \(\lnot\)、\(\to\)、\((\)、\()\)。
其 wf. 包括：
- \(p_i\)。
- 如果 \(A,B\) 是 wf.，则 \(\lnot A\) 和 \(A\to B\) 是 wf.
- 由前两条生成的全体 wf.
其公理包括：
- (L1): \(A\to(B\to A)\)
- (L2): \((A\to(B\to C))\to((A\to B)\to(A\to C))\)
- (L3): \((\lnot A\to\lnot B)\to(B\to A)\)。
- 每个公理都只是一个形式，其具体的实例是无穷多的。
推导规则只有一条 modus ponens 肯定前件式 modus ponens 肯定前件式 (MP)：由 \(A\) 和 \(A\to B\)，可以得到直接推论 \(B\)。

因为 \(\cur{\lnot,\to}\) 是完备联结词集合，所以一切真值表都可以被 wf. 描述，而一切命题形式都逻辑等价于某个 L 中的 wf.。然而，须牢记，命题形式是 Informal Statement Calculus 中的内容，其可以包含 \(\land,\lor\) 乃至其它众多联结词；逻辑等价同样也是 ISC 的部分。然而，良构公式是另一个板块的内容：虽然其自然地与 ISC 兼容。

L 上的一个证明 (proof) 是 wf. 序列 \(A_1,\dots,A_n\)，每一项或者是公理，或者是前面某两项 \(A,A\to B\) 导出的结论。这个证明是关于 \(A_n\) 的，此时可称 \(A_n\) 是一个定理，记作 \(\vdash_LA_n\)。

注意：

只有满足 \(A,A\to B\) 的两项才能应用 MP 导出 \(B\) 的推论。
截取 \(A_n\) 证明的一个前缀，其仍是证明。因此，该序列中的全体 \(A_i\) 均是定理。
公理必是定理。

例题：证明 \(\vdash_L(A\to A)\)。

\(A\to((A\to A)\to A)\) (Axiom.L1)

\((A\to((A\to A)\to A))\to((A\to (A\to A))\to(A\to A))\) (Axiom.L2)

\((A\to (A\to A))\to(A\to A)\) (Consequence.1&2)

\(A\to(A\to A)\) (Axiom.L1)

\(A\to A\) (Consequence.3&4)

从 L 上某个 wf. 集合 Γ 出发，可以进行演绎 (deduction)。演绎同样是 wf. 序列 \(A_1,\dots,A_n\)，每一项或者是公理或 Γ 中 wf.，或者是前面某两项 \(A,A\to B\) 导出的直接推论。\(A_n\) 被称作自 Γ 可演绎的 (deducible)，也称作 Γ 的推论 (consequence)，可记作 \(\Gamma\vdash_L A_n\)。

注意，这里的 Γ 中的 wf. 不一定是定理（定理必须是重言式），这是这个定义最重要的特征。

例题：\(\cur{A,(B\to(A\to C))}\vdash_L(B\to C)\)。

\(A\) (Prop.1)

\(A\to(B\to A)\) (Axiom.1)

\(B\to A\) (Consequence.1&2)

\(B\to(A\to C)\) (Prop.2)

\((B\to(A\to C))\to((B\to A)\to(B\to C))\) (Axiom.2)

\((B\to A)\to(B\to C)\) (Consequence.4&5)

\(B\to C\) (Consequence 3&6)

演绎定理 (Deduction Theorem)：\(\Gamma\cup\cur{A}\vdash_LB\) 当且仅当 \(\Gamma\vdash_L(A\to B)\)。

假言三段论 (Hypothetical Syllogism, HS)：\(\cur{A\to B,B\to C}\vdash_L A\to C\)。

例题：\(\vdash_L(\lnot B\to(B\to A))\)。

\(\lnot B\to(\lnot A\to\lnot B)\) (Axiom.1)

\((\lnot A\to\lnot B)\to(B\to A)\) (Axiom.3)

\(\lnot B\to(B\to A)\) (HS.1&2)

这个例题的效果是，如果 \(\lnot B\) 和 \(B\) 都是定理（即系统的一致性被破坏），则一切命题都是定理。

例题：\(\vdash_L((\lnot A\to A)\to A)\)。

核心是使用 Axiom.L3 先转成 \(\lnot A\to\lnot(\lnot A\to A)\)，然后 \((\lnot A\to A)\to(\lnot A\to\lnot(\lnot A\to A))\) 作为一个整体搭配上 \((\lnot A\to(A\to\lnot(\lnot A\to A)))\) 是 Axiom.L2 的形式，这又是 \(\lnot A\to(\lnot\lnot(\lnot A\to A)\to\lnot A)\) 导出的三段论。

这个例题的效果是，如果 \(\lnot A\vdash_L A\)，则 \(\vdash_L A\)。

L 上的一次赋值 (valuation) 是为全体 wf. 赋以真值的方式，使得对于一切 wf. \(A,B\)，都有：

\(v(A)\neq v(\lnot A)\)。
\(v(a\to b)=\F\)，当且仅当 \(v(A)=\T\) 而 \(v(F)=\t F\)。
即，赋值需要满足 \(\lnot\) 和 \(\to\) 两个联结词的“定义”。

L 中的全体变量赋真值的方式确定，则一组赋值方案即确定。一个 wf. 是重言式，假如在一切赋值下其均为真。

健全性定理 (soundness theorem)：每个定理都是重言式。

对定理的证明列归纳即可。

但是其逆呢？这需要我们借助一些工具。

一个形式逻辑系统的扩张 (extension) 是扩充系统中的公理，并保证所有原先定理仍是定理的新系统。但是，我们并不希望 \(A\) 和 \(\lnot A\) 同时成为定理（如果这样的话，由之前的定理 \(\vdash_L(\lnot B\to(B\to A))\)，所有 wf. 就全是定理了，那么这个系统就毫无意义了）。因此，我们再定义一个标准：

一致性 (consistency)：\(A\) 和 \(\lnot A\) 不能同为定理。这等效于，存在非定理的 wf.，因此 L 显然是一致的。

定理：对于 L 的一致扩展 L*（在这里，它被看作进一步扩展的中间态），考虑 L* 中的一个非定理的 wf. \(A\)，则将 \(\lnot A\) 看做一个新公理后得到的 L**，会仍是一致的。

完全性 (completeness)：一个 wf. 和它的否定，二者至少有一个是定理。

这个定义非常强，因为在 L 中存在太多自身和否定均非定理的 wf. 了。
不一致的系统必然完全：因为两个都是定理也符合完全性的定义。
完全系统不可能再存在一个扩充定理集合的扩张。

定理：令 L* 是一致扩张，则其可以被进一步扩张得到某个一致完全扩张。

wf. 是可数集，因此可以顺次列举为 \(A_0,A_1,\dots\)。令 \(L_0=L^*\)，然后依次判定：

若 \(\vdash_{L_n}A_n\)，则 \(L_{n+1}=L_n\)。

否则 \(L_{n+1}\) 是 \(L_n\) 引入新公理 \(\lnot A_n\) 得到的扩张。

最后定义 \(L^C\) 的公理集合是全体 \(L_n\) 的公理集合的并。

L^C 是一致的。这是因为，若 \(A\) 和 \(\lnot A\) 都是定理，则存在一个充分大的 \(n\) 使得 \(L_n\) 包含了二者推导所需的一切公理，则 \(L_n\) 中 \(A\) 和 \(\lnot A\) 也是定理，则 \(L_n\) 不一致，产生矛盾。

L^C 是完全的，因为每个定理都会被枚举到。

定理：令 L* 是 L 的一致扩张，则存在赋值使得 L* 中所有定理都取真。

区别：L 中所有定理都是重言式（这是我们证明的目标），因此任意赋值均使得 L 中所有定理都取真。

找到一致完全扩张然后看其中 \(A\) 或 \(\lnot A\) 哪个是定理，然后赋值即可。

完善性 (adequacy)：所有重言式都是定理。L 的 完善性定理 (adequacy theorem) 证明了 L 的完善性。

对于重言式 \(A\)，若其并非定理，则可以扩充 \(\lnot A\) 为公理得到一致扩张 L*。然后由前述定理，存在所有定理都取真的赋值，因此存在 \(\lnot A\) 的真赋值，与 \(A\) 的重言性相悖。

总结：

L 健全 (sound)、一致 (consistent)、完善 (adequate)，但不完全 (complete)。

III. Informal Predicate Calculus

非正式谓词逻辑 (Informal Predicate Calculus) 研究量词 (quantifier)，包括 全称量词 (universal quantifier) \(\forall\) 和 存在量词 (existential quantifier) \(\exists\)。二者之间存在转化关系：“存在”不成立，就是并非“全部”不成立。

\[(\exists x)A\iff\lnot(\forall x)\lnot A \]

将其形式化的结果，就是 一阶语言 (first-order language)，其由如下成分组成：

变量 (variable) \(\cur{x_i}\)。
独立常量 (individual constant) \(\cur{a_i}\)。
谓词 (predicate letter) \(\cur{A_i^n}\)，是一种特殊的函数，接受参数后返回 true/false。其中的上标 \(n\) 是接受的参数数目。谓词的另一种理解方式类似（多元）关系。
函数 (function letter) \(\cur{f_i^n}\)。
标点符号 (punctuation symbol) \((\)、\()\) 和 \(,\)。
联结词 (connective) \(\lnot,\to\)。
量词 (quantifier) \(\forall\)。注意只有 \(\forall\) 一个，\(\exists\) 因为其与 \(\forall\) 的互相转化性所以被舍去了。

Remarks：

独立常量的作用是填入谓词或函数中，充当一个元。
函数可以作为谓词和函数的元，而谓词不能；谓词被用于当作 wf. 的一部分（虽然我们目前其实没有介绍一阶语言中的 wf. 是什么）。
为什么是一阶语言？因为它只有对变量的量词，没有对函数、谓词的量词（泛函）。

一阶语言 \(\c L\) 中的基础单元是项 (term)。

变量和独立常量都是项。
如果 \(t_1,\dots,t_n\) 都是项，那么 \(f_i^n(t_1,\dots,t_n)\) 也是项。
所有项由这两条生成。

项是那些被看做物品 (object) 的表达式，它们可以具有一些性质(property)、被针对做出一些断言 (assertion)。

而谓词可以通过项生成 \(A_i^n(t_1,\dots,t_n)\) 的 原子公式 (atomic formula)：其中 \(A_i^n\) 是谓词，而每个 \(t_i\) 都是项。

谓词则被看作是针对项做出的断言，原子 (atomic) 的前缀意味着其是不可分割的——

由此可以定义 \(\c L\) 中的 良构公式 (well-formed formula, wf.)：全体原子公式，以及 \(\lnot A,A\to B\) 和 \((\forall x_i)A\)，其中 \(A,B\) 是 wf.，而 \(x_i\) 是某个变量。

——而良构公式是可以分割的。

\((\forall x_i)A\) 中的 \(x_i\) 不需要与 \(A\) 有任何关联：它可以在 \(A\) 中没有任何出现。
\(\exists,\land,\lor\) 等符号确实可以使用：但是这些字符并非一阶语言中的符号，而是人为后天定义 (defined) 的符号。
\(\lnot,\forall\) 等符号的优先级是最高的。这意味着，\((\forall x_i)A\to B\) 没有省略任何括号，与 \((\forall x_i)(A\to B)\) 应该作不同理解。

在式 \((\forall x_i)A\) 中，称 \(A\) 是这个量词的 作用域 (scope)。在这样的一个 wf. 中，\(x_i\) 的所有出现（无论其是最外层的 \(\forall x_i\) 中的出现还是 \(A\) 内部的出现）都是被称作是受限 (bound) 的。否则，这次出现就是自由 (free) 的。更一般地，如果 \(((\forall x_i)A)\) 作为某个 wf. \(B\) 的子式 (subformula) 出现，也可以这么说。

注意，这里的 \(A\) 指代一个整体的 wf.，它并非字典中的字符。也可以有 \(A(x_1,\dots,x_n)\) 的记法，此时我们关注某些特定的项。此时，我们经常（但并非总是）认为 \(x_1,\dots,x_n\) 在 \(A\) 中是自由的；而如果 \(x_i\) 确实是自由的，那么对于 \(A(x_i)\) 的描述，\(A(t)\) 就可以指代把全体 \(x_i\) 的出现替换为 \(t\) 的新 wf. 。

例：下式中红色字是自由的，蓝色字是受限的。

\[(\forall{\color{blue}x_1})(A_1^2({\color{blue}x_1},{\color{red}x_2})\to(\forall{\color{blue}x_2})A_2^1({\color{blue}x_2})) \]

定义项 \(t\) 在 \(A\) 中对变量 \(x_i\) 自由 (free for \(x_i\) in \(A\))，如果 \(x_i\) 在 \(A\) 中的所有自由出现都不位于某个 \((\forall x_j)\) 的作用域中，其中 \(x_j\) 在 \(t\) 中出现。即，\(t\) 对 \(x_i\) 不自由，如果存在 \(x_j\) 使得：

\(t\) 中存在 \(x_j\) 的字段。
\(A\) 中存在 \(\dots (\forall x_j)(\dots x_i\dots)\) 的字段，且此处的 \(x_i\) 是自由的。

也即，如果 \(t\) 在 \(A\) 中对 \(x_i\) 自由，那么将 \(x_i\) 替换为 \(t\) 并不会引入新的量词与自由元的交互。

一个例子是，\(x_i\) 在一切 \(A\) 中都对 \(x_i\) 自由：因为 \(x_i\) 在 \(A\) 中的自由出现不能位于任何 \((\forall x_i)\) 的内部。

\(\c L\) 上的一个解释 (interpretation) \(I\) 由以下部分构成：

非空集合 \(D_I\)，称作 \(I\) 的 定义域 (domain)。
一个 \(D_I\) 上的元素集合 \((\bar a_1,\dots)\)，是独立常量取值。
一个 \(D_I\) 至自身的多元函数集合 \((\bar f_1^n,\dots)\)，是函数取值。
一个 \(D_I\) 上的多元关系集合 \((\bar A_1^n)\)，是谓词取值。

在一阶语言中，在讨论 wf. 的真伪时，只能在具体的解释 (interpretation) 下进行。例如，“对于一切自然数 \(x,y\)，都存在自然数 \(z\) 使得 \(x+z=y\)”，这就是一个解释，解释依赖加法函数、相等谓词等具体实例，而在这个解释下，这个 wf. 是错的。然而，同一个 wf. 也可以有“对于一切正有理数 \(x,y\)，都存在正有理数 \(z\) 使得 \(xz=y\)”，这个解释下的该 wf. 是正确的。

有的时候，解释还不够（这发生在有自由出现的场合）。因此进一步可以还定义赋值 (valuation)。同命题逻辑一致，此时的赋值是项到 \(D_I\) 中元素的映射，满足：

\(v(a_i)=\bar a_i\)。
\(v(f_i^n(t_1,\dots,t_n))=\bar f_i^n(v(t_1),\dots,v(t_n))\)。

Remarks：

在一个解释的基础上通常可以定义多种赋值。
赋值是关于项的分析，而非关于 wf. 的分析。在全体变量的 \(v(x_i)\) 确定后，整体赋值也随之确定。

两个赋值 \(v,v'\) 被称作是 \(i\)-等价 (\(i\)-equivalent) 的，如果对于一切 \(j\neq i\)，都有 \(v'(x_j)=v(x_j)\)。也即，除了 \(x_i\) 的赋值，其它变量的赋值全同。

令 \(A\) 是一个 wf.，令 \(I\) 是对其的一个解释，则 \(I\) 上的一个赋值 \(v\) 被称作满足 (satisfy) \(A\)，如果：

当 \(A\) 是原子公式 \(A_j^n(t_1,\dots,t_n)\) 时，其被满足，当且仅当 \(\bar A_j^n(v(t_1),\dots,v(t_n))\) 在 \(D_I\) 上为真。
当 \(A\) 是否定式 \(\lnot B\) 时，其被满足，当且仅当 \(B\) 不被满足。
当 \(A\) 是推导式 \(B\to C\) 时，其被满足，当且仅当 \(\lnot B\) 或 \(C\) 至少一者被满足。
当 \(A\) 是量词式 \((\forall x_i)B\) 时，其被满足，当且仅当所有 \(i\)-等价于 \(v\) 的 \(v'\) 都满足 \(B\)。

Remark：

验证满足性的过程是递归式的。
一个 wf. 或它的否定，二者恰有一个被一组赋值满足。
最后一条的意义是，在出现 \((\forall x_i)B\) 时，这就相当于 \(v\) 中对 \(x_i\) 的赋值短暂失效了，而这是符合实际意义的。

定理：令 \(x_i\) 在 \(A(x_i)\) 中自由。令 \(t\) 在 \(A\) 中对 \(x_i\) 自由。令 \(v\) 是一个赋值，而 \(v'\) 是与之 \(i\)-等价且 \(v'(x_i)=v(t_i)\) 的赋值，则 \(v\) 和 \(v'\) 具有相同的满足性。

定义：一个 wf. 在某个解释下为真 (true)，如果所有赋值都满足之；为假 (false)，如果都不满足。有 \(I\vDash A\) 的表示 \(A\) 在 \(I\) 下为真的记法。

存在非真非假的解释。
因为解释的定义域须非空，所以赋值集合非空，所以不能既真又假。
\(A\) 为假当且仅当 \(\lnot A\) 为真。
\(A\to B\) 为假当且仅当 \(A\) 为真而 \(B\) 为假。
如果 \(A\) 和 \(A\to B\) 都为真，则 \(B\) 为真。
对于任何变量 \(x_i\) 和任何 wf. \(A\)，\(I\vDash A\) 当且仅当 \(I\vDash(\forall x_i)A\)。

这其实比较显然：\((\forall x_i)A\) 与 \(A\) 的区别是，前者的一组赋值要为真，需要全体 \(i\)-等价赋值均为真；而二者中任何一者 作为解释下的 wf. 为真，都需要全体赋值为真。

推论：对于任何变量 \(y_1,\dots,y_n\) 和任何 wf. \(A\)，都有 \(I\vDash A\iff I\vDash(\forall y_1)\dots(\forall y_n)A\)。

也可以有另一种看法：一组解释为真，当且仅当对于一切赋值为所有变量都添加上全称量词对于一切赋值为所有变量都添加上全称量词其为真。

同理，一个赋值 \(v\) 满足 \((\forall x_i)A\)，当且仅当存在一个 \(i\)-等价的 \(v'\) 满足 \(A\)。

对于命题逻辑 L 上的一个 wf. \(A_0\)，由其可以得到一阶语言 \(\c L\) 上的一个 替换实例 (substitution instance)：只需要把 \(A_0\) 中的全体命题变量替换为 \(\c L\) 上的某个项即可（相同命题变量须替换为相同项）。这合法，因为 L 和 \(\c L\) 的联结词均只有 \(\to,\lnot\) 两个。

\(\c L\) 上的一个 重言式 (tautology) 是 L 上重言式的替换实例。

定理：\(\c L\) 上的重言式在一切解释下均为真。

一个 wf. \(A\) 是封闭 (closed) 的，如果其中没有自由变量。两个关于全体自由变量均相等的赋值必然具有相同的满足性。故，一个封闭 wf. 在任意解释下均非真即假。

一个 wf. \(A\) 是 逻辑有效 (logically valid) 的，如果在一切解释下均为真；是矛盾 (contradictory) 的，如果均为假。

事实上，逻辑有效等效于重言。

IV. Formal Predicate Calculus

命题逻辑可以被扩充为 谓词逻辑 (formal predicate calculus) K_L。其 wf. 集合为 \(\c L\)，而其上公理包括：

(K1) \(A\to(B\to A)\)。
(K2) \((A\to(B\to C))\to((A\to B)\to(A\to C))\)。
(K3) \((\lnot A\to\lnot B)\to(B\to A)\)。
(K4) \(x_i\) 在 \(A\) 中没有自由的出现，则 \(((\forall x_i)A)\to A\)。
(K5) 如果 \(t\) 在 L 中对 \(A(x_i)\) 关于 \(x_i\) 自由，则 \(((\forall x_i)A(x_i))\to A(t)\)。
(K6) \(x_i\) 在 \(A\) 中没有自由的出现，则 \(((\forall x_i)(A\to B))\to(A\to(\forall x_i)B)\)。

推导规则则是

modus ponens 肯定前件式 modus ponens 肯定前件式 (MP)，从 \(A\) 和 \(A\to B\) 推出 \(B\)。
generalization 一般化 generalization 一般化 (Gen)，从 wf. \(A\) 推出 \((\forall x_i)A\)，其中 \(x_i\) 可以是任意变量。需要注意的是，这个东西不能写作 \(A\to(\forall x_i)A\)，因为二者含义不同：前者是从定理 \(A\) 出发的推导，后者的 \(A\) 不一定是定理，而可以是一个普通的命题。

Remark：

考虑实例 \((\forall x_i)A\to A\)：如果 \(x_i\) 在 \(A\) 中自由，那么由 K5 其成立，否则由 K4 成立。

证明 (proof)、定理 (theorem)、演绎 (deduction)、推论 (consequence) 等定义被继承了。

定理：重言式都是定理。

重言式是 L 上重言式（由 adequacy，其必是定理）的替换实例，因此对其证明链替换即得 K_L 上证明。

定理：K456 的全体实例都是逻辑有效的。

因此我们仍有 健全性定理 (Soundness Theorem)：K_L 上的定理都是逻辑有效的。

归纳。所有公理都逻辑有效；MP，在 \(A\) 和 \(A\to B\) 均逻辑有效时 \(B\) 也逻辑有效；Gen，我们已知 \(I\vDash A\) 当且仅当 \(I\vDash(\forall x_i)A\)。

因此有推论：K_L 具有一致性 (consistency)，因为逻辑有效式的否定必然非逻辑有效。

演绎定理 (deduction theorem) 在 K_L 上的形式有所差别：如果 \(\Gamma\cup\cur{A}\vd_KB\)，并且推导过程中不含任何牵扯到 \(A\) 中自由变量的 generalization，则 \(\Gamma\vd_K(A\to B)\)。

一个演绎定理的反例是，有 \(\cur{A}\vdash_K(\forall x_i)A\)，但没有 \(\vdash_KA\to(\forall x_i)A\)。这并非违背了 generalization，而是 generalization 只有在 \(A\) 是永真式（定理）时才成立。【反之，MP 在某个具体的 interpretation 下，或是在两个永真式间，均成立，因此只有 Gen 要单独讨论】

例如，命题 \(A_1^2(x_1,x_1)\) 不是定理：当 \(A_1^2\) 是“相等”关系时，有 \(A\vd_K(\forall x_i)A\)；但是 \(A_1^2(x_1,x_1)\to(\forall x_1)A_1^2(x_1,x_1)\) 并非定理（因为其非永真式），所以其不能被推出。

当然也可以使用演绎定理的变种：

如果 \(\Gamma\cup\cur{A}\vd_KB\) 且 \(A\) 是封闭 (closed，即无自由变量) 的 wf.，则必然有 \(\Gamma\vd_K(A\to B)\)。
（逆演绎定理）如果 \(\Gamma\vd_K(A\to B)\)，则必然有 \(\Gamma\cup\cur{A}\vd_KB\)。

假言三段论 (Hypothetical Syllogism, HS) 仍然可用。

例：如果 \(x_i\) 在 \(A(x_i)\) 中自由，且 \(x_j\) 是一个未在 \(A(x_i)\) 中出现的变量，则有 \(\vd_K(\forall x_i)A(x_i)\getsto(\forall x_j)A(x_j)\)。

\((\forall x_i)A(x_i)\to A(x_j)\) (K5)

\(\forall x_j[(\forall x_i)A(x_i)\to A(x_j)]\). (Generalization from 1)

\(\forall x_j[(\forall x_i)A(x_i)\to A(x_j)]\to[(\forall x_i)A(x_i)\to(\forall x_j)A(x_j)]\) (K6)

\((\forall x_i)A(x_i)\to(\forall x_j)A(x_j)\) (MP)

反之亦然。

例：如果 \(x_i\) 在 \(B\) 没有自由出现，则 \(\vd_K((\forall x_i)(A\to B))\to(((\exists x_i)A)\to B)\)。

证明：

\(((\forall x_i)(A\to B))\to(A\to B)\) (K4/K5)

\((A\to B)\to(\lnot B\to\lnot A)\) (K3)

\(((\forall x_i)(A\to B))\to(\lnot B\to\lnot A)\) (HS)

\((\forall x_i)(((\forall x_i)(A\to B))\to(\lnot B\to\lnot A))\) (Gen)

\(((\forall x_i)(A\to B))\to((\forall x_i)(\lnot B\to\lnot A))\) (K6&MP from 4)

\(((\forall x_i)(\lnot B\to\lnot A))\to(\lnot B\to(\forall x_i)\lnot A)\) (K6)

\((\lnot B\to(\forall x_i)\lnot A)\to(\lnot(\forall x_i)\lnot A\to\lnot\lnot B)\) (K3)

对 567 连用两次 MP 吧！可以直接使用 \(\lnot\lnot B=B\) 的引理（虽然还没有证过）。

\(A\getsto B\) 并非 wf.：其可以被看做 \(\lnot((A\to B)\to\lnot(B\to A))\) 的简写。

定理：\(\vdash_K A\getsto B\) 当且仅当 \(\vdash_K A\to B\) 且 \(\vdash_K B\to A\)。

当 \(\vdash_KA\getsto B\) 时，我们称二者是 可证明等价 (provably equivalent) 的。可证明等价具有自反性、交换性和传递性。

定理：如果 \(x_i\) 在 \(A(x_i)\) 中自由，\(x_j\) 在 \(A(x_i)\) 中没有任何出现，则

\[\vdash_K((\forall x_i)A(x_i))\getsto((\forall x_j)A(x_j)) \]

定理：对于全体自由变量为 \(y_1,\dots,y_n\) 的 \(A\)，\(\vdash_KA\) 当且仅当 \(\vdash_K(\forall y_1)\dots(\forall y_n)A\)。后者被称作 \(A\) 的 全称闭包 (universal closure)，常常被简记作 \(A'\)。

\(A\) 和 \(A'\) 只有在一者为定理时才可证明等价；均非定理时则不一定，原因还是因为 Gen 需要定理。但是 \(A'\to A\) 是显然成立的（K5）。

定理：考虑有基础命题 \(A_0\)；令 \(B_0\) 是 \(A_0\) 将其中 \(A\) 的一次或多次出现替换为 \(B\) 得到的 wf.，则\

\[\vdash_K((A\getsto B)'\to(A_0\getsto B_0)) \]

推论：如果 \(\vd_KA\getsto B\)，则 \(\vd_K(A_0\getsto B_0)\)。

推论：如果 \(x_j\) 在 \(A(x_i)\) 中没有任何出现，则在 \(A_0\) 中将 \((\forall x_i)A(x_i)\) 替换为 \((\forall x_j)A(x_j)\) 得到的 \(B_0\) 必有 \(\vd_K(A_0\getsto B_0)\)。

定理：如果 \(x_i\) 在 \(A\) 中没有自由出现，则

\(\vd_K(\forall x_i)(A\to B)\getsto(A\to(\forall x_i)B)\) (K6 及其逆)
\(\vd_K(\exists x_i)(A\to B)\getsto(A\to(\exists x_i)B)\)

定理：如果 \(x_i\) 在 \(B\) 中没有自由出现，则

\(\vd_K(\forall x_i)(A\to B)\getsto((\exists x_i)A\to B)\)
\(\vd_K(\exists x_i)(A\to B)\getsto((\forall x_i)A\to B)\)

这说明 \(((\forall/\exists\cdot)\cdot)\to((\forall/\exists\cdot)\cdot)\)，可以被转成 \((\forall/\exist\cdot)(\cdot\to\cdot)\)，而反之亦然！后一种形式是好的，因为它直接是一个简洁的

\[(Q_1x_{i1})(Q_2x_{i2})\dots(Q_kx_{ik})D \]

的形式，其中 \(D\) 是不含量词的 wf.，\(Q_i\) 是量词。这种形式被称作 前束范式 (prenex form)。

定理：任意 wf. 都等价于前束范式 wf.。

前束范式可以分为以下两种：

Π_n 形式 (Π_n form)，以 \(\forall\) 量词开头，然后两种量词形成的极长连续段交替 \(n-1\) 次。
Σ_n 形式 (Σ_n form)，同理，以 \(\exists\) 开头并交替 \(n-1\) 次。

易知，每一种前束范式必然是 Π_n 或 Σ_n 之一。

重言式都是定理；K_L 上的定理都是逻辑有效的；然后就是最后一条 完善性定理 (adequacy theorem)：逻辑有效的都是定理，证明 K_L 的完善性了。证明同 L 的完善性。

唯一的区别是，只能添加封闭的 wf. 为公理。

这也被称作 Gödel 完备性定理 (Gödel's Completeness Theorem)。

对于 wf. 集合 Γ，使得其中全体 wf. 都为真的解释 \(I\) 被称作 Γ 上的一个模型 (model)。一个一阶系统 \(S\) 上的模型是使得其中全体定理都为真的解释。

定理：只要全体公理都取真，则 \(I\) 就是 \(S\) 上的模型。

定理：\(S\) 一致当且仅当存在模型。

一致当且仅当存在非定理者；而模型是一种解释，解释必然存在假式，在某种解释下为假的式子则必非定理。

定理：一致系统 \(S\) 下，在所有模型下均取真的封闭 wf. 是定理。

若其不是定理，则将其逆作为公理引入后产生矛盾。

Löwenheim-Skolem 定理：如果一个一阶系统存在模型，则存在定义域为可数集的模型。

紧性定理 (Compactness Theorem)：如果公理集合的全体有限子集都有对应模型，则该一阶系统存在模型。

推论：对于无穷的 wf. 集合 Γ，如果其全体有限子集都有模型，则其存在模型。

V. Mathematical Systems

在数数中，有一些命题是正确的：

对于自然数 \(x,y\)，如果 \(x=y\) 那么 \(x=y\)。

但是，它的正确性是来自于逻辑 (logically)：K_L 中有 \((\forall x_1)(\forall x_2)(A_1^2(x_1,x_2)\to A_1^2(x_1,x_2))\) 作为定理。

然而，命题

对于自然数 \(x,y\)，如果 \(x=y\) 那么 \(y=x\)。

的正确性是来自于 \(=\) 的性质，或者说来自于算数 (mathematically)：其对应的 wf. 并非定理。

我们自然可以添加一些其它公理，使得上式对应的 wf. 成为定理。这些新添加的公理被称作 专用公理 (proper axioms)，与 逻辑公理 (logical axioms) K1~K6 做出区分。由此，即得到 K_L 的一个一致扩展，所谓的 数学系统 (mathematical system)。

Remark：任何包含逻辑推理的理论都是谓词逻辑的一致扩展，同时也是谓词逻辑上的一个模型；新理论被唯一确定、建立某些新的定理，就需要引入新公理。

例如，代表相等的系统 E 就多了如下三条描述特定谓词，等价性方法 \(A_1^2(x_1,x_2)\) 的公理：

(E7) \(A_1^2(x_1,x_1)\)
(E8) \(A_1^2(t_k,u)\to A_1^2(f_i^n(t_1,\dots,t_k,\dots,t_n),f_i^n(t_1,\dots,u,\dots,t_n))\)
(E9) \(A_1^2(t_k,u)\to(f_i^n(t_1,\dots,t_k,\dots,t_n)\to f_i^n(t_1,\dots,u,\dots,t_n))\)

由这些公理可以证明 \((\forall x_1)(\forall x_2)(A_1^2(x_1,x_2)\to A_1^2(x_2,x_1))\)。这三条公理被称作 相等公理 (axioms for equality)。E，以及其一切一致扩展，被称作 含相等关系的一阶系统 (first order system with equality)。

因此，可以使用 \(x_1=x_2\) 这个记号来描述该关系。但是注意，这里的等号仅仅是一个为方便表述的形式记号，wf. 的字符集中不包括这个等号。另一种说法是，存在一种把 \(A_1^2\) 解释为等号（这里的等号是符合传统认知的等号而非手动定义的等号）的模型。这样的模型被称为 正规模型 (normal model)。

裙论也可以用一阶系统描述：其包含独立常量的单位元；逆元、乘法两个函数；相等的谓词符号。其公理是乘法结合律、左单位元、左逆元三条。

算数 (arithmetic) 同理。常量 \(a_1=0\)，方法 \(f_1^1(\cdot)\) 取后继，方法 \(f_1^2(\cdot,\cdot)\) 求和，方法 \(f_2^2(\cdot,\cdot)\) 求积，则代表自然数的系统 N 就多了如下公理：

(N1) \((\forall x_1)\lnot(f_1^1(x_1)=a_1)\)——所有自然数的后继均非零。
(N2) \((\forall x_1)(\forall x_2)(f_1^1(x_1)=f_1^1(x_2)\to x_1=x_2)\)——后继相等则原数相等。
(N3) \((\forall x_1)(f_1^2(x_1,a_1)=x_1)\)——\(0\) 与一切自然数求和是本身。
(N4) \((\forall x_1)(\forall x_2)(f_1^2(x_1,f_1^1(x_2))=f_1^1(f_1^2(x_1,x_2)))\)——归纳求和。
(N5) \((\forall x_1)(f_2^2(x_1,a_1)=a_1)\)——\(0\) 与一切自然数求积是 \(0\)。
(N6) \((\forall x_1)(\forall x_2)(f_2^2(x_1,f_1^1(x_2))=f_1^2(f_2^2(x_1,x_2),x_1)\)——归纳求积。
(N7) \(A(a_1)\to((\forall x_1)(A(x_1)\to A(f_1^1(x_1)))\to(\forall x_1)A(x_1))\)，其中 \(x_1\) 在 \(A\) 中自由。此乃归纳法。

其中，N1、N2 和 N7 被称作 Peano 假设 (Peano's Postulate)。

正如在 E 中使用 \(=\) 取代了繁琐的 \(A_1^2\) 一般，此时我们亦可使用 \('\) 表示后继，\(+\) 表示加法，\(\times\) 表示乘法。使用 \(0\) 表示 \(a_0\)，但是也只有 \(0\) 是 N 中符号，\(1,2,\dots\) 均不是：它们指代的是 \(0',0'',\dots\)。可以使用 \(0^{(n)}\) 表示 \(n\)。

我们非常关心 N 是否完全：这关系到算数系统中是否可能存在既非真又非假的命题。更进一步地，如果存在这样的命题，则通过将其和其否定分别作为两条公理，可以得到 N 的两个不同的分支扩展。而由下文中将阐述的 Gödel 不完备性定理 (Gödel's Incompleteness Theorem)，很遗憾，N 不是完全的。

VI. The Gödel Incompleteness Theorem

定义：一个 \(k\) 元关系 \(R\) 在 N 上是 可表示 (expressible) 的，如果存在一个有 \(k\) 个自由变量的 wf. \(A\) 满足：

\(R(n_1,\dots,n_k)\) 成立则有 \(\vd_N A(0^{(n_1)},\dots,0^{(n_k)})\)。
不成立则有 \(\vd_N\lnot A(\dots)\)。

Remark：

假如 N 有完全性，则上述描述可以直接写成“当且仅当”。但是很遗憾它没有。
因此，并非每一个 wf. 都确定一个关系。
\(n\) 元函数是一种特殊的 \(n+1\) 元关系：对于确定的前 \(n\) 元取值，其仅在唯一的 \(n+1\) 元上取真。

相等关系是一个可表示关系的例子。\(\leq\) 也显然：\(m\leq n\) 当且仅当 \((\exists x_1)(0^{(m)}+x_1=0^{(n)})\)。

“素数判定”这个一元关系甚至都是可表示的：\(P(0^{(n)}):(\forall x_1)(0''\leq x_1\to(\forall x_2)(0''\leq x_2\to\lnot(x_1\times x_2=0^{(n)})))\)。

引：一个关系是 recursive 的，当且仅当其在一阶算数 N 上可表示；而 total general recursive function 又与 Turing 可决定性等价。

原始递归函数 (Primitive Recursive Functions)：

基础函数
- 零 (zero) 函数 \(f(n)=0\)。
- 后继 (successor) 函数 \(f(n)=n+1\)。
- 投影 (projection) 函数 \({p^k}_i:{p^k}_i(n_1,\dots,n_k)=n_i\)。
复合 (composition) 法则：对于函数 \(g(n_1,\dots,n_j)\) 和 \(1\leq i\leq j\) 的 \(h_i(n_1,\dots,n_k)\)，可以定义复合

\[f(n_1,\dots,n_k)=g(h_1(\dots),\dots,h_j(\dots)) \]
递归 (recursion) 法则：对于 \(g(n_1,\dots,n_k)\) 和 \(h(n_1,\dots,n_{k+2})\)，可以定义

\[f(n_1,\dots,n_k,0)=g(n_1,\dots,n_k) \\f(n_1,\dots,n_k,n+1)=h(n_1,\dots,n_k,n,f(n_1,\dots,n_k,n)) \]
即，\(h\) 的前 \(k\) 位是参数，倒数第二位是递归层数，最后一位是前一轮递归结果。

\(f(m,n)=m+n\) 可以被原始递归描述。

注意到原始递归定义下的 \(f\) 总是对所有自然数输入都是 well-define 的——这样的函数称作 完全函数 (total function)——但我们可以仅对部分输入 well-define，即 部分函数 (partial function)。

由此定义 部分递归函数 (Partial Recursive Functions)，较前者的区别是多了一条

极小化 (minimization) 法则：对于已知的 \(g(m,n_1,\dots,n_k)\)，定义 \(f(n_1,\dots,n_k)=p\)，其中 \(p\) 是满足 \(g(p,n_1,\dots,n_k)=0\) 但 \(g(i,n_1,\dots,n_k)>0\) 对于一切 \(0\leq i<p\) 均成立的 \(p\)。即，寻找首个映到 \(0\) 的 \(g(\cdot,n_1,\dots,n_k)\)。

注意，这样的 \(p\) 不一定存在。这意味着，这样的 \(f\) 不一定是良定义的，因此可谓“部分 (partial)”。

原始递归函数的表达式可以被长度有限的字符串描述，因此构成可数集。那么，原始递归函数是否是全体可计算完全函数呢？并非如此。再次使用对角化技巧：令 \(f_n\) 表示第 \(n\) 个原始递归函数，则考虑函数 \(g_n=f_n(n)+1\)：其显然可计算，但并不归属于原始递归函数集。于是，我们知道原始递归函数并非全体可计算完全函数集合。

递归函数 (Recursive Function) 是 total 的 partial recursive function。

另一种理解是，只允许极小化法则应用于满足存在 \(g(p,n_1,\dots,n_k)=0\) 的 \(p\)，这样的 \(g\)。

存在 recursive 但不是 primitive recursive 的 function，例如 Ackermann 函数

\[A(m,n)=\begin{cases}n+1&(m=0)\\A(m-1,1)&(m>0,n=0)\\A(m-1,A(m,n-1))&(m>0,n>0)\end{cases} \]

区别在于，primitive function 可以由有限步 recursion 达到，但是要想描述 Ackermann 函数，则需要无限步 recursion。

需要注意的是，对角线方法并不能证明存在 total recursive function 的不可数。这是因为，不能 list 全部的 total recursive function：判定一个 partial 是否是 total 的，等效于 Turing 停机问题。

一个集合 \(A\sube\N\) 是递归 (recursive) 的，如果其 特征函数 (characteristic function) \(C_A\) 是 total recursive 的。其中，\(C_A\) 的定义为 \(C_A(x)=[x\in A]\)。是 递归可枚举 (recursive enumerable) 的，如果其特征函数是 partial recursive 的。

一个 \(n\) 元关系 (relation) 是 \(\N^n\) 的一个子集。例如，等于关系即为集合 \((0,0),(1,1),(2,2),\dots\)。因此我们可以称呼一个关系是递归关系，假如其可以使用递归方式判定。

Gödel 标号 (Gödel number) 是自 wf. 或 wf. 序列到自然数的映射。其具体映射方式为，为 wf. 中可能出现的所有字符分配一个奇自然数，然后将 wf. 转成自然数数列；然后就是经典的 \(2^{p_1}\cdot 3^{p_2}\cdot5^{p_3}\cdot\dots\) 的同样被称作 Gödel 标号的技巧。这样做可以简单区分字符的标号和 wf. 的标号：前者为奇数而后者为偶。

不过具体的标号方式其实完全不重要，只要知道存在这么一种单射且易于用 Turing 机求逆的标号即可。

对于一个 wf. \(U\)，令 \(m\) 为其 Gödel number，令 \(n\) 为其证明的 Gödel number（注意到一个 proof 是一个长度有限的 wf. 序列，因此可以被编号），则可以定义关系 \(\t{Pf}(m,n)\) 为：

\(n\) 对应的 wf. 序列是 \(m\) 对应的 wf. 的证明。

自自然数至 wf. 或序列的逆映射，以及验证一个 wf. 序列是否是证明，都是 Turing decidable 的。因此，\(\t{Pf}(m,n)\) 就是可表示的。于是，存在一个 wf. \(P(x_1,x_2)\) 满足 \(\t{Pf}(m,n)\) 当且仅当 \(\vd_NP(0^{(m)},0^{(n)})\)。

这里 \(P\) 的定位，是体系内 (within the system) 对元问题 (metaquestion) 的一次判定。

现在考虑另一个关系：对于一个只有 \(x_1\) 是自由元的 \(A(x_1)\)，令 \(m\) 为 \(A\) 对应的 Gödel number，令 \(n\) 为 \(A(0^{(m)})\) 对应的证明，则判定 \(m,n\) 是否满足上述关系是 Turing decidable 的，于是可以定义 \(W(m,n)\) 表示这个 expressible 的关系，存在对应的 wf. \(W(x_1,x_2)\) 描述之。

“这句话不可证明”这句话是不可证明也不可证伪的。尝试形式化描述之。

考虑从 wf. 实例 \(W(x_1,x_2)\) 出发，定义 \(A(x_1)=(\forall x_2)\lnot W(x_1,x_2)\)。将 \(A(x_1)\) 翻译成自然语言，就是“\(x_1\) 这个命题是不可证明的（是伪命题）”。

现在要想达成“这句话是伪命题”的结果，就可以令 \(p\) 为 \(A(x_1)\) 对应的 Gödel number，然后尝试 \(A(0^{(p)})\)。也即，令 wf. \(U\) 表示 \((\forall x_2)\lnot W(0^{(p)},x_2)\)。若其存在某个证明，则令 \(q\) 为其对应的 Gödel number，此时有关系 \(W(p,q)\) 成立，于是 \(\vd_NW(0^{(p)},0^{(q)})\)。

然而，因为 \(U\) 存在 proof，则 \(U\) 是定理，有 \((\forall x_2)\lnot W(0^{(p)},x_2)\) 成立；既然 \(0^{(q)}\) 也是一种 \(x_2\)，于是 \(\vd_N\lnot W(0^{(p)},0^{(q)})\)，与 consistency 相悖。因此假设不成立，\(U\) 不存在证明。

然而，\(U\) 不存在证明也可能产生一些漏洞。

定义：一个 ω-一致 (ω-consistent) 的系统和单纯的一致性略有不同：其要求不存在以 \(x_1\) 为自由元的 \(A(x_1)\) 满足 \(\lnot(\forall x_1)A(x_1)\) 且全体 \(A(0^{(n)})\) 均为定理。

也即，如果全体 \(A(0^{(n)})\) 均为定理，则 \((\forall x_i)A(x_i)\) 是定理。这看起来有点显然，但是因为你 不能保证 \(N\) 的某种解释中不存在 \(0^{(n)}\) 以外的变量，所以在某些场合，这是不生效的。

定理：ω-一致则一致。

假设其不一致。则全体 \(A(0^{(n)})\) 均为定理。然而由 ω-一致，\(\lnot(\forall x_1)A(x_1)\) 非定理，矛盾。

现在回到我们的 \(U\)。如果 N 是 ω-一致的。因为 \(U\) 不存在证明，所以对于一切 \(q\) 都有 \(W(p,q)\) 不成立，即 \(\lnot W(0^{(p)},0^{(q)})\) 对一切 \(q\) 都成立。由 ω-一致，有 \(\lnot(\forall x_2)\lnot W(0^{(p)},x_2)\) 不能是定理，则 \(U\) 和 \(\lnot U\) 均非定理，产生矛盾。

因此得到结论：

Gödel 第一不完备性定理 (Gödel first incompleteness theorem)：一切 ω-一致的算术系统都是不完备的。

有办法扩张 N 使其完备吗？只要可以递归检查证明，上述对不完备性的证明就是成立的。而检查证明的递归性等价于公理集合的递归性（可以使用 Turing 机生成全体公理）。