哥德尔的speed-up theorem可以提供部分符合条件的命题.

根据哥德尔不动点定理, 我们可以用PA的语言写下一个句子 [公式] 并且在PA中证明" [公式] [公式] 不存在哥德尔编码小于100^100^100的证明". 其中"哥德尔编码小于100^100^100"只是为了固定好的测量证明长度/复杂程度的方法 (例如我们可以定义"一个证明的长度/复杂度就是这个证明的哥德尔编码的自然数"). 如果我们哥德尔编码采用的是finite sequences的prime number coding, 那么哥德尔编码的大小的确对应了证明符号的多少.

Claim: 1) PA [公式] ; 2)不存在哥德尔编码小于100^100^100的, 从PA公理出发, 并且以 [公式] 为最后一行的证明

如何证明2):

首先我们回顾一下PA如何讨论自己的证明: PA的语言中存在一个带两个自由变元的语句, prf(x,y). 这个语句capture了PA的证明关系.

"prf(x,y) capture了PA的证明关系"的意思是说, PA语言中的谓词 prf(x,y)有著如下特质: 如果P是个对语句S的(以PA公理出发的)证明, 那么PA也可以证明prf(n, [公式] ), 其中n是对P作为finite sequence的哥德尔数编码, "S"是S的哥德尔数; 如果P不是个对语句S的(以PA公理出发的)证明, 那么PA也可以证明~prf(n, [公式] ).

我们现在用反证法证明2). 假设2)不成立. 也就是假设PA可以证明 [公式] , 并且有哥德尔编码小于100^100^100的证明.

令P为该证明, 令m为P的哥德尔数编码. 那么根据上面对prf(x,y)的回顾, 我们可以得知PA能证明 [公式] . 其中prf(x,y)是上述的PA中可定义的二元关系, 并且prf(x,y) capture了PA的证明关系.

根据 [公式] 的定义, 如下句子是PA的定理:

"不存在一个自然数n, 使得n小于100^100^100, 并且prf(n, [公式] )".

通过逻辑推理和PA的基本性质, 我们可以推论出如下PA定理: "对于每一个小于100^100^100的自然数k, ~prf(k, [公式] )". 这个与 [公式] 矛盾. 2)证毕

如何证明1): 因为我们已经证明了2), 也就是说不存在哥德尔数小于100^100^100的对 [公式] 的证明. 由于prf(x,y) capture了PA的证明关系, 我们有如下PA定理: [公式] . 但是根据 [公式] 的定义, PA可证 [公式] 与上一句话里的定理等价. 所以 [公式] 可证 [公式] . 1)证毕.

总结一下到目前为止我们都了解了什么:

首先, 我们知道了PA可以证明 [公式] (而且我们只用了不到一页纸的文字来证明)

其次, 我们知道如果要从PA的公理出发, 我们必须要用非常非常非常多的字元来证明 [公式] . (显然, 100^100^100只是我随手选的数字, 我们可以随意替换为更大的数字).

所以, 文章开头定义的 [公式] 这个语句以及它的一系列变体, 就符合"证明它为真的难度大于证明它可证真的难度".

但是为什么我在文章开头要说"部分符合条件的命题"呢? 这是因为我在上述讨论中小小地作弊了一下, 偷偷换了几次理论. 想要看清这点, 我们仔细审查一下, 我们对于2)的证明到底证明了一个什么东西:

1.出于反证法, 我们假设了结果不成立.

2.根据PA的性质, 我们可以推论出我们上面的假设可以推论出"PA可证S"

3.经过推理, 我们又推论出了"PA可证~S"

4. 矛盾. 所以我们开头的假设是错的.

细心的读者应该可以看出, 我们2和3步没有推导出任何矛盾(recall: 矛盾是形为[P ~P]的一个句子). 我们只推论出了["PA可证S" "PA可证~S"]. 我们并没有推论出["PA可证S" ~"PA可证S"]. 在对2)的证明中, 我偷偷把工作环境(也就是我的元理论)换成了PA+Con(PA), 才能让["PA可证S" "PA可证~S"]成为矛盾.

也就是说, 之所以"证明它可证真的难度"比"证明它为真的难度"低, 是因为在"证明它可证真"的时候, 我们换了一个更强的系统. 如果我们都是用PA+Con(PA)的话, 那么实际上, 我们可以把2)中的论证看作是PA+Con(PA)中对上述 [公式] 的证明. 在这个情况下(元理论固定为PA+Con(PA)), "证明它可证真的难度"和"证明它为真"的难度又变得差不多了.

所以我们可以进一步问：

存不存在命题P, 使得PA可以证明P, 并且PA也可以证明 [公式] ; 但是从PA公理出发, 最短的对" [公式] "的证明要比最短的对P的证明要简单? (或者说前者的哥德尔数（/证明步数/证明所用的符号等）比后者的要小很多). 这里估计就涉及到证明复杂度的知识了, 如果没有什么我没有留意到的特别明显的事实, 不然的话这里已经超出了我的知识范围. 希望更懂这方面的人可以回答.

这个先要定义什么是难度吧，

不过如果能证明为真，一定可以证明可证为真

如果题主问的是：是否有某个命题，已经证明它可被证明，但本身还未被证明？

最近刚好看到这篇文章：https://www.scottaaronson.com/blog/?p=2725

研究了一下，它其实证明了包括哥德巴赫猜想和黎曼猜想在内的猜想都是可证明的，只要把那个图灵机程序运行充分长时间，只是这个时间要大于BB(3000)之类神仙大数.....所以，我认为它符合题主的要求。

参看：

adamyedidia/parsimony

知乎用户：大一，再学多少年可以接触到前沿数学？?

www.zhihu.com图标

这里说的问题显然可证明或者证否。然而目前还是open的。不知道这个是否是题主的意思？

不存在。它们的复杂度一定相同。

「一个命题为真」与「一个命题可证真」是等价的。

现在提出两个命题：

X命题：命题Z为真。

Y命题：命题Z可证真。

X命题和Y命题是什么关系？它们是等价关系。

证明：X与Y是等价关系。

先证明X-&>Y，显然，真命题一定可证真，不然红口白牙、天地良心，你凭啥说它是真命题。

再证明Y-&>X，显然，可证真的命题一定是真命题，不然红口白牙、天地良心，你凭啥说它可证真。

两个等价的问题复杂度一定相同

显然，如果两个问题等价，解决了其中一个就解决了另外一个。

停机问题

图灵说存在计算机无法解决的问题：停机问题。

停机问题的关键在于：要想证明它能「停机」，就必须走到「停机」那一步才行。

回到此问题，要想证明一个问题「可证」，就必须要走到「把问题证明」这一步。

「原子性」是资料库里形容两个操作必须都成功或者都失败，不能存在部分完成的现象。

「可证明」与「证明」这两个过程就是原子性的。

显然，证明它为真的前提，是得要先证明它可证真。

不存在，可证真是证其为真的前提条件。。即必要不充分条件。不可证真而先强行证其为真那是诡辨...

比如题主这个命题

「存在一个数学命题，证明它为真的难度大于证明它可证真的难度。」

想要想要证明它为真需要对所有命题进行讨论

而证明它可证真只需要一个例子

不知道够严谨么？欢迎指教

民科附体。。。0.99...=1

把可证真（信息不必足）理解成二者之间无限小的一点

把证真（信息必须足）理解成二者之间无限多的全部点

推荐阅读：
相关文章