數學上能否指出某個公理體系中符合哪些條件的真命題是可以證明的，符合哪些條件的命題是「真而不可證」的？

哥德爾不完備性定理說道，任何相容的形式系統，只要蘊涵皮亞諾算術公理，就可以在其中構造在體系中既不能證明也不能否證的命題（即體系是不完備的）。那麼數學上能否進一步指出在某個具體的公理體系中符合哪些條件的真命題是可以證明的，符合哪些條件的命題是「真而不可證」的？

---

題主的問題很好，這涉及到數理邏輯中「語法的」(syntactical)和「語義的(semantic)」概念之間的區別. 先放結論：(1) 否，但取決於「判定」的含義；(2) 只有形式系統無法討論「真」.

UPDATE: 增加了關於不完備性定理的討論.

粗體代表重要，粗體代表重要，斜體代表玩梗，不喜歡看玩梗的請自動忽略.

我們來考察「可證」與「真」這兩個概念.

所謂「可證」，是相對一個形式系統來說的。具體地說，一個命題 σ 在系統 Γ 中可證是指存在一列公式，每一個：

1. 是 Γ 中的句子，
2. 或是一條邏輯公理，
3. 或是由之前出現過的兩個公式經由 Modus ponens (latin: the way that affirms by affirming) （其實就是三段論推理）得到.

並且最後一個公式為待證的命題 σ (Hilbert system).

可以看到，上面所有涉及的概念都是「語法的」，即只涉及數學符號的變換. 至於這些符號的意義究竟是什麼暫付闕如.

這樣定義直觀上當然保證了如果 Γ 中的句子都「成立」，那麼 σ 也「成立」（保真性），因為邏輯公理和推理規則都是「放之四海而皆準」的. 然而「成立」是一個十分模糊的說法，什麼叫「成立」？我們來看這樣的陳述：「如果將 0 作為單位元，+ 作為運算，-x 作為 x 的逆元，那麼群論公理在整數集中成立」. 可以看到，「成立」或數理邏輯中通常說的「真」，實際上是在一定的條件下，一個形式系統與一個集合之間的關係（更準確的說不是一個單純的集合，而是指定了一些「解釋」的集合，如這裡將群論公理中提到的單位元解釋為 0, 運算解釋為加法等. 這樣的集合稱為結構；如果 Γ 在該結構中成立則稱此結構為 Γ 的模型）. 因此，離開具體的結構，是無法談論「真」的. 因此第二個問題沒有意義.

不過，第二個問題與 G?del 完備性定理 (Godel completeness theorem) 相關. 該定理是說，對任意相容的形式系統 Γ, 如果命題 σ 在 Γ 的所有模型中都成立，則 σ 可由 Γ 證明. 例如，如果某性質是所有群共有的，則一定可以用群論公理證明. （反過來也對，即前面提到的保真性；相關的定理被稱為可靠性定理 (Soundness)）在這個意義下，可以說「在所有模型中真」即「可證」. 注意該定理與系統的強度無關；強於 Peano 算術的系統，只要是相容的，也具有這個性質.

或問，不完備性定理與完備性定理豈不矛盾？第二不完備性定理是說，對於充分複雜的形式系統，如果它是相容的，那麼它不能證明自身是相容的. 這涉及到數理邏輯中最容易混淆的概念：形式定理與元定理 (Metatheorem). 簡而言之，這個陳述中兩個「相容的」含義有微妙的區別.

有了證明序列的概念，很容易定義相容性：稱 Γ 是相容的，是指不存在一個由 Γ 到矛盾式的證明. （簡便起見，如果 Γ 強於皮亞諾算術，不妨將該矛盾式取為 0 = 1）. 這是關於形式系統 Γ 的一個陳述，這個陳述本身在形式系統之外. 另一方面，由於所有證明序列都是滿足一定規則的有窮字元串，可以借適當的編碼將它們與自然數對應. 因此「Γ 相容」本身也可以形式化為

