Intuitionistic and classical natural deduction systems with the catch and the throw rules (Q1392143)

Two natural deduction systems \(\text{NJ}_{c/t}\) and \(\text{NK}_{c/t}\) are introduced. \(\text{NJ}_{c/t}\) is an extension of the intuitionistic natural deduction system NJ with the catch and throw rules. \(\text{NK}_{c/t}\) is an extension of the classical natural deduction system NK with the catch and throw rules. These rules are motivated from catch and throw program constructs. \(\text{NJ}_{c/t}\) and \(\text{NK}_{c/t}\) are formulated in the standard way, except that (1) an assumption variable is attached to each assumption formula in a proof figure in order to capture the mechanism of variable abstraction in the interpretation rule and disjunction elimination rule, and (2) a tag variable is attached to each premise of the throw rule in order to capture the mechanism of variable abstraction in the catch rule. The main results of the paper are that \(\text{NJ}_{c/t}\) and \(\text{NK}_{c/t}\) are logically equivalent to NJ and NK, respectively. Also an interpretation of \(\text{NJ}_{c/t}\) in terms of an extension of type-free lambda calculus by the catch and throw mechanism is given. This interpretation is an extension of the Curry-Howard isomorphism between NJ proofs and lambda terms.