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。