第2不完全性定理からLöbの定理を導く
任意の文$ \varphiに対し，$ T \vdash \mathrm{Pr}_T(\ulcorner \varphi \urcorner) \to \varphi \implies T \vdash \varphi
Proof
2を仮定する．
対偶と演繹定理より$ T + \lnot \varphi \vdash \lnot \mathrm{Pr}_T(\ulcorner \varphi \urcorner) 導出可能性条件D2（の変種）の対偶$ T \vdash ( \mathrm{Pr}_T ( \ulcorner \varphi \urcorner ) \land \lnot \mathrm{Pr}_T ( \ulcorner \psi \urcorner ) ) \to \lnot \mathrm{Pr}_T ( \ulcorner \varphi \to \psi \urcorner ) より，$ T + \lnot\varphi \vdash ( \mathrm{Pr}_T ( \ulcorner \lnot \varphi \urcorner ) \land \lnot \mathrm{Pr}_T ( \ulcorner \bot \urcorner ) ) \to \lnot \mathrm{Pr}_T ( \ulcorner \lnot \varphi \to \bot \urcorner )
更に，$ T + \lnot\varphi \vdash ( \mathrm{Pr}_T ( \ulcorner \lnot \varphi \urcorner ) \land \mathrm{Con}_T ) \to \lnot \mathrm{Pr}_T ( \ulcorner \lnot \varphi \to \bot \urcorner )
Lem2より$ T + \lnot\varphi \vdash \mathrm{Con}_T
よって$ T + \lnot \varphi \vdash \lnot \mathrm{Pr}_T ( \ulcorner \lnot \varphi \to \bot \urcorner )
形式化された演繹定理より$ T + \lnot \varphi \vdash \lnot \mathrm{Pr}_{T + \lnot \varphi} (\ulcorner \bot \urcorner ) References