Other Definitions of Formalized Consistency

[SnO2WMaN]

一般に「理論 $T$ の無矛盾性」を表す文 $\mathrm{Con}_T$ は $\mathrm{Con}_T \equiv \lnot \mathrm{Pr}_T(\ulcorner \bot \urcorner)$ として定義して，この定義の元で第2不完全性定理を証明するのが普通であり，DerivableConditions.leanでもそのようにしている．しかし無矛盾性を表現する文，およびそれを成り立たせるための導出可能性条件は他にもいくつかある．前述の無矛盾性はLöbに帰する（らしい）ので $\mathrm{Con}_T^\mathrm{L}$ とする．他の例は

• Hilbert-Bernaysの無矛盾性 $\mathrm{Con}^\mathrm{HB}_T \equiv \forall x. \lbrack \mathrm{Fml}(x) \land \mathrm{Pr}_T(x) \to \lnot \mathrm{Pr}_T(\dot{\lnot}(x)) \rbrack$

  • 「 任意の論理式 $\varphi$ に対して $T \vdash \varphi$ なら $T \nvdash \lnot \varphi$ 」の形式化

• Gödelの無矛盾性 $\mathrm{Con}^\mathrm{G}_T \equiv \exists x. \lbrack \mathrm{Fml}(x) \land \lnot \mathrm{Pr}_T(x) \rbrack$

  • 「 $T \nvdash \varphi$ な論理式 $\varphi$ が存在する」の形式化

• 証明不能な $\Sigma_1$ 文の存在 $\mathrm{Con}^{\Sigma_1}_T \equiv \exists x. \lbrack \mathrm{\Sigma_1 Fml}(x) \land \mathrm{Sent}(x) \land \lnot \mathrm{Pr}_T(x) \rbrack$

ここで $\dot{\lnot}(x))$ は否定を付けた論理式のGödel数 $\ulcorner \varphi \urcorner \mapsto \ulcorner \lnot \varphi \urcorner$ を計算する関数とし， $\mathrm{Fml}(x)$ は $x$ が何らかの論理式 $\varphi$ のGödel数であることを表現する述語とする． $\mathrm{\Sigma_1 Fml}(x)$ や $\mathrm{Sent}(x)$ も同様．

$\mathrm{Con}^{\Sigma_1}_T$ は $\Sigma_1$ 論理式という概念に触れるのでおそらく算術に直接関わりを持たざるを得ないが， $\mathrm{Con}^\mathrm{HB}_T$ や $\mathrm{Con}^\mathrm{G}_T$ の範囲なら DerivabileConditions.lean のように型クラスなどで抽象的に扱えないだろうか？ 自分は $\mathrm{Fml}(x)$ などの定義や $\dot{\lnot}(x))$ の定義などをどうすればよいかはあまり見当がついておらず，表現能力がどこまであるのかよくわかっていないので，実際には普通に Arithmetizationの範疇かもしれない．

[iehality]

証明可導述語は複数あるので型クラスにする意味があるが， $\dot{\lnot}$ や $\mathrm{Fml}$ を複数定義することはないので型クラスにする利益はあまりないと思う． $\Sigma_1\mathrm{Fml}$ 以外はすでにArithmetizationで形式化されているので，上２つの無矛盾性は今にでも定義はできる．