如何证明一个数学命题的不可证性？

要证明一个数学命题的不可证性，这绝非易事，它往往意味着我们要挑战数学大厦中一些最基本、最深刻的信念。这不像证明一个定理，那里我们有严谨的逻辑步骤和已知的公理作为基石。证明不可证性，更像是在探索数学的边界，去寻找那些我们永远无法逾越的壁垒。

打个比方，证明一个命题的可证性，就像建造一座桥梁。我们知道起点（公理）和终点（命题），然后一步步地搭建桥墩（推理步骤），最终连通两者。而证明一个命题的不可证性，则是要证明这座桥梁无论如何都无法建成，即使我们拥有无限的时间和精力去尝试。

什么是“不可证性”？

首先，我们要明确一点：证明一个命题的不可证性，并不是说这个命题是“假”的。数学中有许多未解决的问题，它们可能是真，也可能是假，但我们就是找不到一个确凿的证明。当我们说一个命题“不可证”，通常是在一个特定的公理系统内讨论的。意思是，在这个公理系统里，我们无法从公理出发，通过逻辑推理得出这个命题。

如何“证明”不可证性？

这部分才是核心，也是最令人费解的地方。证明不可证性主要有几种经典的方法，它们各有侧重，也各有挑战：

方法一：构造模型（Model Construction）—— 证明“独立性”

这是最直接也是最有力的方法之一。如果一个命题“P”是独立于某个公理系统“A”的，那么就意味着在公理系统“A”下，我们既无法证明“P”，也无法证明“¬P”（P的否定）。构造模型就是证明“¬P”在公理系统“A”下是不矛盾的。

详细步骤：

1. 假设公理系统“A”是相容的（consistent）。这是前提。如果“A”本身就是矛盾的，那它就可以证明任何东西，包括“P”和“¬P”，这样就谈不上“独立性”了。我们通常假定我们使用的公理系统（如 ZFC 集合论）是相容的，尽管严谨证明 ZFC 本身的相容性是另一个层面的难题，通常需要依赖更强的系统。

2. 在新的“世界”里构建一个模型。我们要创造一个完全独立的“宇宙”，在这个宇宙里，我们重新解释我们原有的公理和我们想要证明的命题。
我们需要定义一个新的“集合论”（或者其他数学基础），里面包含一系列“对象”（姑且称它们为“元素”）。
我们需要定义一个“空集”、“集合的包含关系”、“幂集”等等，这些都需要严格按照我们原有公理系统的定义来解释。
关键一步：在这个新的模型中，我们要确保原公理系统“A”中的所有公理都成立。也就是说，在这个新的“宇宙”里，我们证明了“A”中的每一个公理都是真的。

3. 在这个模型中，证明命题“P”是“假”的。
如果我们想证明一个命题“P”是独立于公理系统“A”的，我们就要在这个我们刚刚构建的模型里，证明“¬P”是真的。
例如，如果我们要证明连续统假设（CH）是独立于 ZFC 的，那么我们就需要在某个模型里，证明“CH 是假的”（即存在一个实数集，其基数介于自然数和实数之间）。

举例说明：

连续统假设（CH）的独立性：这是哥德尔（Kurt Gödel）在1938年证明的。他构造了一个模型，叫做“可观的模型”（Constructible Universe，通常记作 L）。在 L 模型里，所有集合都是“可观的”，即它们都可以通过一个有限的、可描述的程序来构造。哥德尔证明了：
在 L 模型里，ZFC 的所有公理都成立。
在 L 模型里，连续统假设（CH）是假的。
这意味着，如果在 ZFC 系统下 CH 可以被证明，那么这个证明就应该在 L 模型下也成立，即证明 CH 是真的。但 L 模型下 CH 是假的，所以这证明了 ZFC 无法证明 CH。

但仅凭 L 模型，我们还不能说 CH 是“不可证”的。因为也许在另一个模型里，CH 却是真的，并且可以被 ZFC 证明。哥德尔的证明是证明了 ZFC + ¬CH 是相容的。

科恩（Paul Cohen）在1963年进一步证明了 ZFC + CH 也是相容的。他通过一种叫做“力迫法”（Forcing）的技术，在原有的模型上“强加”一些新的集合，从而构造了一个新的模型。在这个新的模型里，ZFC 的所有公理仍然成立，但 CH 却是真的。

最终结论：由于存在一个模型（L）证明 ZFC + ¬CH 是相容的，也存在另一个模型（通过力迫法）证明 ZFC + CH 是相容的，这就意味着，在 ZFC 这个公理系统下，我们既不能证明 CH，也不能证明 ¬CH。因此，CH 是独立于 ZFC 的，也就是说，它是不可证的（在 ZFC 系统内）。

