形式化された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 の定理は形式化できることが知られている。
$T$, $\mathrm{Pr}_T(x)$ の設定は前と同様とする。このとき、任意の $\varphi$ に対して：
$$
\mathrm{PA} \vdash \mathrm{Pr}_T(\mathrm{Pr}_T(\varphi) \rightarrow \varphi) \rightarrow \mathrm{Pr}_T(\varphi)
$$
当該定理の証明を以下に示す。
不動点補題より、次を満たす文 $\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$ 健全な場合に限る）。
