Contextual Natural Deduction

This paper defines the contextual natural deduction calculus NDc for the implicational fragment of intuitionistic logic. NDc extends the usual natural deduction calculus (here called ND) by allowing the implication introduction and elimination rules to operate on formulas that occur inside contexts. In analogy to the Curry-Howard isomorphism between ND and the simply-typed λ-calculus, an extension of the λ- calculus, here called λc-calculus, is defined in order to provide compact proof-terms for NDc proofs. Soundness and completeness of NDc with respect to ND are proven by defining translations of proofs between these calculi. Furthermore, some NDc-proofs are shown to be quadratically smaller than the smallest ND-proofs of the same theorems