Questions: Curry-Howard Correspondence

Question 1

Under the Curry-Howard correspondence, what does a value of type A -> B correspond to in logic?

• A. A proof that A is false and B is true
• B. A proof of the implication 'A implies B' — a function that transforms any proof of A into a proof of B
• C. A proof that A and B are equivalent
• D. A disproof of A

Answer: (B)

A function of type A -> B takes an input of type A and produces an output of type B. Under Curry-Howard, this is exactly a proof of 'A implies B': given a proof of A (the input), it constructs a proof of B (the output). The function IS the proof — not a description of a proof, but the proof itself, embodied as a computational object. This is why proof assistants like Coq represent proofs as typed lambda-calculus terms.

Question 2

Under the Curry-Howard correspondence, a type with no inhabitants (no values of that type) corresponds to a proposition that is unprovable.

• T. True
• F. False

Answer: True

If a type T has no inhabitants (no well-typed closed terms of type T exist), then under Curry-Howard, the corresponding proposition has no proof — it is unprovable. The empty type (Void, or False in Coq) has no constructors and no values, corresponding to a logical falsehood. Conversely, a type with at least one inhabitant corresponds to a provable proposition. This is why type inhabitation and provability are the same question viewed from different angles.

Question 3

Explain why the Curry-Howard correspondence works with constructive (intuitionistic) logic rather than classical logic, and what this means for the law of excluded middle.

Model answer: The correspondence naturally aligns with constructive logic because a proof of 'A or B' must provide either a proof of A or a proof of B (corresponding to constructing either a Left or Right value of a sum type). Classical logic's law of excluded middle (A or not A) would require a program that, for any proposition A, decides whether A is true or false — which is not computable in general. Classical reasoning can be recovered by adding axioms (corresponding to non-constructive language features like continuations), but the direct correspondence is with constructive logic.

This is not merely a technical limitation but a philosophical point. Constructive logic requires that existence claims be witnessed by explicit constructions: to prove 'there exists an x such that P(x)', you must produce a specific x. Under Curry-Howard, this means a proof of an existential is a pair (witness, proof), which is a dependent pair type. Classical logic allows proving existence without a witness (by contradiction), which has no direct computational interpretation. The Curry-Howard correspondence reveals that constructive logic IS computation.

Question 4

If proof normalization corresponds to program evaluation under Curry-Howard, what does a non-terminating program correspond to in logic?

Model answer: A non-terminating program corresponds to a 'proof' that never reaches a normal form — effectively a circular or infinite argument that does not actually establish its conclusion. In a consistent logic, proofs of false (the empty type) should not exist, but a non-terminating program of type False would inhabit the empty type, making the logic inconsistent. This is why proof assistants like Coq require all functions to terminate (total functions only), ensuring the logic remains consistent.

This is a critical design constraint for proof assistants. General recursion allows writing fix f. f : A for any type A, which would 'prove' any proposition including False. By restricting to terminating programs (via structural recursion, well-founded recursion, or termination checkers), the system ensures that every type inhabitant is a genuine proof. The tension between expressiveness and consistency — between being a useful programming language and a sound logic — is a central challenge in dependent type theory.