p→∀v(p) - oupoの日記

最近ゲーデルの不完全性定理の証明に登場する形式的体系 $P$ で遊んでます。
数学ガールゲーデル編を読んで以来、 $p$ から $\forall v (p)$ が導けるという推論規則がなんであるのか、 $p \to \forall v (p)$ を公理とするのではだめなのか気になっていました。その疑問が解決しました。任意の論理式 $p$ について $p \to \forall v (p)$ が定理だとすると形式的体系 $P$ は矛盾するのです。

以下それを示します。

任意の論理式 $p$ について $p \to \forall v (p)$ が定理だとする。
$a \to b$ が定理ならば $\neg b \to \neg a$ が定理だから
　　　 $\neg \forall v (p) \to \neg p$ が定理
$p$ に $\neg p$ を代入して
　　　 $\neg \forall v (\neg p) \to \neg \neg p$ が定理
$\exists$ を使って書きなおすと
　　　 $\exists v (p) \to \neg \neg p$ が定理
$\neg \neg p \to p$ が定理であり、 $a \to b$ と $b \to c$ が定理のとき $a \to c$ が定理だから、
　　　 $\exists v (p) \to p$ が定理
よって任意の論理式 $p$ について $\exists v (p) \to p$ が定理である。 ...(1)

$\alpha$ を自由変数を含まない適当な定理の一つとする。

ここで内包公理より
　　　 $\exists x_2 (\forall x_1 (x_2(x_1) \rightleftharpoons \alpha))$
　　　 $\exists x_2 (\forall x_1 (x_2(x_1) \rightleftharpoons \neg \alpha))$
が定理。
(1)より任意の論理式 $p$ について $\exists v (p) \to p$ が定理だから
　　　 $\forall x_1 (x_2(x_1) \rightleftharpoons \alpha)$
　　　 $\forall x_1 (x_2(x_1) \rightleftharpoons \neg \alpha)$
が定理。
任意の論理式 $p$ について $\forall v (p) \to p$ が定理より
　　　 $x_2(x_1) \rightleftharpoons \alpha$
　　　 $x_2(x_1) \rightleftharpoons \neg \alpha$
が定理。

$p \rightleftharpoons q$ が定理であることは $p \to q$ と $q \to p$ がともに定理であることと同値だから、
　　　 $\alpha \to x_2(x_1)$
　　　 $x_2(x_1) \to \neg \alpha$
が定理。
よって $\alpha$ が定理であるから、
　　　 $\neg \alpha$
が定理。

$\alpha$ と $\neg \alpha$ がともに定理であるから、形式的体系 $P$ は矛盾する。 □

参考図書

数理論理学は数学ガールゲーデル編で初めて触れて、形式的体系 $P$ で遊んでいるうちに興味持って最近「数理論理学の基礎・基本」を買った初心者です＞＜