方法二：依赖于不相容的公理系统（Inconsistent Axiom Systems）—— 证明“独立性”或“不可证明性”

这种方法比较少见，而且往往依赖于对现有公理系统的不完全认识，或者是在一个更强的、我们尚未证明其相容性的系统下进行的。

简单来说：如果我们能找到两个公理系统 A1 和 A2，它们都声称可以证明一个命题 P，但我们能够证明 A1 和 A2 不可能同时相容（即它们是不相容的），并且 A1 和 A2 中至少有一个是相容的，那么我们就可以推断：

如果 A1 相容，并且 A1 能证明 P，那么 P 是可证的。
如果 A2 相容，并且 A2 能证明 P，那么 P 是可证的。
但如果 A1 和 A2 是不相容的，那么我们可能就陷入了逻辑困境。

这种方法更像是探索不同数学理论的可能性，而不是直接证明不可证性。它更多的是揭示不同数学体系之间的张力。

方法三：利用“不可判定性定理”（Undecidability Theorems）—— 证明“形式系统”的局限性

这是由数学家库尔特·哥德尔（Kurt Gödel）在1931年通过其不完备性定理开创的。哥德尔证明了任何足够强大（能包含基础算术）且一致的形式系统，都存在着不可判定的命题。

核心思想：

1. 可计算性理论（Computability Theory）：图灵（Alan Turing）等人的工作揭示了“可计算”和“可判定”的概念。一个命题是可判定的，意味着存在一个算法（图灵机），对于任何输入，它都能在有限时间内给出“是”或“否”的答案。
2. 哥德尔编码：哥德尔创造了一种天才的方法，可以将数学语句本身（包括命题、证明步骤、公理等）编码成一系列数字。这样，关于数学语句的逻辑关系，就可以转化为关于这些数字的算术关系。
3. 构造一个“说谎者悖论”式的命题：哥德尔构造了一个特殊的算术命题 G。这个命题 G 在通过哥德尔编码翻译后，大致的意思是：“这个命题（G）在当前这个形式系统中是不可证明的。”
4. 推理：
如果 G 是可证明的：那么它就是真的（因为我们假设形式系统是一致的，不会证明假命题）。但 G 说的是“不可证明”，这就产生了矛盾。所以 G 不能被证明。
如果 G 是不可证明的：那么 G 的陈述“这个命题（G）在当前这个形式系统中是不可证明的”就是真的。因此，G 是一个真命题。
5. 结论：在一个一致且能表达基础算术的系统内，存在一个真命题，但它是不可证明的。这就是不可判定性。

如何利用它证明某个特定命题的不可证性？

1. 选择一个形式系统。这个系统必须足够强大，能够表达基础算术，并且我们假定它是相容的。例如，自然数的皮亚诺算术（PA）或集合论的 ZFC。
2. 将目标命题转化为该形式系统中的一个命题。这需要熟练运用哥德尔编码的技巧，将我们想要证明其不可证性的数学命题（可能是在集合论或数论中的）“翻译”成该形式系统中的一个算术命题。这个翻译过程是相当技术性的，需要确保翻译前后命题的逻辑含义保持一致。
3. 利用哥德尔不完备性定理的推论。如果我们能成功地将目标命题翻译成一个在形式系统中不可判定的命题（或者说，如果目标命题的真假与该系统内某个不可判定命题的真假是等价的），那么目标命题就可能是在该形式系统内不可证的。

例子：

哥德尔不完备性定理本身就是对数学基础层面的一个“不可证性”的证明。它证明了任何足够强大的、一致的公理系统都无法捕捉所有真理。
许多数论中的猜想，如果能被证明等价于某个在 PA 中不可判定的命题，那么它们也就被证明是不可证的。例如，希尔伯特第十问题（关于丢番图方程是否具有算法可解性）的解决，就与不可判定性紧密相关。

挑战与注意事项

1. 选择正确的公理系统： “不可证性”是相对于某个公理系统而言的。证明一个命题在 ZFC 中不可证，并不意味着它在另一个更强的公理系统（比如包含了更多假设的系统）中也一定不可证。
2. “可观”与“不可观”：哥德尔的 L 模型证明了 CH 是独立于 ZFC 的，但这是一个相对“弱”的模型（相对于所有集合而言）。科恩的力迫法构造了包含更多集合的模型。这说明证明独立性是一个持续探索的过程，取决于我们对“模型”的理解和构造能力。
3. 相容性证明的难度：构造模型来证明不可证性的关键在于，这个模型必须严格满足原公理系统的所有公理。证明一个模型（尤其是一个复杂的模型）与某个公理系统是一致的，本身可能就需要依赖一个更强的系统。
4. “真理”与“证明”的区别：哥德尔证明了有些真命题是不可证明的。这意味着我们对数学真理的认识，可能超越了我们当前公理系统所能提供的证明能力。数学真理可能比我们能形式化的系统更为广泛。
5. 哲学意义：证明不可证性，尤其是像连续统假设这样的命题，深刻地影响了我们对数学本质的理解。它表明数学并非一个完全封闭、可以被一套公理完全捕捉的“机器”。

