ゲーデルの不完全性定理で出てくる「証明できない」

質問

ゲーデルの不完全性定理の証明に関する本をいろいろ読んでみましたが（あまり厳密なものは読んでいませんが）、どの本を読んでいても理解が先に進まず立ち止まってしまうところがありました。それは、「証明できない」ということの定式化（言葉がこれで正しいのかわかりませんが）についてです。

ある論理式が「証明できる」というのは、使用できる「公理」と「変形規則（推論というのでしょうか、これも言葉が正確かすみません覚えていません）」を有限回使用してその論理式に実際に到達できること、という理解をしており、これは理解できます。

これに対してある論理式が「証明できない」というのは、以下の（A)(B)（C)のどの意味なのでしょうか。
（A)使用できる「公理」と「変形規則」を有限回使用してもその論理式に実際に到達できない、ということ。
（B)その論理式の否定が証明できる、ということ。
（C）その論理式が証明できない、ということを示す何らかの論理式に、使用できる「公理」を「変形規則」を有限回使用して実際に到達すること。

(A)かなとも思いますが、それってどのように理解すればよいのでしょうか。1000回使用して到達できなくても、1001回使用すれば到達できるかも知れないのでは？　
(B)ではないと思っていますが自信がありません。
(C)は実際には（A)だったり（B)だったりする？。。判断ができません。

昔の一時期、結構悩みました。現在再チャレンジしていており同じ個所で悩んでいます。もやもやを晴らして頂ければ大変うれしいです。

回答No.1

alice_44

「証明できない」の意味は、(A)です。
(B)は「否定が証明できる」ことを、
(C)は「証明できないことが証明できる」ことを表しており、
「証明できない」とは異なります。

ゲーデルの証明不能命題は、存在することだけは証明されていますが、
その命題が証明不能であることもまた証明不能だと判っていますから、
推論が１０００回とか１００１回とか悩む必要もないです。
ゲーデル文は、遠くにありて思ふもの… です。掴むことはできません。