【一階述語論理3】形式的証明と健全性

論理記号の定義

簡単のため形式的証明で論理式を扱う時には次のように定義されているものとする.

定義（論理記号）：
論理記号は

$\bot, \rightarrow, \exists$ のみであるとし, 論理式

$\varphi, \psi$ について,

$\lnot \varphi := \varphi \rightarrow \bot,$
$\varphi \lor \psi := \lnot \varphi \rightarrow \psi,$
$\varphi \land \psi := \lnot ( \varphi \rightarrow \lnot \psi ),$
$\varphi \leftrightarrow \psi := (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi),$
$\forall x \varphi := \lnot \exists x \lnot \varphi.$

一階述語論理の証明系 $\mathcal{H}$

▼ 展開/縮小

一階述語論理の証明系 $\mathcal{H}$

$t, s$ とそれに添え字を付したものは閉項,

$x$ は変数記号,

$\varphi, \psi, \theta$ を論理式,

$f \in \mathcal{F}, R \in \mathcal{P}$ とする. 証明系

$\mathcal{H}$ の公理とは，次の形をした閉論理式であるか, 次の形をした論理式の全称閉包のことである.

[公理系]

■　命題論理の公理
（１） $\varphi \rightarrow \psi \rightarrow \varphi,$
（２） $(\varphi \rightarrow \psi \rightarrow \theta) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \theta,$
（３） $\lnot \lnot \varphi \rightarrow \varphi,$

■　量化子に関する公理
（４） $\forall x (\varphi \rightarrow \psi) \rightarrow \forall x \varphi \rightarrow \forall x \psi,$
（５） $\forall x \lnot \varphi(x) \rightarrow \lnot \exists x \varphi(x),$
（６） $\varphi(t) \rightarrow \exists x \varphi(x),$

■　等号公理
（７） $t = t,$
（８） $t = s \rightarrow s = t,$
（９） $(t_1 = t_2 \land t_2 = t_3) \rightarrow t_1 = t_3,$
（１０） $(t_1 = s_1 \land t_2 = s_2 \land \cdots \land t_n = s_n) \rightarrow f(t_1, t_2, \cdots, t_n) = f(s_1, s_2, \cdots, s_n),$
（１１） $(t_1 = s_1 \land t_2 = s_2 \land \cdots \land t_n = s_n) \rightarrow R(t_1, t_2, \cdots, t_n) \rightarrow R(s_1, s_2, \cdots, s_n),$

[推論規則]

（MP） $\frac{\varphi \rightarrow \psi \quad \varphi}{\psi}$ .

証明の定義

▼ 展開/縮小

定義（証明・証明可能）：

$L$ を言語,

$L$ -閉論理式の集合を

$\Sigma$ ,

$\varphi$ を

$L$ -閉論理式とする．証明系

$\mathcal{H}$ における言語 $L$ についての $\varphi$ の証明とは

$L$ -閉論理式の有限列,

$\quad \varphi_1, \varphi_2, \cdots, \varphi_n,$

で $\varphi_n = \varphi$ であり, $\varphi_i \: (i = 1, 2, \cdots, n-1)$ は $\Sigma$ の元であるか $\mathcal{H}$ の公理であるか $j, k < i$ なる $\varphi_j, \varphi_k$ からの推論規則(MP)による結論となっているようなものである．
また， $\Sigma$ からの言語 $L$ についての $\varphi$ の証明が存在するとき言語 $L$ について $\varphi$ は $\Sigma$ から証明可能といい， $\Sigma \vdash \varphi$ と表す．特に, $\Sigma = \emptyset$ のとき単に $\vdash \varphi$ と表す.

演繹定義

▼ 展開/縮小

定理（演繹定理）：

$L$ を言語,

$L$ -閉論理式の集合を

$\Sigma$ とする．このとき，次が成り立つ．

$\Sigma \vdash \varphi \rightarrow \psi \iff \Sigma \cup \{ \varphi \} \vdash \psi$ .

（証明）
( $\Longrightarrow$ )
$\Gamma \vdash \varphi \rightarrow \psi$ かつ $\Gamma \subset \Gamma \cup \{ \varphi \}$ より， $\Gamma \cup \{ \varphi \} \vdash \varphi \rightarrow \psi$ が成り立つ．よって，(MP)より $\Gamma \cup \{ \varphi \} \vdash \psi$ .
( $\Longleftarrow$ )
$\psi$ の種類によって場合分けする.
　[１] $\psi \in \Gamma$ のとき． $\mathcal{H}$ の公理(1)より $\Gamma \vdash \psi \rightarrow \varphi \rightarrow \psi$ であり，これと $\psi$ で(MP)を使うことで $\Gamma \vdash \varphi \rightarrow \psi$ を得る（注： $\psi \rightarrow \varphi \rightarrow \psi$ とは $\psi \rightarrow (\varphi \rightarrow \psi)$ を表すのであった）．
　[２] $\psi$ が $\mathcal{H}$ の公理のとき． $\Gamma \vdash \psi$ および $\mathcal{H}$ の公理(1)より $\Gamma \vdash \psi \rightarrow \varphi \rightarrow \psi$ より(MP)を使えば $\Gamma \vdash \varphi \rightarrow \psi$ を得る.
　[３] $\psi \equiv \varphi$ のとき. 次の補題4-1で示す．
　[４] $\psi$ が(MP)の結論になっているとき． $\Gamma \cup \{ \varphi \}$ からの $\psi$ の証明の長さに関する帰納法で示す．長さ $１$ の時は[１]～[３]の場合に相当するから示された．証明の長さが $n$ のとき，ある論理式 $\theta$ について $\Gamma \cup \{ \varphi \} \vdash \theta \rightarrow \psi$ および $\Gamma \cup \{ \varphi \} \vdash \theta$ が成り立っているから帰納法の仮定より, $\Gamma \vdash \varphi \rightarrow \theta \rightarrow \psi$ および $\Gamma \vdash \varphi \rightarrow \theta$ を得る. $\mathcal{H}$ の公理(2)より, $\Gamma \vdash (\varphi \rightarrow \theta \rightarrow \psi) \rightarrow (\varphi \rightarrow \theta) \rightarrow \varphi \rightarrow \psi$ が成り立つから(MP)を２回用いることで結論を得る．

