Intuitionistic Proof

---

自然演繹の直観主義体系

テキストでは直観主義の証明論、自然演繹の規則も示しておいた。この直観主義の体系では、二重否定からもとの命題への推論が禁止されるので、背理法やそのほかの推論にかなり大きな制限がかかる。しかし、もちろん、その分、より基本的で厳密な証明が得られるという、基礎づけにかかわるメリットが生じる。幾つか、直観主義の制限のもとでの証明を練習してみよう。

（1）A⊃(B⊃A)

（2）((A⊃(B⊃C))⊃((A⊃B)⊃(A⊃C))

（3）A⊃A

（4）(A⊃B)⊃(～B⊃～A)

（5）A⊃(～A⊃B)

（6）(～A∨B)⊃(A⊃B)

（7）A&～B⊃～(A⊃B)

（8）A⊃～～A

Uchii, S. (1989) 『真理・証明・計算』ミネルヴァ書房、1989。