Curry-Howard for Classical Logic

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 \lambda-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 \lnot\lnot A \to A is the type of callcc.

Following that, a veritable flurry of \lambda-calculi for classical logic was developed. It appears that no solution has emerged as canonical. Amongst others, we have:

• Felleisen's \lambda\mathcal{C} calculus, as typed by Griffin 1990
• Parigot's \lambda\mu-calculus
• Curien and Herbelin's \bar{\lambda}\mu\tilde{\mu}-calculus

Joyal's lemma

One of the key characteristics of classical logic is the principle of double negation elimination, i.e. the theorem

\lnot\lnot A \to A

(The other direction, viz. A \to \lnot\lnot A, is intuitionistically provable if \lnot A := A \to X.)

As in the Curry-Howard correspondence we are mainly concerned about proofs. Thus, as A and \lnot\lnot A are logically equivalent, it is reasonable to consider the proposition that a proof theory of classical logic would require that the proofs of A and the proofs of \lnot\lnot A 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 \mathcal{C} with a distinguished object R for which there is a natural isomorphism

\phi : \textsf{Id}_\mathcal{C} \xRightarrow{\cong} (- \Rightarrow R) \Rightarrow R

is a preorder.

Putting R := \bot, 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.

Which classical logic?

Ariola and Herbelin 2003 point out that in a minimal setting, i.e. one with just implication (\to) as a logical connective, there are at least three possible classical extensions:

• weak classical logic
• minimal classical logic
• full classical logic

These are characterised by the following axioms:

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) \bot \to A, all these logics are equivalent.

Ariola and Herbelin claim that the weak classical logic "seems uninteresting."

References

• The relationship between classical logic and control was first pointed out in

@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}
}

• Fine distinctions between classical axioms in a minimal/implicational setting are made in

@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:

@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}
}