Abstract

This paper studies a new classical natural deduction system, presented as a typed calculus named View the MathML sourceλ̲μlet. It is designed to be isomorphic to Curien and Herbelinʼs View the MathML sourceλ¯μμ˜-calculus, both at the level of proofs and reduction, and the isomorphism is based on the correct correspondence between cut in sequent calculus, and substitution 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 View the MathML sourceλ¯μμ˜-calculus, that explains co-terms and cuts as, respectively, contexts and hole-filling instructions. View the MathML sourceλ̲μ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 View the MathML sourceλ̲μlet.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 View the MathML sourceλ¯μμ˜ , with which one can give a new definition of η-reduction.