20260617_1

20260610_1

---

直観主義では否定はならばの特殊なケースになる
$\neg Fx\to \perp$とみなすと、$\neg E$

宣言や存在量化氏は直観主義に特有

$A\to B$: Aのどんな証明もBの証明に変換する操作

$\vee$の導入と除去

導入は簡単

$$\frac{P}{P\vee Q}\vee I\frac{Q}{P\vee Q}\vee I$$

除去が大変

$$\begin{array}{rlr}& [\mathbb{P}{]}^n& [\mathbb{Q}{]}^n\\ & ⋮& ⋮\\ \mathbb{P}\vee \mathbb{Q}& \mathbb{C}& \mathbb{C}\\ & & \\ \mathbb{C}& & \end{array}\vee E,n$$

• $\mathbb{P}\vee \mathbb{Q}$
• $\mathbb{P}$と仮定すると$\mathbb{C}$
• $\mathbb{Q}$と仮定すると$\mathbb{C}$

これはダメ

$\frac{\mathbb{P}\vee \mathbb{Q}}{\mathbb{P}}\vee E$

$Fx\to Hx,Gx\to Hx,Fx\vee Gx⊢Hx$

$$\frac{Fx\vee Gx\frac{[Fx{]}^{1}Fx\to Hx}{Hx}\to E\frac{[Gx{]}^{1}Gx\to Hx}{Hx}\to E}{Hx}\vee E,1$$

$\forall x(Fx\vee Gx\to Hx)⊢\forall x(Fx\to Hx)$

$$\frac{\frac{[Fx{]}^1}{Fx\vee Gx}\vee I\frac{\forall x(Fx\vee Gx\to Hx)}{Fx\vee Gx\to Hx}}{\frac{\frac{Hx}{Fx\to Hx}\to I,1}{\forall x(Fx\to Hx)}\forall I}$$

$\forall x(Fx\to Hx),\forall x(Gx\to Hx)⊢\forall x(Fx\vee Gx\to Hx)$

証明（場合分け∨Eを使う）：

$$\frac{\frac{\frac{[Fx\vee Gx{]}^3\frac{[Fx{]}^2\frac{\forall x(Fx\to Hx)}{Fx\to Hx}\forall E}{Hx}\to E\frac{[Gx{]}^2\frac{\forall x(Gx\to Hx)}{Gx\to Hx}\forall E}{Hx}\to E}{Hx}\vee E,2}{(Fx\vee Gx)\to Hx}\to I,3}{\forall x((Fx\vee Gx)\to Hx)}\forall I$$

$\exists$の導入と除去

導入は簡単

$$\frac{\mathbb{P}(t)}{\exists x\mathbb{P}(x)}\exists I$$

除去

$$\begin{array}{rlr}& [\mathbb{P}(a){]}^n& \\ & ⋮& \\ \exists x\mathbb{P}(x)& \mathbb{C}& \\ & & \\ \mathbb{C}& & \end{array}\exists E,n$$

ただし、$a$は$\mathbb{C}$に現れてはいけない
$\mathbb{C}$に自由変項$x$があってはいけない

$\exists xPx,\forall (Px\to Qx)⊢\exists xQx$

$\exists xPx$から直接何かを導くことはできない→$\exists E$を使う必要性

$$\frac{\exists xPx\frac{\frac{[P(a){]}^1\frac{\forall x(Px\to Qx)}{P(a)\to Q(a)}\forall E}{Q(a)}\to E}{\exists xQx}\exists I}{\exists xQx}\exists E,1$$

$Fa,\forall x(Fx\to Gx)⊢\exists xGx$

$$\frac{Fa\frac{\forall x(Fx\to Gx)}{Fa\to Ga}\forall E}{\frac{Ga}{\exists xGx}\exists I}\to E$$

$Fa⊢\exists x(Fx\vee Gx)$

$\frac{\frac{Fa}{\exists xFx}\exists I}{\exists x(Fx\vee Gx)}\vee I$

$\neg \exists xPx⊢\forall x\neg Px$

$$\frac{\frac{\frac{\frac{[P(a){]}^1}{\exists xPx}\exists I\neg \exists xPx}{\perp }\to E}{\neg P(a)}\neg I,1}{\forall x\neg Px}\forall I$$