# Curry-Howard isomorphism and non-constructive logic

My understanding of the Curry–Howard correspondence is that it shows an isomorphism between constructive logic (also called intuitionistic logic) and computer programs in appropriate typed languages.

Basically, a (logical) proposition corresponds to a type, a proof (of that proposition) is an inhabited type, a function of type $$A \to B$$ is an implication $$A \implies B$$ (regarding the corresponding proposition) an so on...

What I don't understand, is that it is often said that this CH correspondence is crucial in how proof assistant (e.g. Coq or Lean) work, whereas those proof assistant support classical (non-constructive) logic.

My question is: how can this correspondence (about constructive logic) be helpful for proof assistant in the context of classical (non-constructive) logic?

(An explanation in simple words — without too many assumptions on any general knowledge about type systems or proof assistant would be much appreciated)

• Note that the programs simulated by the typical proof assistant are not the same as programs executed on physical hardware. For example, Coq has an extraction phase which can't realize all axioms automatically; the only axioms which are easy to realize are those which are admitted by BHK. Sep 18 at 16:44

I think people sometimes disagree on what exactly Curry-Howard is. But, one way to look at it is an exact correspondence between the syntactic rules for logic and for type theory.

For the presentations type theory is usually based on, this continues to hold for classical logic. Typically type theories are written using natural deduction, and the way excluded middle typically works in that frameworks is as an axiomatic rule:

$$\frac{}{Γ ⊢ A ∨ ¬ A}$$

This is essentially no different from just adding some uninterpreted term of the appropriate type to the corresponding type theory. And that is how classical reasoning is usually enabled in the proof assistants you mention (maybe with another term for the axiom of choice).

Maybe I should also say: the correspondence continues to hold for classical logic in any case. But some presentations of classical logic differ considerably from the presentations usually encountered in type theory. There are studied type theories that correspond to these other presentations, but they're not the ones that are typically used for proof assistants (at least the ones I'm familiar with).

While proof assistants typically use constructive mathematics, the Curry-Howard-Correspondence does not necessarily require constructivism. The important aspect of the correspondence is that the logical rules correspond to the type-checking rules of your programming language of choice.

The "natural" correspondence is constructive, since Curry/Howard were interested in types that were added to the λ calculus to bypass Curry's paradoxon. However, one can add additional features to the programming language at hand with respective typechecking rules that may correspond to a logical axiom not part of constructive mathematics. While the proof assistants you mentioned, like Coq, simply add these axioms as "uninterpreted symbols" (a feature in the programming language without computation), it is actually possible to support classical reasoning without giving up on a computational interpretation: call/cc, as seen in programming languages like Scheme.

To see this, it is instructive to first look at the dynamic and at the static semantics of call/cc. (call/cc f) + 2 will apply f to the "outer context". Essentially, the part (call/cc f) in the whole expression (call/cc f) + 2 will become a "hole" that is to be filled, which is applied to f: (f (λh. h + 2)) Trying to typecheck this, as done in Typing First-Class Continuations in ML, will lead to the type: $$\operatorname{call/cc}:\forall\alpha,((\alpha\to\forall\beta,\beta)\to\alpha)\to\alpha$$ This looks eagerly similar Peirce's Law, which is equivalent to the law of excluding middle, the core feature of classical reasoning! So, even when you are allowed to time-travel, you can establish a feature in your programming language that has a computational interpretation while fulfilling the Curry-Howard-Correspondence.

The correspondence itself is "disconnected" from the concrete logic or programming language at hand, i.e., it does not matter whether you look at classical logic, constructive logic, linear logic, minimal logic, ultrafinitist logic, ..., whatever logic and likewise for programming languages. And moreover, the correspondence itself is "disconnected" from the computation of the programming language, i.e., we can add "compiler intrinsic functions" or "custom axioms without computational meaning" that nonetheless typecheck (after all, not everything has to compute in a proof assistant, since it is not a programming language). The key point is really that "whatever typechecks in your programming language has an interpretation in (some) logic". In turn, the correspondence is helpful for proof assistants in the context of whatever logic you are interested in.

• Yes, the reason this option isn't really available to proof assistants is that it introduces non-determinism into the reduction relation, and that becomes unsound in dependent type theory if you incorporate it naively. If you only include EM for genuine propositions with at most one value, it's less problematic. Or, you can do something described in this paper, but I'm not sure how usable that would be for proof assistant purposes. But just not giving a computational meaning to EM is, obviously, the easiest. Sep 18 at 16:09

The Curry-Howard correspondence is not crucial for functioning of a proof assistant. Unforunately, the term "Curry-Howard correspondence" seems to be misused nowadays for all sorts of things.

My understanding is that a Curry-Howard correspondence arises when one exhibits a translation (in both directions!) between a logic and a type theory that converts proofs to terms and vice versa.

However, Lean and Coq use a different approach, as they are both type theories equipped with a universe Prop of propositions, thereby embedding logic into type theory. In the case of Lean, the logic is classical. I would call such a setup an embedding of logic into type theory, not an "isomorphism".