Towards a Canonical Classical Natural Deduction System

摘要

This paper studies a new classical natural deduction system, presented as a typed calculus named λμlet. It is designed to be iso-morphic to Curien-Herbelin's λμμ-calculus, both at the level of proofs and reduction, and the isomorphism is based on the correct correspondence between cut (resp. left-introduction) in sequent calculus, and substitution (resp. elimination) in natural deduction. It is a combination of Parigot's λμ-calculus with the idea of "coercion calculus" due to Cervesato-Pfenning, accommodating let-expressions in a surprising way: they expand Parigot's syntactic class of named terms. This calculus aims to be the simultaneous answer to three problems. The first problem is the lack of a canonical natural deduction system for classical logic. λμlet is not yet another classical calculus, but rather a canonical reflection in natural deduction of the impeccable treatment of classical logic by sequent calculus. The second problem is the lack of a formalization of the usual semantics of A/x/i-calculus, that explains co-terms and cuts as, respectively, contexts and hole-filling instructions. The mentioned isomorphism is the required formalization, based on the precise notions of context and hole-expression offered by λμlet. The third problem is the lack of a robust process of "read-back" into natural deduction syntax of calculi in the sequent calculus format, that affects mainly the recent proof-theoretic efforts of derivation of λ-calculi for call-by-value. An isomorphic counterpart to the Q-subsystem of λμμ-calculus is derived, obtaining a new λ-calculus for call-by-value, combining control and let-expressions.