Logic Seminar

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。


Last modified May 27, 2008. (c) Soshichi Uchii