形式化されたLöbの定理の証明

ここでは、証明可能性論理の文脈で重要となる、形式化された Löb の定理の証明を示す。
そもそも Löb の定理とは、次のような主張であった。

Löbの定理
$T$ を $\mathrm{PA}$ の r.e. 拡大理論とする。また $\mathrm{Pr}_T(x)$ は可導性条件 $\mathrm{D2}$, $\mathrm{D3}$ を満たす証明可能性述語とする。このとき、任意の式 $\varphi$に対して：

$$T \vdash \mathrm{Pr}_T(\varphi) \rightarrow \varphi \quad \Rightarrow \quad T \vdash \varphi$$

すなわち、ある命題 $\varphi$ を証明するのに、その形式的証明可能性を公理に加えても問題ないことを述べている。

証明は省略するが、形式化された演繹定理と Gödel の第2不完全性定理を組み合わせることで容易に示すことができる。

Löb の定理は形式化できることが知られている。

形式化された Löb の定理
$T$, $\mathrm{Pr}_T(x)$ の設定は前と同様とする。このとき、任意の $\varphi$ に対して：

$$\mathrm{PA} \vdash \mathrm{Pr}_T(\mathrm{Pr}_T(\varphi) \rightarrow \varphi) \rightarrow \mathrm{Pr}_T(\varphi)$$

当該定理の証明を以下に示す。

Proof

不動点補題より、次を満たす文 $\sigma$ が存在する（いわゆる「サンタクロース文」の変種）：

$$\mathrm{PA} \vdash \sigma \leftrightarrow (\mathrm{Pr}_T(\sigma) \rightarrow \varphi)$$

可導性条件 $\mathrm{D1},\mathrm{D2}$より：

$$\mathrm{PA} \vdash \mathrm{Pr}_T(\sigma) \rightarrow (\mathrm{Pr}_T(\mathrm{Pr}_T(\sigma)) \rightarrow \mathrm{Pr}_T(\varphi))$$

可導性条件 $\mathrm{D3}$より：

$$\mathrm{PA} \vdash \mathrm{Pr}_T(\sigma) \rightarrow \mathrm{Pr}_T(\varphi)$$

よって：

$$\mathrm{PA} \vdash (\mathrm{Pr}_T(\varphi) \rightarrow \varphi) \rightarrow (\mathrm{Pr}_T(\sigma) \rightarrow \varphi)$$

さらに、可導性条件 $\mathrm{D1},\mathrm{D2}$ と $\sigma$ の作り方より：

$$\mathrm{PA} \vdash \mathrm{Pr}_T(\mathrm{Pr}_T(\varphi) \rightarrow \varphi) \rightarrow \mathrm{Pr}_T(\sigma)$$

したがって：

$$\mathrm{PA} \vdash \mathrm{Pr}_T(\mathrm{Pr}_T(\varphi) \rightarrow \varphi) \rightarrow \mathrm{Pr}_T(\varphi) \quad \blacksquare$$

この定理の内容を様相演算子を用いて記述すると

$$\Box(\Box\varphi \rightarrow \varphi) \rightarrow \Box\varphi$$

となり、これは様相論理 GL の公理 L に対応する。

このことから、特定の証明可能性述語は様相演算子として良く振る舞うことが読み取れる。

実際、理論 $T$ を弱く表現する $\Sigma_1$ 論理式 $\tau(v)$ によって構成された Feferman 的な証明可能性述語 $\mathrm{Pr}_\tau(x)$ の様相原理は GL で尽くされることが知られている（ただし、$T$ が $\Sigma_1$ 健全な場合に限る）。

参考文献

• 佐野勝彦‧倉橋太志‧薄葉季路‧黒川英徳‧菊池誠 (2016).『数学における証明と真理―様相論理と数学基礎論―』共⽴出版
• 倉橋⼤志.『証明可能性述語の様相論理』