patternMinor
Curry-Howard isomorphism and non-constructive logic
Viewed 0 times
howardnonconstructivelogiccurryandisomorphism
Problem
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)
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)
Solution
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).
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).
Context
StackExchange Computer Science Q#162105, answer score: 7
Revisions (0)
No revisions yet.