On the formulae-as-types correspondence for classical logic

Abstract

The Curry–Howard correspondence states the equivalence between the constructions implicit in intuitionistic logic and those described in the simplytyped lambda-calculus. It is an insight of great importance in theoretical computer science, and is fundamental in modern approaches to constructive type theory. The possibility of a similar formulae-as-types correspondence for classical logic looks to be a seminal development in this area, but whilst promising results have been achieved, there does not appear to be much agreement of what is at stake in claiming that such a correspondence exists. Consequently much work in this area suffers from several weaknesses; in particular the status of the new rules needed to describe the distinctively classical inferences is unclear. We show how to situate the formulae-as-types correspondence within the proof-theoretic account of logical semantics arising from the work of Michael Dummett andDag Prawitz, and demonstrate that the admissibility of Prawitz’s inversion principle, which we argue should be strengthened, is essential to the good behaviour of intuitionistic logic. By regarding the rules which determine the deductive strength of classical logic as structural rules, as opposed to the logical rules associated with specific logical connectives, we extend Prawitz’s inversion principle to classical propositional logic, formulated in a theory of Parigot’s lambda-mu calculus with eta expansions. We then provide a classical analogue of a subsystem of Martin-Lof’s type theory corresponding to Peano Arithmetic and show its soundness, appealing to an extension of Tait’s reducibility method. Our treatment is the first treatment of induction in classical arithmetic that truly falls under the aegis of the formulae-as-types correspondence, as it is the first that is consistent with the intensional reading of propositional equality.