20260610_1

20260527_1

---

---

自然演繹は証明体型

ラムダ計算は計算体型

自然演繹には導入規則と除去規則が存在

$\to$の導入

$\mathbb{P}\to \mathbb{Q}$を証明するためには$\mathbb{P}$を一時的に仮定して$\mathbb{Q}$を証明すればよい

$[\mathbb{P}{]}^n$(閉じた仮定)は$\to$の導入によって$\mathbb{P}$という一時的仮定が閉じられたこと、そして$n$という番号は一時的仮定が閉じられた場所を示している

$\forall x(Fx\to Gx)⊢Ft\wedge Ht\to Gt$を示したい

まずは$\forall x(Fx\to Gx)$を仮定して$Ft\wedge Ht\to Gt$を示す

$$\frac{\frac{\frac{[Ft\wedge Ht{]}^1}{Ft}\wedge E\frac{\forall x(Fx\to Gx)}{Ft\to Gt}\forall E}{Gt}\to E}{Ft\wedge Ht}\to I,1$$

$\forall$の導入

$$\frac{\mathbb{P}(x)}{\forall x\mathbb{P}(x)}$$

ただし、$\mathbb{P}(x)$に至る証明の開いた仮定に$x$は自由変更として現れない

ダメな例

\begin{align}& \mathbb{Q}(x) \nonumber \\& \quad \vdots \nonumber \\& \frac{\mathbb{P}(x)}{\forall x \mathbb{P}(x)} \forall I\end{align}
$\mathbb{P}(x)$の証明は$\mathbb{Q}(x)$に依存しているのに、制限されていた$x$を再度使っている
$\frac{Fy}{\forall yFy}\forall I$
$Fy$を開いた仮定として、$Fy$を結論とする証明になっている

$$\frac{\frac{\forall xFx}{Fy}\forall E}{\forall yFy}\forall I$$

ならOK

$\forall x(Fx\to \forall yGy)⊢\forall x\forall y(Fx\to Gy)$

• $Fx\to Gy$を導きたい

$$\frac{\frac{\frac{\frac{\frac{[Fx{]}^1\frac{\forall x(Fx\to \forall yGy)}{Fx\to \forall yGy}\forall E}{\forall yGy}\to E}{Gy}\forall E}{Fx\to Gy}\to I,1}{\forall y(Fx\to Gy)}\forall I}{\forall x\forall y(Fx\to Gy)}\forall I$$

$\neg$の除去/導入

$\neg$は$\to$の特別なケースとして考えられる

$\neg E$ (除去規則)

$$\frac{\mathbb{P}\neg \mathbb{P}}{\perp }\neg E$$

$\neg I$ (導入規則)

$$\begin{array}{c}[\mathbb{P}{]}^n\\ ⋮\\ \frac{\perp }{\neg \mathbb{P}}\neg I,n\end{array}$$

(仮定$[\mathbb{P}{]}^n$を閉じて$\neg \mathbb{P}$を導く)

$Fx\to Gx,\neg Gx⊢\neg Fx$

$$\frac{\frac{\frac{[Fx{]}^{1}Fx\to Gx}{Gx}\to E\neg Gx}{\perp }\neg E}{\neg Fx}\neg I,1$$

$\forall x(Fx\to Gx),\neg Ga⊢\neg Fa$

$$\frac{\frac{\frac{[Fa{]}^1\frac{\forall x(Fx\to Gx)}{Fa\to Ga}\forall E}{Ga}\to E\neg Ga}{\perp }}{\neg Fa}\neg I,1$$ $$\frac{\frac{\frac{\frac{[Gx{]}^2\frac{[Fx{]}^1\frac{\forall x(Fx\to \neg Gx)}{Fx\to Gx}\forall E}{\neg Gx}\neg E}{\perp }\neg E}{\neg Fx}\neg I,1}{Gx\to Fx}\to I,2}{\forall x(Gx\to \neg Fx)}\forall I$$