‚‰-Calculus: A NATURAL DEDUCTION FOR CLASSICAL LOGIC
Yuichi Komori · 2002
In this note, we will pose a new system, named ‚‰{calculus. While the type assignment system TA‚ gives a natural deduction for intuitionistic implicational logic, the type assignment system TA‚‰ gives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem fi there exists a proof of fi in TA‚‰ enjoying the subformula property. Ryo Kashima has posed a natural deduction system for the classical implicational logic. His system has three rules, the elimination of the implication, the introduction of the implication and the case rule. The author noticed that the introduction of the implication is derivable from the case rule and the weakening. So we have gotten the system TA„ from Kashima’s system by replacing the introduction of implication by the weakening (cf. [3]). Then we have discovered the ‚‰{calculus, introduced in the present paper.