Curry-Howard isomorphism and non-constructive logic

Question

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)

Answer 1

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).

Answer 2

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.

Answer 3

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".

Answer 4

I understand the statement that "Curry-Howard is important to proof assistants" as simply a statement that proof assistants work by creating a proof term in a suitable dependently-typed lambda calculus. Once a proof term is created and type-checked, the proof assistant accepts the proof as valid.

So, the whole idea that a proof of a mathematical proposition is equivalent to some "proof term", i.e., to just an expression in a suitable lambda-calculus, is central to how proof assistants work. "Proofs are programs", or more precisely "proofs are lambda-terms". A proof assistant is an interface for people to work with those (very complicated) lambda-terms more easily.

This is not in contradiction to the fact that proof assistants can validate proofs about classical logic. The lambda calculus on which the proof assistant itself works might be based on constructive logic, like most functional programming languages today. But the proof terms can express reasoning about arbitrary axioms and derivation rules.