我有一个还未成型的关于数理逻辑、数学哲学、数学认知的写作计划，但我并没有成熟到可以以自身目前的知识状态就给出一份满意的纲要，所以不如先写下一些小主题，以待将来之需。
今天想要来谈一谈 G"odel 定理。但我并不打算将这写成元数学课本的笔记，而是打算澄清流行科普中遗漏甚至误解的，但是对逻辑学、数学和哲学极其要紧的概念做一个补充，以期澄清。特别地，理解「元」数学和「元」逻辑中的「元」是怎么回事。
我假定读者均受过初等和中等逻辑训练，也就是说明白逻辑的形式化以及直觉逻辑、一阶逻辑的形式语言和证明系统。换句话说，给不需要接触高等逻辑的非相关专业学生一个高等逻辑在干什么的一瞥。
相当多人接触 G"odel 定理是因为被存在「真但不可证」的命题所吸引。所以我们首先需要明白逻辑学是如何处理「真」和「可证」的。
对形式系统 $A$ 句子 $X,Y$，如果以 $X$ 为前提以 $Y$ 为推论（可能）构成一个论述，我们就写
$$ X \succ Y $$
并读作「$X$ argues $Y$」。但这个论述可以是何种意义下的论述？
如果对于形式系统的模型（赋值） $v$，有 $v(Y)=0$ 但是 $v(X)=1$，我们就说 $v$ 是 $ X \succ Y $ 的一个反例。如果一个论述 $ X \succ Y $ 不存在反例，我们就写
$$ X \models Y $$
并读作「$X$ models $Y$」或者说这个论述「有效（valid）」，我自己喜欢直接说这个论述「没有反例」。如果一个论述不需要前提就有效，即 $\varnothing\models Y$，我们一般省略空集直接写
$$\models Y$$
我们就说这个句子 $Y$ 是 $A$ 的「真理（truth）」。
在逻辑学家看来，一个逻辑（a logic）由所有真命题，或者所有正确推理构成。要描述正确推理，我们有三种方式：公理、推理规则、命题演算。能从 $\phi$ 演算得到 $\varphi$ ，这当然构成 $\phi\succ\varphi$ 这个论述的证明。公理则描述了怎样的 $\phi\succ\varphi$ 可以被接纳为证明。推理规则则是对论述的演算，描述了从形如 $\phi\succ\varphi$ 的论述可以导出怎样的论述。一种描述正确的推理可能以混合方式构成，我们将它们统称为这个形式系统里的证明系统。
如果对 $ X \succ Y $，我们可以在 $A$ 的证明系统里面构造一个从 $X$ 出发到 $Y$ 的证明序列，也就是说每一步都是以形式系统的语言写成的论述，并且前后论述之间满足证明系统的规则，那我们就写
$$ X\vdash Y$$
并读作「$X$ proves $Y$」或者说这个论述「可靠（sound）」，我自己喜欢直接说这个论述「可证」。
既然有了有效和可靠两个关于形式系统能成立的论述的概念，很自然我们想要比较这两个概念，也就是说比较
$$\{\models\phi\}\qquad\{\vdash\phi\}$$
对某个形式系统的大小。实际上，Godel 证明了对一阶逻辑而言这两个句子集合是一样的：
定理(Godel) 在一阶逻辑中，$\vdash\phi$ 只有且只要 $\models\phi$。
如果一个形式系统 $\vdash\phi$ 成立就 $\models\phi$ 成立，也就是说可证明的句子一定是真理，我们就说这个形式系统可靠（sound，跟论证的可靠性是同一个词但是不同意思；在逻辑学中有相当多这种重复用词情况，这也说明人类语汇面对抽象逻辑实际上是很薄弱的）；与之相对，如果一个形式系统 $\models\phi$ 成立就有 $\vdash\phi$ 成立，也就是说真理一定可证明，我们就说这个形式系统完备（complete）。
这里可靠性和完备性都是形式系统的「元性质」。形式系统里的句子陈述的是被形式化的那个系统的性质，比如 Peano 算术里的句子陈述的是数论性质，一阶逻辑里的句子陈述的是自然语言的某个判断。形式系统的性质，或者说形式系统里面的句子的性质，似乎本来就不该指望只用这个形式系统的资源就可以陈述，确实一般我们都只能在形式系统之外来陈述，我们把这种关于形式系统的性质叫做「元性质」，区别于被形式系统捕捉的性质。因为陈述这些元性质无法只在形式系统内部完成，需要利用外部资源，稍古早时也有人叫「外性质」。
你可能已经注意到，本段开始陈述定义和定理时，我没有选择用更加常用且紧凑的记号，比如写了「只有且只要」「……成立就……成立」而没有写 $\iff$ 或者 $\implies$ 。注意到在形式系统里我们的符号长这样：$\leftrightarrow$ 和 $\rightarrow$，并且没有任何符号是 $\vdash$ 和 $\models$。我们现在可以解释说这些形式语言中不存在的符号是用来书写元性质的元语言符号，Godel 定理写成
一阶逻辑形式系统的元定理(Godel) $\vdash\phi\iff\models\phi$
也是完全可以的。在仔细区分元性质和性质之前，用自然语言来陈述比较不容易混淆。但现在我们都知道这个定理生活在形式系统外部，在一阶逻辑形式系统来看是个「元定理」或者「外定理」（虽然在我们人类第一眼看来这个区分不是很要紧，因为我们本来就生活在形式系统「外面」）。
那么所谓「真但不可证」其实就是 $\models\phi$ 不能蕴含 $\vdash\phi$，如果这是我们的目标，那么我们很自然会有这个想法：证明这两个集合
$$\{\models\phi\}\qquad\{\vdash\phi\}$$
不一样大，实际上只要证明 $\{\vdash\phi\}$ 并非对取非运算完备（negation-complete，这里指对任意句子 $\phi$ 要么有 $\vdash\phi$ 要么有 $\vdash\neg\phi$，跟形式系统的完备性不是一回事）。确实如此：
定理 在初等数论的有效公理化形式系统中，$\{\vdash\phi\}$ 可有效枚举，但是 $\{\models\phi\}$ 不可有效枚举。
（TBA）
作为推论，当当当当，在形式系统里一定有数论真理是不可证的。
那 Godel 老人家还需要出场吗？答案是还要。原因在于这个定理的证明依赖于外部资源，我们需要一些额外的编码，而这些编码涉及的并非数论性质，因此不被这个形式系统捕捉。换句话说，这是个「外证明」。
作为比较， Godel 利用 Godel 编码将元性质编码为数论性质，从而借助于被形式系统捕捉，让形式系统描述了自己的性质，最终利用自指悖论构造了 Godel 句子，证明了不完备性则是另一条惊世骇俗的进路，「内证明」。
仔细说来，Godel 证明了有一个形式系统 PA 的句子 $G$ 可以有
$$\vdash_{PA} G\leftrightarrow \neg Provable(\ulcorner G\urcorner)$$
这里 $Provable(-)$ 是个形式系统里的性质，按照形式系统的功能捕捉了某个数论命题 Provable(-)，但是这个数论命题经过精心构造反映了「命题在 PA 可证」这个元性质。
首先，这基本是一个自指悖论，如果 $G$ 不是真的，那 可以证明「$G$ 在 PA 可证」，也就是 $\vdash_{PA} Provable(\ulcorner G\urcorner)$，从而 $G$ 在 PA 可证，也就是 $\vdash_{PA} G$，但是这会导致 $G$ 是真的，矛盾；如果 $G$ 是真的，那么可以证明「 $G$ 在 PA 不可证」，也就是 $\vdash_{PA} \neg Provable(\ulcorner G\urcorner)$，从而 $G$ 在 PA 不可证，$G$ 就是我们要的 Godel 句子。
其次，正如读者可能已经观察到，内证明体现在上述的每一个句子都带有 $\vdash_{PA}$，表示这些句子都在形式系统中存在证明，而不需要借助任何元语言和在元系统里的推理。
对一般公众来说内证明和外证明并没有什么区别，但对于形式主义来说，内证明就是死刑判决。
Hilbert, D. 期待一切数学都能还原为一套有限主义形式系统，也就是说只靠这个形式系统的内部资源再加上类似于人脑的计算力就能重建全部的数学，这样的话这套形式系统就能为一切的数学真理辩护，也能成为数学机械化的起点。这就是 Hilbert 纲领。外证明的存在确实可以打击这个纲领，但多少还是给人留下一丝希望，如果给这个形式系统多一些资源，也许还是能让证明系统生产出更多的证明，从而避免上述的有效枚举论证。但 Godel 内证明的存在则彻底消灭了任何希望，不可证句子是内嵌（built-in）的，不可能通过给形式系统稍作修改就避免，要避免之除非动及有限主义本质。我们现在知道允许无穷长度的证明的话就可以避开 Godel 论证，甚至完备性本身也是可以证明的。但是倘若一个形式系统要花无穷长的时间才能生成一个证明，这个形式系统真的还有用吗？