面倒だな。
フォーミュラ（論理式）というのは、「無意味」な記号列の１種だから命題では
ない。

命題というのは、
真偽の定まった判断の内容。
真偽の定まった文または式（等式とか不等式とか、読んだときに
文になる式のみ）というと、文の文字列のことか、文の内容のことか、
ちょっと微妙な表現になってしまうけどね。

連続体仮説とかも、そう呼ばれる表現の文字列が公理と呼ばれる文字列から
機械的に導出可能なら「証明可能」と言うことになってる。機械的に導出
不可能なら「証明不能」。でも、ゲーデルの想像する望ましい解釈のもとでは
「真」と推定されたのだろう。