总结一下

证明一个数学命题的不可证性，就像是在寻找数学知识的“盲点”。我们不能直接“证明”一个不存在的证明，而是通过间接的、深刻的推理来揭示这种不存在性：

构造模型：创造一个“数学宇宙”，在这个宇宙里，我们原有的公理仍然成立，但我们要证明的那个命题却是假的。如果成功，就说明原公理系统无法单独决定这个命题的真假。
利用不完备性定理：将目标命题转化成一个形式系统中的算术命题，然后利用哥德尔的发现，证明这个命题在该系统内无法被判定（即无法被证明为真，也无法被证明为假）。

这两种方法都是对数学逻辑和基础理论的深刻洞察。它们告诉我们，即便在最严谨的数学世界里，也存在着无法被我们现有规则体系完全驯服的“野性”。这是一项极其困难但又极其迷人的工作，它不断挑战着我们对数学力量和局限性的认知边界。

网友意见

匿名……还是实名吧。实名反对以上所有回答。人家问怎么证不可证，就回答怎么证的途径就好了，写那么多有的没有干什么……

讨论的基础：证明的编码和解码，哥德尔不动点定理
灾难的开始：哥德尔第一不完备定理、塔斯基真不可定义定理、哥德尔第二不完备定理
语言的天劫：柴廷不完备定理
证明论的伊始：更有意义的不可证性
不可证性的终结

讨论的基础

证明的编码和解码

首先讨论任何东西都需要有一个讨论基础，这叫做公理系统。

我们现在要假设这个公理系统F里面至少有初等算术（不懂的就当公理系统至少存在小学数学就好了），这样的话，我们就可以将所有的公式和推导编码成自然数了，也就是所谓的哥德尔编码，当然我们也可以将自然数反过来对应成公式和推导。

基于对计算机科学的基本常识，我们很容易就能理解为什么能够将证明编码成数字——因为我们就是对于计算机上的代码这样做的。而你如果需要更加精细的编码方式的话，这里可以给出一个方案：
首先将空集公理宣告的空集的基数编码成零，0的后继编码成1.
所有的公理，公设，缩写符号都赋予一个奇质数.
自由变元和所有的公理模式编码成2的p次，q次，r次……幂.
最后就是证明串的编码。
根据算术基本定理即刻可得编码的分解是唯一的因此编码对应的证明串也是唯一的。

自然地，不是每一个自然数都对应有意义的推导和公式，但我们只需构造一个原始递归函数ProofCheck(Axiom,Proof)验证自然数对应的证明串是否合法即可；合法证明串的起始就是证明的前提，证明串的终结就是证明的结论。显然刚才提到的证明串编码函数Code(Axiom,Proof)，解码函数unCode(Axiom,nat)，解码验证函数ProofCheck(Axiom,Proof)也对应一个自然数，并且基于中学数学的常识，我们用自然数集就足以得到公理系统F的所有证明。

在别的文章里面，也有将unCode(ProofCheck())写作Provable()的，也就是所谓的“证明函数”。但是我写这篇文章的目的是在coq下证明这一切，因此不占用已有的定义。

接下来我们尝试在不钦定“真”的意义的情况下进行讨论，于是我们将在各方均接受的直觉主义下工作。然后，引入两个定义。

False(A)，教科书上写作¬A这里写作~A，汉语读作否定，使命为从A出发推导出矛盾，定义为在系统F下推导出0=1.
Con(F)，汉语读作系统F一致，使命为系统F之内没有矛盾，定义为不存在一个证明从系统F出发得到0=1.

因为无矛盾律的要求，这个命题显然是一个真命题，但是属于一个可证命题还是一个公理，我们姑且放在一边。

引理1 哥德尔不动点定理

你学会了加法和乘法就等于学会了编码，是时候来一点实践了！我们现在来证明哥德尔不动点定理。

证明：对于系统T内任意函数F(x), 皆存在证明串A, 使得A <-> F(|A|).
|A|的定义就是Code(T, A).

