|
C. A. Stewart
On the formulae-as-types
correspondence for classical logic
PhD thesis, Oxford University, 2000
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.
[ bib |
.pdf |
.ps |
http ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
