What is the concept of truth in the Curry-Howard isomorphism?

176 Views Asked by At

Does the Curry-Howard isomorphism give a meaning or a new interpretation to the concept of classical boolean truth ?

The correspondence is about proofs and provability. Proofs are interpreted as programs and formulas/propositions as types. We can't say that a type is true or false but that we can construct a program according to a given type.

When considering only the intuitionistic world of Logic, "constructibility" or "realizability" doesn't seem to match with "truth". But quite recently, we discovered a Curry-Howard correspondence for Classical Logic through control operators and environements ($\lambda\mu$-calculus for instance).

What is truth ? Is it an information about the possibility of realizing a program with a given type ?