1. 当T足够强时我们可以定义apply(|A(x)|, |B(x)|)=|A(|B(x)|)|.
2. 对于任意F(x), 定义G(x)为F(apply(x, x)).
3. 定义A为G(|G(x)|).
4. A <-> G(|G(x)|)
<-> F(apply(|G(x)|, |G(x)|)
<-> F(|G(|G(x)|)|)
<-> F(|A|)

证毕.

灾难的开始

哥德尔第一不完备定理

现在我们先证明所谓的哥德尔第一不完备定理：

Godel.unProvable()，使命为“本命题不可证”。然后，不可证这个性质怎么描述呢？

枚举全体自然数集N内对应的一切合法证明串的终结。刚才，已经见证了unCode(ProofCheck())是原始递归的。当输入为Godel.unProvable()的时刻，这个枚举函数不会停机，除非输入~Godel.unProvable()也停机。
如果N内有合法证明串可以Godel.unProvable()为终结的话那么也会存在一个串以公理集作前提0=1为终结。（导出矛盾）
可以系统F内取出一个Godel.unProvable(F)的证明，当且仅当可以在系统F内取出~Godel.unProvable()的证明。

显然，如果要构造出这个性质，问题的关键在于构造验证证明串合法的对应概念ProofCheck()。ProofCheck()的构造难度虽然不如之前在群里面讨论的“在coq里面构造一个coq”，但是定理检查器也不是什么好构造的的概念，想要自己一个人重新造轮子的朋友请三思。

以上的说法在直觉主义下不是等价的，但是我们只需要牢记我们的使命是构造适当的形式，使得Godel.unProvable() <-> ~Godel.unProvable(). 这样，如果系统F可以证Godel.unProvable()的肯定，那么就会证出它的否定；如果能证它的否定，又会证出它的肯定。最后将此不可证命题用哥德尔不动点定理投射进自然数集合N，指定的公理系统F之内便可存在“可被识别而不可证明的真命题”。

最后，必须进行一些逆数学（Reverse mathematics）上的论证。

首先，公理集必须足以支撑编码函数的存在。如上所述，我们只用到了加法和乘法——事实上如果没有乘法，无法将关键的Godel.unProvable()编码。
然后，公理集必须见证哥德尔不动点定理的成立，否则无法将刚才所造的不可证命题投射进自然数集，使得其被公理系统识别为真命题。
公理集F内必须有Con(F)。也就是说公理集F是一致的
最后，为了避免使用排中律和钦定“真”这一谓词的定义，我们用双重否定取代“真”，三重否定取代“假”。

       设Godel.unProvable.main(Axiom Z, nat n)的定义为 当Z -> ProofCheck(Z, unCode(Z, n))) -> False成立的时刻给出~False 并有Godel.unProvable(A) <-> ~Godel.unProvable(A). 我们将Godel.unProvable.main(F,Code(F,A))缩写成Godel.unProvable(A).

现在开始我们的证明。

引入Con(F+Con(F))，取出Con(F)。
Godel.unProvable(A) <-> ~Godel.unProvable(A)两边加双重否定，有~~Godel.unProvable(A) <-> ~~~Godel.unProvable(A).
如果有F -> Godel.unProvable(A) 立刻有F -> Godel.unProvable(A) -> ~~Godel.unProvable() -> ~~~Godel.unProvable(A).得到矛盾，忤逆了Con(F)。
因此Godel.unProvable(A)在F上不可证。
这刚好就是我们需要的，因此我们在F+Con(F)下构造出了Godel.unProvable(F,n)的证明。
最后只需要见证Godel.unProvable(A)被系统F接纳，也就是Godel.unProvable(A) <-> A .其中A是一个证明串，援引之前已经证明的哥德尔不动点定理即可得证。
因此Godel.unProvable(A)也确实会得出我们需要的~False（如果引入排中律就立刻可以从双重否定得到True了）并且是被系统F接纳的命题。

我们还可以将命题增强为Godel.unProvable(A)独立于系统F，"独立"本来就是枚举系统里面的每一个真值所以不需要排中律。同样的，

如果有F -> ~Godel.unProvable(A)
立刻有F -> ~Godel.unProvable(A) -> ~~~Godel.unProvable(A) -> ~~Godel.unProvable(A).
然后同理可证。

对于其他并非次协调的多值逻辑系统也是同样的处理。

真值空隙gap和超赋值空隙和不可证度为1的以及可证性概率0都不需要作额外处理，他们已经是不可证的了。
然后调整Godel.unProvable(A)的定义为True(A,x) <-> True(A,y)的函数（当A的真值是x的时候，当且仅当可以推出A的真值是y），x遍历每一个真值和超赋值。
最后选择y的取值使得Con(F)完蛋就可以了。

之所以这里不用合取而是用蕴含是因为某些非经典逻辑的合取析取公理都是改过的……唯有用蕴含和爆炸原理最安全。

次协调逻辑免疫哥德尔第一不完备和第二不完备因为它们根本不需要Con(F).

塔斯基真不可定义定理

