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。