□

対偶法

▼ 展開/縮小

補題3-1:

$L$ を言語,

$\varphi$ を

$L$ -閉論理式とする. このとき, 次が成り立つ.

$\vdash \varphi \rightarrow \varphi$ .

（証明）
$\theta \equiv \varphi \rightarrow \varphi$ とすると,

$\vdash (\varphi \rightarrow \theta \rightarrow \varphi) \rightarrow (\varphi \rightarrow \theta) \rightarrow \varphi \rightarrow \varphi,$ 　（公理（２））
$\vdash \varphi \rightarrow \theta \rightarrow \varphi,$ 　（公理（１））
$\vdash \varphi \rightarrow \varphi \rightarrow \varphi,$ 　（公理（１））
$\vdash (\varphi \rightarrow \theta) \rightarrow \varphi \rightarrow \varphi,$ 　（(MP)による）
$\vdash \varphi \rightarrow \varphi.$ 　（(MP)による）

□

補題3-2（二重否定の付与）:

$L$ を言語,

$\varphi$ を

$L$ -閉論理式とする. このとき, 次が成り立つ.

$\vdash \varphi \rightarrow \lnot \lnot \varphi$ .

（証明）
補題3-1より $\vdash \lnot \varphi \rightarrow \lnot \varphi$ が成り立つから,

$\{ \lnot \varphi\} \vdash \lnot \varphi,$ 　（演繹定理）
$\{ \lnot \varphi\} \vdash \varphi \rightarrow \bot,$ 　（否定の定義）
$\{ \lnot \varphi, \varphi\} \vdash \bot,$ 　（演繹定理）
$\{ \varphi\} \vdash \lnot \varphi \rightarrow \bot,$
$\{ \varphi\} \vdash \lnot \lnot \varphi,$ ]
$\quad \vdash \varphi \rightarrow \lnot \lnot \varphi.$

□

補題3-3（対偶法）:

$L$ を言語,

$\varphi, \psi$ を

$L$ -閉論理式とする. このとき, 次が成り立つ.

$\vdash \varphi \rightarrow \psi \iff \vdash \lnot \psi \rightarrow \lnot \varphi$ .

（証明）
( $\Longrightarrow$ )

$\vdash \varphi \rightarrow \psi,$ 　
$\{\varphi\} \vdash \psi,$ 　（演繹定理）
$\vdash \psi \rightarrow \lnot \lnot \psi,$ 　（補題3-2（二重否定の付与））
$\{\varphi\} \vdash \lnot \lnot \psi,$ 　（直前２つで(MP)）
$\{\varphi, \lnot \psi\} \vdash \bot,$ 　（演繹定理と否定の定義）
$\{\lnot \psi\} \vdash \lnot \varphi,$ 　（演繹定理と否定の定義）
$\vdash \lnot \psi \vdash \lnot \varphi.$ 　（演繹定理）

( $\Longleftarrow$ )
　上の証明を逆にたどればよい. ただし, 二重否定の付与の代わりに公理（３）二重否定の除去を使用する.

□

健全性定理

▼ 展開/縮小

定理（健全性定理）：

$L$ を言語とし

$\Sigma$ を

$L$ -閉論理式の集合,

$\varphi$ を

$L$ -閉論理式とする. このとき, 次が成り立つ.

$\Sigma \vdash \varphi \Longrightarrow \Sigma \vDash \varphi$ .

（証明）
証明系 $\mathcal{H}$ の公理として採用した論理式 $\varphi$ が $\vDash \varphi$ を満たすことと, (MP)が $\{\varphi, \varphi \rightarrow \psi\} \vDash \psi$ を満たすことによる.

□

参考文献

[1] 新井敏康，数学基礎論　増補版，東京大学出版会，2021.

[2] ケネス・キューネン, キューネン数学基礎論講義, 日本評論社，2016.

[3] 鹿島亮, 現代基礎数学15 数理論理学, 朝倉書店, 2009.

[4] Stephen Cole Kleene, Introduction To Meta-Mathematics, Ishi Press Internal, 1952.

[5] Joseph R. Shoenfield, Mathematical Logic, CRC Press, 1967.

[6] Richard E. Hodel, An Introduction to Mathematical Logic, Dover Publications Inc, 1995.

論理記号の定義

一階述語論理の証明系H\mathcal{H}

証明の定義

演繹定義

対偶法

健全性定理

参考文献

コメントを残す コメントをキャンセル

一階述語論理の証明系 $\mathcal{H}$

コメントを残すコメントをキャンセル