Towards a canonical classical natural deduction system

This paper studies a new classical natural deduction system, presented as a typed calculus named . It is designed to be isomorphic to Curien and 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 and Pfenning, accommodating let-expressions in a surprising way: they expand Parigotʼs syntactic class of named terms.This calculus and the mentioned isomorphism Θ 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 -calculus, that explains co-terms and cuts as, respectively, contexts and hole-filling instructions. 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 .We use “read-back” to achieve a precise connection with Parigotʼs λμ, and to derive λ-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 (“co-context”), with which one can give a new definition of η-reduction.