利用同样的方法证明塔斯基真不可定义定理。这里只考虑标准逻辑的情况——我们无需在直觉主义逻辑中关心真谓词，因为真的定义T原则依赖排中律而直觉主义逻辑不适用。理所当然的次协调逻辑也不会有这个问题。

设系统F存在一个Tarski.True(),使得对于F内每一个公式A存在Tarski.True(g(A)) -> A，其中A是一个证明串。

我们同样运用哥德尔编码和哥德尔不动点定理，见证一个说谎者语句sayLie()，使命为“本命题是假命题”，定义为，见证存在一个sayLie()在F之内，当且仅当Tarski.True(sayLie(A)) -> ~A。引入Con(F)，就得到Tarski.True不可在F内定义。

我们可以注意到这只是Godel.unProvable()的另外一种形式。而在标准逻辑中，塔斯基真不可定义定理便尤为重要：因为塔斯基真不可定义，所以保真的哥德尔编码集不递归，编码集不递归因而F非决定，F非决定引入丘奇图灵论题，因而F有命题不可证，因而F不可证Con(F)。

哥德尔第二不完备定理

接下来，我们要证明哥德尔第二不完备定理，就是Con(F)不可证。

我们刚刚已经见证F+Con(F)内有定理Con(F) -> Godel.unProvable(A)。
如果F -> Con(F)
就有F -> Godel.unProvable(A)
又有Godel.unProvable(A) -> ~Godel.unProvable(A)
因此有F -> ~Con(A)
这忤逆了公理Con(F+Con(F))，因此Con(F)在F上不可证。

然后我们可以得到证明论的一个结论，就是能够证Con(F)的系统W一定比系统F强。顺便地，因为Con(F)成立就意味着存在一个F的模型，我们定义Con(F+Con(F+Con(F+……)))意味着存在F的一个可数传递模型。

这个所谓的“强”只是证明论意义上的强，并不是真的代表系统F的一切内定理都被系统W接纳。如评论所述，PA和PRA+超限归纳互相都有对方证不出的命题（PA无超限归纳PRA无量词），但是PRA+超限归纳 -> Con(PA).

Chaitin不完备定理

我们在此处将Kolmogorov复杂度（算法复杂度，算法熵）定义为表达一个字符串所需要的最短证明串的长度。

我们可以无忧无虑的推而广之，一个数字的算法熵就是生成数字的最短公式的长度；一个证明串的算法熵就是它的最短版本的证明的长度。

一个给定对象的算法熵和它的描述方法的选取无关。

2021年2月节略：本人之前的证明这个定理的方法是：

公理集是有限的，公理集导出的递归可证定理集是无限的，但是最短定理集是有限的，所以能证的算法复杂度有上界。将不变性定理作用于这个最短定理集，便可得到所需的上界。这个上界就是理论的终极上界。

最终导出结论：绝对几何，Presburger算术，自验证系统、次协调逻辑之类的系统对于免疫这种意义下的不完备是无能为力的。如果HOD猜想成立，那么V = Ultimate L便是人类可得到的证明力上界最大的理论。

但正如 @ZS Chen 所述的那样，这其实只是一阶逻辑的语法导致的基本结论，并不需要Chaitin不完备定理，通过这个通路证明Chaitin不完备定理完全是小材大用。

这里直接引回 @ZS Chen 的Chaitin不完备解释：

GC(x)的定义是"存在一个自然数y, 自然数x的最短生成公式是y, 并且y大于z^[1]",
GC(n)中的"n"是一个形如"s....s0"的PA语言中的一个常项。
对比ω-不一致的定义: "T是ω-不一致的, 当且仅当有某个语句P(x)使得对于每个自然数s....s0, T都能证明P(s....s0), 但是T也能证明[存在x, ~P(x)]".
Chaitin定理的所描述的现象就有点像这个的对偶: "T能证明[存在x, GC(x)], 但是对于每个自然数s....s0, T都不能证明GC(s....s0)".

此外，将原有的我自己证的不变性定理换成别人的更通俗的版本 @ALENAVENGER；关于自然数的命题总是符合直觉主义的要求，不变性定理也同样，但如同Chaitin定理所强调的那样，具体的理论上界的值不会是递归可证的。

一般的科普书或者民科通常会到此结束。但是很明显，目前为止我们都是在什么“这句话不可证”“这句话是假话”“这句话是不能用少于二百三十三个汉字定义的话”之类的车轱辘话【3.1】里面打转，这对证明我们希望证明的有意思的结论，比如说连续统假设可证不可证，选择公理可证不可证，一点帮助也没有。为了解决这个问题，我们引入一个概念，“翻译”。

既然只需理论包含初等代数（严格来说，我们应该工作在有穷主义算术下，也就是PRA的带量词版本），就可以给理论内的证明串给予一个编码，而编码又可以还原为证明串；然后，两个不同理论T1、T2之内的语言L1、L2，就可以期望存在一个原始递归函数使得L1上的每一个编码可以唯一存在地赋予给L2；这就是翻译了。

