哥德爾的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

把可證真（信息不必足）理解成二者之間無限小的一點

把證真（信息必須足）理解成二者之間無限多的全部點

推薦閱讀：
相關文章