C.A. Stewart, 2000. On the formulae–as–types correspondence for classical logic. DPhil thesis, Programming Research Group, University of Oxford.
The Curry-Howard correspondence states the equivalence between the constructions implicit in intuitionistic logic and those described in the simply-typed 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 and Dag 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-Löf'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.
The thesis was supervised by Luke Ong, and was examined in March 2000 by Zhaohui Luo and Lincoln Wallen. I have publically distributed three versions of this thesis: in 1998, when seeking an external examiner; in 2000, as submitted to my examiners prior to my defence, and in 2001, the amended copy submitted to Oxford University's Examination Office. (The PDF of the 2001 manuscript (215 pages)) is available for download.
The 2000 version differs from the 1998 version in having a completely rewritten introduction and conclusion. The 2001 version differs from the 2000 in incorporating corrections in reaction to the examiners' criticisms, and also incorporates some additional, speculative commentary in the conclusion.