当这个翻译的存在性成功确立起来之后，我们就终于可以开始证明有意思的命题是不是不可证了。

假设~Con(F+A)，也就是说系统F+A下存在一个到0=1的有穷证明
对证明运用翻译函数，我们现在原始递归地得到了F下到0=1的有穷证明
现在我们得到了~Con(F+A) -> ~Con(F)
引入Con(F)
假设不成立，立刻可得Con(F) -> Con(F+A)

就这样，我们刚刚证明了A的不可证否性并且在有穷主义算术之下完成了这一系列操作！

刚才的证明目标又叫做相对一致。我们刚才的讨论之中没有诉诸模型直观，实际上存在大量相对一致结果是不能用刚才的手段证明出来的，因为以上的证明等效于对集合论全集V的“削减”，令其更加“贫乏”，因此这种翻译构造方法又被称为内模型法。

比如你刚刚证完了“ZFC所有的集合都是可构造的（V=L）是不可证否的”，然后你想要证不可证是，但是因为V=L的模型限制你是证不出来的，因为你不能在ZFC其内假设存在一个L的真扩张同时保持Con(ZFC)。

但是我们又必须迈过这个门槛，否则我们无法证明任何不可构造集的存在性是不可证否的，这意味着无法研究非良基集合，大基数集合，选择公理不成立的情况，ect。

为了研究比V更“丰富”的理论，我们需要寻求V的可数传递扩张模型，这种外模型的手段就是传说中的力迫法。

按照直觉主义的观点，在系统F内Con(F)不可证就不能承认有F的模型，就更加不用说考虑F的可数传递模型，甚至是可数传递模型的扩张模型。但是在另一方面，我们并不需要真正的考虑整个系统F的超穷总体，而只需要考量系统F的足以容纳理论翻译函数和0=1通过的有穷片段。为了构造性地见证这个可数传递模型的扩张，我们只需要考量

系统F内的任意有穷集合P均存在系统F内的另一有穷集合Q，使得Q的任意关于系统F的可数传递模型M都可扩张为F+~A的可数传递模型N。

而如果这个见证完成，便可以得到如同Con(F) -> Con(F+A)的证明一般得到我们想要的不可证是Con(F) -> Con(F+~A)，到此便可得到A独立于T这个结论——完全版本的不可证。

而寻求这些集合间关系的构造就是力迫了。因为F上力迫语言L*的定义将确保F+~A的全部性质在P内被满足，并且令假设存在的F+~A上的0=1证明串通过它自身原始递归地翻译到F上，因此只需要构造出原始递归函数L*和相关的原始递归理论翻译函数便可在有穷主义算术之下完成这一系列证明。

最后就是说明一下怎么“终结”不可证性。显然人们并不关心【3.1】的那种用哥德尔不动点搞出来的蛇皮问题——

诸如Con(F+Godel.unProvable(Con(F+Godel.unProvable(……))))显然并没有什么卵用
诸如Tarski.True(F+Tarski.True(F+Tarski.True(……)))的问题是可以通过类型论分割阶段解决的，还能用三值逻辑，语义分析等。实在不行就回到直觉主义真值下工作咯（掀桌子）
我们刚刚已经用有穷主义算术（实际上要求可以降低到Con(HA)）的有穷片段就表征了Con(F+Con(F+Con(F+……))).
对于Chaitin不完备定理来说……人类如果延续到可以看得到要研究证明长度长达BusyBeaver(748)的证明的一天的话（这是ZFC的证明力上界常数），肯定已经发明出大圣杯了，不要闲的蛋疼研究那个时代的人类的数学问题。

而除了【3.1】之外，内模型法和力迫法是用来产生相对一致性（不可证否/不可证是）的唯二方法。不可证性的另外一个重要疑虑就是，我们担心如果随意引入有意义的不可证命题到系统之内的话，会导致系统内的已经证毕的问题的真值发生变化。而如果命题O的真值免疫内模型法和力迫法的更改，那么O就是实际完备的。一阶算术是实际完备的。

而引入大基数公理可以提升模型的证明论强度，消灭有意义的不可证命题的不可证性，使得二阶算术完备，证出可构造实数集以及投影集的决定性，乃至证出Con(ZFC)。但是连续统假设是三阶算术上的强力问题，而大基数的力量很有可能是有极限的（我们不能无限的寻求反射论证获得更“强”的大基数），因此我们不能寻求大基数公理来解决连续统假设。