其中"codes a proof sequence"及"proves"都是在形式語言中定義的關係；這一形式語句通常簡記為 Con(Γ). 所以說存在兩個版本的相容性：「外部的」，即系統之外（元理論中）的相容性，和「內部的」（形式化的）相容性. 第二不完備性定理是說一個系統如果在外部看是相容的，則無法證明內部的相容性.

或問，既然 Γ 本身是相容的，那麼 Γ 每個模型中 Γ 都是相容的，因此由完備性定理，Γ 應能證明自身的相容性. Good question! 這裡的陷阱在於，即使 Γ 在外部看是相容的，在內部看也未必相容！這是由於在 Γ 的模型中可能存在「非標準自然數」（見 Non-standard model of arithmetic），它們編碼了 Γ 到矛盾式的證明；而在外部看，這些對象是無窮的，因而不是一個合法的證明序列. 因此第二不完備性定理與完備性定理並不矛盾；相反，兩者結合還可以得出一個前者的較不容易混淆的等價表述：對於充分複雜的形式系統 Γ, 如果 Γ 是相容的，則存在一個的模型. 當然，想要在較短的篇幅內講明白非標準算術是不可能的，如果想要了解更多，參見最後一句.

至於第一個問題，相當於問證明序列能否「有效地」 (Effectively computable, 通常譯作「能行地」，但我覺得這個詞有點奇怪)找到. 這又涉及到數理邏輯的另一個分支——可計算性理論. 簡而言之，和停機問題類似：只要枚舉所有的證明序列（滿足一定規則的有限長字元串），便可以找到所有可證的命題；然而，這將消耗無限的計算時間. 如果一個命題可證，一直枚舉下去一定能找到一個證明，即搜索在有限時間內終止；若否，則永遠找不到證明. 即，驗證某命題確實可證是可行的；然而並沒有什麼卯月，對於充分複雜的形式系統，判定某命題是否可證是做不到的. （也就是御坂妹 @蘇暖暖 所引用的命題，と徐天00001這樣解釋道）即「可證」是半可判定的，又稱「能行可枚舉」/「遞歸可枚舉」/「可計算可枚舉」 (Computably enumerable, 提出這個術語的人你出來！我從未見過如此糟糕的術語！)的. 當然，要精確定義這些可計算性概念本身也不是一件容易的事，在這裡就不多說了，可以理解為「完全不用動腦子就能做的事」，或者「機器也肯定能做的事」

「真」與「可證」之間的區別實際上推動了整個數理邏輯的發展. 「四大論」（證明論，模型論，可計算性理論與集合論）中至少前三者皆濫觴於此. 如果你有興趣的話，和 G?del簽訂契約，成為數理邏輯少年吧！

---

遺憾的是，不能。

---

窩覺得你的腦洞大概等價於這個！

判定性問題(Decision problem)

最初是於1936年，丘奇用λ演算（Lambda calculus）給出了判定性問題的一個否定的解，證明了PA不可判定……（也就是蘇暖暖的回答中的塗紅部分啦。。）隨著科學的進步……越來越多的不可判定問題被發現了！
WIKI資料：不可判定問題列表（List of undecidable problems）

---

我印象中結論是存在一系列這種命題是不可遞歸的。其中有個叫goodstein 定理已經證明了在一階邏輯不可證，需要用二階邏輯證明為真。

---

第一個問題：從某種意義上來說可以，因為在一個形式系統中，可以應用的證明規則是有限的，所有可以被證明的 命題是re的，那麼所有可以被某個特定program驗證的命題就是你想知道的那些命題。

第二個問題：如果你想說的條件，指的是一些類似於演算法的規則，那麼答案是否定的。因為所有真命題的集合是productive的，換句話說，你用任何方法想要effectively enumerate這些命題，總會有遺漏。

---

可以的，兩個相同的規則球體，3個以上的不規則球體垂直重疊，可計算，不可驗證。

---

假設:哥德巴赫猜想是真的，但是它不存在有限長度的證明，也就是說除了逐一驗證外並沒有什麼好辦法。
以上應該是你說的那種命題的存在的一種形式。

---

推薦閱讀：