Towards a canonical classical natural deduction system

Abstract

This paper studies a new classical natural deduction system, presented as a typed calculus named lambda-mu- let. It is designed to be isomorphic to Curien and Herbelin's lambda-mu-mu~-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 lambda-mu -calculus with the idea of "coercion calculus" due to Cervesato and Pfenning, accommodating let-expressions in a surprising way: they expand Parigot's syntactic class of named terms. This calculus and the mentioned isomorphism Theta offer three missing components of the proof theory of classical logic: a canonical natural deduction system; a robust process of "read-back" of calculi in the sequent calculus format into natural deduction syntax; a formalization of the usual semantics of the lambda-mu-mu~-calculus, that explains co-terms and cuts as, respectively, contexts and hole- filling instructions. lambda-mu-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; and provides the "read-back" map and the formalized semantics, based on the precise notions of context and "hole-expression" provided by lambda-mu-let. We use "read-back" to achieve a precise connection with Parigot's lambda-mu , and to derive lambda-calculi for call-by-value combining control and let-expressions in a logically founded way. Finally, the semantics , when fully developed, can be inverted at each syntactic category. This development gives us license to see sequent calculus as the semantics of natural deduction; and uncovers a new syntactic concept in lambda-mu-mu~ ("co-context"), with which one can give a new de nition of eta-reduction.