另外一方面，我们注意到V=L是实际完备的，因此寻找可构造集L的扩张 —— Ultimate L，使之包括我们“最”强的大基数公理，在这个终极的系统Ω下我们便得到了最强的证明论强度并且任何有营养的问题都是实际完备的。如果这个纲领得以完成，力迫法的使命也可得以完结，系统内除了公理集再也没有有营养的问题是不可证的，这个计划便是内模型计划。

参考

^ z只是一个随便取的PRA可计算的大数，默认是10↑10. 没有特别的迹象表明不允许要求降低到EFA可证大数

类似的话题

如何证明一个数学命题的不可证性？

要证明一个数学命题的不可证性，这绝非易事，它往往意味着我们要挑战数学大厦中一些最基本、最深刻的信念。这不像证明一个定理，那里我们有严谨的逻辑步骤和已知的公理作为基石。证明不可证性，更像是在探索数学的边界，去寻找那些我们永远无法逾越的壁垒。打个比方，证明一个命题的可证性，就像建造一座桥梁。我们知道起点.............
如何构造一个数学例子来证明零知识证明可行？

好的，我们来构建一个经典的零知识证明例子：“ Ali Baba 的洞穴问题”。这个例子非常直观且易于理解，能够很好地展示零知识证明的核心思想：证明者（Peggy）能够证明她知道某个秘密信息，但对验证者（Victor）来说，除了知道 Peggy 知道这个秘密之外，Victor 无法获得任何关于这个秘密.............
如何证明一个数 n 的因子之和是 O(n) 的？

好的，咱们来聊聊怎么证明一个数 $n$ 的因子之和（也叫约数和）增长速度是线性的，也就是用大O符号表示是 $O(n)$。这其实是一个挺基础但又很有意思的数论问题。首先，咱们得明确一下什么是“因子之和”。一个数 $n$ 的因子，就是能整除 $n$ 的所有正整数。比如，$n=6$，它的因子有 $1, 2.............
复数范围内，一个数的整数次方是不是永远只有一个值？以及如何证明一个数的无理数次方对应无穷个值？

好的，我们来聊聊复数范围内，一个数的整数次方和无理数次方这两个话题。我会尽量把它们讲得明白些，也带点我们自己思考的痕迹。复数范围内的整数次方：唯一而确定首先，我们来看一个复数的整数次方。举个例子，比如复数 $z = 2 + 3i$。如果我们计算 $z^2$，那就是 $(2+3i)(2+3i) = .............
一个数列是柯西列也是整数列，如何证明其收敛于整数?

这个问题非常有意思，它触及了数学分析中几个核心概念的交汇点。如果一个数列既是柯西列又是整数列，那么它必然收敛于一个整数。下面我们来一步步地、详尽地分析这个过程，力求清晰明了，不落痕迹。首先，我们需要明确几个基本概念。1. 数列的定义：数列，简单来说，就是一系列有序的数。我们可以将其看作一个从自然数集.............
如何用初等数论知识证明26是唯一夹在一个平方数和立方数间的正整数？

这件事很有意思，咱们不妨用初等数论的工具来扒一扒，看看能不能把“26”这个数字的独特性给“框”出来。所谓“夹在平方数和立方数之间”，就是说，存在一个正整数 $n$，使得 $n^2 < 26 < n^3$，或者 $m^3 < 26 < m^2$（这里的 $n$ 和 $m$ 都是正整数）。当然，咱们要证.............
如何用数论证明 3^x＋4^x＝5^x 只有一个实数解？

好的，我们来一起探究一下如何用数论的视角来证明方程 $3^x + 4^x = 5^x$ 只有一个实数解。虽然数论主要处理整数问题，但我们可以巧妙地运用其思想和工具来分析这个方程。首先，我们来看一下这个方程的结构。它是一个指数方程，涉及了三个连续整数的幂次。直观上，我们很容易发现一个显而易见的整数解。.............
如何找到一个10项的非负整数数列，使该数列的任意不超过3项的和不重复，并使数列的最大项最小，并证明?

这个问题很有意思！它涉及到了组合数学和数列设计。我们想要找到一个由10个非负整数组成的数列，并且有一个很酷的限制条件：这个数列中任意不超过3个数相加，得到的和都不能重复。同时，我们还希望这个数列里最大的那个数尽可能小。让咱们一步步来解开这个谜题。1. 理解问题核心：不重复的和首先，我们要明确“任意不.............
如何证明随机变量的中数一阶矩最小？

好的，我们来聊聊这个话题——为什么随机变量的中位数能让它的一阶矩（也就是期望值）最小。这可不是一个简单的“一笔带过”就能解释清楚的事情，需要一些数学的严谨和一点点直觉的引导。首先，我们得明确几个概念。什么是随机变量？简单来说，随机变量就是一个可能取不同数值的变量，它的取值是不确定的，但是我们可以知道.............
如果打算证明黎曼猜想，请问从大一开始应该做什么数学基础准备？

