The Curry-Howard correspondence is a connection between logic and computation.
More precisely, the Curry-Howard correspondence amounts to showing that, if proofs of intuitionistic logic (and subsystems) in natural deduction are written as terms, then these terms are effectively the simply-typed -calculus.
Extending this correspondence to the natural deduction system for classical logic is not evident.
However, [Griffin 1990] suggested that there is a connection between proofs in classical logic and non-local control flow. In particular, they suggested that the double negation elimination (DNE) axiom is the type of callcc.
Following that, a veritable flurry of -calculi for classical logic was developed. It appears that no solution has emerged as canonical. Amongst others, we have:
One of the key characteristics of classical logic is the principle of double negation elimination, i.e. the theorem
(The other direction, viz. , is intuitionistically provable if .)
As in the Curry-Howard correspondence we are mainly concerned about proofs. Thus, as and are logically equivalent, it is reasonable to consider the proposition that a proof theory of classical logic would require that the proofs of and the proofs of are in bijection.
Unfortunately, any such proposal is doomed to fail. This was noticed by André Joyal, who proved the following lemma.
Claim. Any cartesian closed category with a distinguished object for which there is a natural isomorphism
is a preorder.
Putting , this proves that there can be no nontrivial "proof-theoretic semantics" of classical logic where double negation elimination is an isomorphism: all such models are preorders, so essentially Boolean algebras.
A proof of this can be found in the classic book by Lambek and Scott, or in the paper [Streicher and Reus 1998].
[Ariola and Herbelin 2003] point out that in a minimal setting, i.e. one with just implication () as a logical connective, there are at least three possible classical extensions:
These are characterised by the following axioms:
| Logic | Axiom | Name of axiom |
|---|---|---|
| weak | weak Pierce's law (wPL) | |
| weak | excluded middle (EM) | |
| minimal | Pierce's law (PL) | |
| minimal | generalized excluded middle (GEM) | |
| full | double negation elimination (DNE) |
Indeed, none of these axioms are derivable in minimal logic. Also weak is a subset of minimal, and minimal is a subset of full. Moreover, in the presence of ex falso quodlibet (EFQ) , all these logics are equivalent.
Ariola and Herbelin claim that the weak classical logic "seems uninteresting."
Griffin, Timothy G. 1990. ‘A Formulae-as-Type Notion of Control’. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’90, 47–58. ACM Press. https://doi.org/10.1145/96709.96714. [pdf]
@inproceedings{griffin_formulae-as-type_1990,
title = {A formulae-as-type notion of control},
doi = {10.1145/96709.96714},
booktitle = {Proceedings of the 17th {ACM} {SIGPLAN}-{SIGACT} symposium on {Principles} of {Programming} {Languages} - {POPL} '90},
publisher = {ACM Press},
author = {Griffin, Timothy G.},
year = {1990},
pages = {47--58}
}
Ariola, Zena M., and Hugo Herbelin. 2003. ‘Minimal Classical Logic and Control Operators’. In Automata, Languages and Programming, edited by Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, 2719:871–85. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-45061-0_68. [slides]
@inproceedings{ariola_2003,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Minimal {Classical} {Logic} and {Control} {Operators}},
volume = {2719},
doi = {10.1007/3-540-45061-0_68},
booktitle = {Automata, {Languages} and {Programming}},
publisher = {Springer Berlin Heidelberg},
author = {Ariola, Zena M. and Herbelin, Hugo},
editor = {Baeten, Jos C. M. and Lenstra, Jan Karel and Parrow, Joachim and Woeginger, Gerhard J.},
year = {2003},
pages = {871--885}
}
There is a lecture course on Curry-Howard for classical logic by Stephane Lengrand. A general overview of the issues is given in the lecture notes for the course.
Amongst other material, the following contains a proof of Joyal's lemma:
Streicher, Th., and B. Reus. 1998. ‘Classical Logic, Continuation Semantics and Abstract Machines’. Journal of Functional Programming 8 (6): 543–72. https://doi.org/10.1017/S0956796898003141.
@article{streicher_1998,
title = {Classical logic, continuation semantics and abstract machines},
volume = {8},
doi = {10.1017/S0956796898003141},
number = {6},
journal = {Journal of Functional Programming},
author = {Streicher, Th. and Reus, B.},
year = {1998},
pages = {543--572}
}