用户: HoshinoKoji/数理逻辑/命题集散

1一阶逻辑公理系统

命题 1.1 (自反性). $⊢ φ \to φ$ .

证明. 给出如下证明序列.

(1)	$φ \to (φ \to φ) \to φ$ (P1)
(2)	$(φ \to (φ \to φ) \to φ) \to (φ \to φ \to φ) \to (φ \to φ)$ (P2)
(3)	$(φ \to φ \to φ) \to (φ \to φ)$ (MP)
(4)	$φ \to φ \to φ$ (P1)
(5)	$φ \to φ$ (MP)

于是得证.

$□$

命题 1.2 (双重否定消去). $⊢ \neg\neg φ \to φ$ .

证明. 给出如下证明序列, 略去与 (1.1) 完全相同的部分.

(1)	$(\neg φ \to \neg φ) \to (\neg φ \to \neg\neg φ) \to φ$ (P3)
(2)	$\neg φ \to \neg φ$ (1.1)
(3)	$(\neg φ \to \neg\neg φ) \to φ$ (MP)
(4)	$((\neg φ \to \neg\neg φ) \to φ) \to \neg\neg φ \to ((\neg φ \to \neg\neg φ) \to φ)$ (P1)
(5)	$\neg\neg φ \to ((\neg φ \to \neg\neg φ) \to φ)$ (MP)
(6)	$(\neg\neg φ \to (\neg φ \to \neg\neg φ) \to φ) \to (\neg\neg φ \to \neg φ \to \neg\neg φ) \to (\neg\neg φ \to φ)$ (P2)
(7)	$(\neg\neg φ \to \neg φ \to \neg\neg φ) \to (\neg\neg φ \to φ)$ (MP)
(8)	$\neg\neg φ \to \neg φ \to \neg\neg φ$ (P1)
(9)	$\neg\neg φ \to φ$ (MP)

于是得证.

$□$

命题 1.3. $⊢ \neg\neg φ \to ψ \to φ$ .

证明. 给出如下证明序列, 略去与 (1.2) 完全相同的部分.

(1)	$φ \to ψ \to φ$ (P1)
(2)	$(φ \to ψ \to φ) \to \neg\neg φ \to (φ \to ψ \to φ)$ (P1)
(3)	$\neg\neg φ \to φ \to ψ \to φ$ (MP)
(4)	$(\neg\neg φ \to φ \to (ψ \to φ)) \to (\neg\neg φ \to φ) \to (\neg\neg φ \to ψ \to φ)$ (P2)
(5)	$(\neg\neg φ \to φ) \to (\neg\neg φ \to ψ \to φ)$ (MP)
(6)	$\neg\neg φ \to φ$ (1.2)
(7)	$\neg\neg φ \to ψ \to φ$ (MP)

于是得证.

$□$