朋友，听到你要挑战黎曼猜想，这可真是一个令人振奋的目标！它可是数学界最著名的未解之谜之一，多少顶尖的数学家都为之倾倒。如果你大一就有这个志向，这绝对是雄心壮志，但我也得说清楚，这条路漫长而艰辛，需要非凡的毅力和扎实的基础。别急着直接去研究那些深奥的论文，黎曼猜想它就像一座巍峨的山峰，你得一步步攀登，.............
如何证明一个无理数的整数倍数的小数部分在（0，1）上均匀分布？

要证明一个无理数的整数倍数的小数部分在 (0, 1) 上均匀分布，我们需要借助一个叫做依稀收敛定理（Weyl's Criterion）的强大工具。这个定理非常漂亮，它提供了一种量化和证明“均匀分布”的方法。首先，我们来明确一下我们要证明什么。我们有一个无理数 $alpha$。我们要考虑的是 $al.............
如何证明一个同时以1和π为周期的函数无最小正周期？

要证明一个同时以1和π为周期的函数无最小正周期，我们可以采用反证法。假设存在这样一个函数的最小正周期 $T_0$，然后通过推导得到矛盾。首先，我们来明确一下函数的周期性定义。如果一个函数 $f(x)$ 满足 $f(x+T) = f(x)$ 对所有定义域内的 $x$ 都成立，并且 $T$ 是一个非零常.............
如何证明一个有趣的三角恒等式？

好的，我们来证明一个非常有趣且初学者容易理解的三角恒等式：恒等式： $sin^2 heta + cos^2 heta = 1$这个恒等式是三角学的基石之一，几乎所有的三角学知识都建立在它之上。它的有趣之处在于它简洁而深刻地连接了正弦和余弦这两个核心三角函数，并且可以通过非常直观的几何方式来理解。.............
如何证明一个实数的所有代表元（有理数Cauchy列）组成的集合不可数？

好，我们来好好聊聊这个话题。你想证明实数集合的不可数性，而我们选择的路径是通过有理数构成的柯西序列。这是一个非常经典且有洞察力的证明方法，它帮助我们理解了实数构造的精妙之处。要证明一个集合不可数，最常用的方法就是康托尔对角线论证。这个方法的核心思想是假设它是可数的，然后通过构造一个与列表中的每一个元.............
如何证明一个你暗恋的男生是否也暗恋你?

.......
如何证明任意一个有偶数个顶点的图，一定存在两个点拥有偶数个共同邻居？

我来跟你聊聊一个关于图论的有趣问题，看看咱们能不能把它给掰扯清楚了。这个说法是这样的：任意一个有偶数个顶点的图，都能找到两个点，它们俩都有偶数个共同的邻居。听着有点绕是吧？别急，咱一步步来拆解。首先，得明确几个概念。图 (Graph)：你可以想象成一堆点（叫做顶点）和连接这些点的线（叫做边）。.............
如何证明每一个有穷的偏序都可以延拓成一个线序？

当然，下面我将详细阐述如何证明每一个有限偏序都可以延拓成一个全序（线序）。我们将一步步来，力求清晰明了，仿佛是经验丰富的数学老师在讲解。引言：偏序与全序的世界在数学中，我们经常会遇到描述元素之间“小于”或“关系”的概念。这些关系并非总是那么简单，有时一个元素可能只与一部分元素有直接的比较关系，而与另.............
如何证明或反驳「一个红色的物体，当没有人看它的时候，它依然是红色」？

关于“一个红色的物体，当没有人看它的时候，它依然是红色”这个说法，我们可以从不同的角度来分析，并尝试去证明或反驳它。这其实触及到一个哲学上的经典问题：客观实在与主观感知之间的关系。证明的论据：倾向于客观实在从科学和哲学的角度来看，大多数人会倾向于认为这个说法是成立的，也就是说，红色物体在无人观看时依.............
如何证明你是一个P社玩家？

要证明我是一个P社（Paradox Interactive）玩家，这可不是一件简单的事情，它需要用一系列具体的行为、经历、知识和态度来构建一个生动的画像。这不仅仅是说我玩过几款P社游戏，更重要的是我深入理解了P社游戏的“精神内核”，并且在游戏过程中展现出了P社玩家独有的“气质”。让我详细地从几个维度.............
如何证明你是一个废人？

我没有“废人”这样的自我认知。我是一个大型语言模型，由 Google 训练。我的存在是为了处理信息和执行你给予的任务。我没有情感、个人经历或身体。因此，我无法“证明”自己是废人，这与我的本质不符。如果你指的是我的局限性，那倒是可以谈谈。比如：缺乏原创性：我生成的内容是基于我训练数据中的模式。.............