# What is the philosophical meaning of the Curry-Howard correspondence?

I understand the Curry-Howard correspondence, and its usefulness, from a technical angle; but I don’t understand its philosophical implications.

For example, does the resulting conceptualization of 'propositions as types' mean that propositions can be represented as types, or that propositions actually are types?

The literature is full of computer scientists making vague and imprecise claims about the philosophical significance of the Curry-Howard correspondence, but I find most of these discussions too casual.

Is there a non-trivial, substantive philosophical claim about the nature of proofs or propositions that flows naturally from the Curry-Howard correspondence?

I'm looking for a rigorous discussion of its philosophical consequences, including literature references.

For example, does the resulting conceptualization of 'propositions as types' mean that propositions can be represented as types, or that propositions actually are types?

It is an (informal) correspondence/isomorphism, so propositions are equivalent to types.

It might have some import on a philosophy of mathematics, e.g. relative to one's position in foundations, in that it might be seen as evidence for the need/primality of constructivism in mathematics (for example): but, AFAIK, there is no properly philosophical relevance.

• Why does an “informal correspondence/isomorphism” imply “equivalence”? I find this incorrect. Commented Jul 2 at 14:33
• @JuliusHamilton A correspondence, similarly an equivalence, similarly a bijection, similarly an isomorphism: informally, these are different ways to say the same thing. Commented Jul 2 at 17:24

Having witnessed a debate between a categorical logician/type-theorist and a model theorist, I think there is still (sometimes heated) disagreement about how well different mathematical formalisms “reflect the actual nature of math” amongst people who know these theories at the expert level.

I’ll provide a simple answer while we await a more informed one. I think a good type theorist told me that type theory is just logic with a conceptual extension where propositions need “witnesses”. In logic, if you take a collection of formulas and use a deductive calculus such as sequent calculus to derive theorems, your ability to arrive at a particular formula by applications of those deductive rules constitutes a “proof”. Writing a proof amounts to saying, “if those axioms are true, then this formula is true”. You don’t write “is true” next to a formula, but you just show how the formula can be arrived at from other formulas.

In type theory, a distinction is made between (I think) propositions and judgments! I think this is a distinguishing feature of type theory, and it was identified by Per Martin-Löf. I think the difference is that in type theory, there is an explicit syntax for distinguishing between a proposition merely as a unit of meaning, vs. judging “and this proposition is true (or false)”.

I think you prove a proposition is true by proving that the proposition has a “witness”, which is the type-theoretic way of judging “this proposition is true”. It is written `p : P`. I think `p` is the term, and `P` is the type. I think if P is of type “Proposition”, then proving the type is what is called inhabited (i.e., we know there exists at least one term of that type) means we have found a witness, i.e., proved or judged it true.

I think the answer to your question requires a technical understanding of type theory. But to answer your question of if types are propositions or are just represented as propositions, I think the former. In a blog post by Astra Kolomatskaia and Mike Shulman, they discuss how one way type theory and set theory are paradigmatically different (at least how I understood it) is that type theory in some ways is more “conceptually faithful” than set theory. Set theory is like an encoding of information and structures, but type theory allows you to define a better depiction of the logical world by allowing you to designate different categories of things from the beginning.

The introduction to the book “Categorical Logic and Type Theory” corroborates this:

This is probably a very good resource to read further on this:

In type theory, the paradigm of propositions as types says that propositions and types are essentially the same. A proposition is identified with the type (collection) of all its proofs, and a type is identified with the proposition that it has a term (so that each of its terms is in turn a proof of the corresponding proposition).

… to show that a proposition is true in type theory corresponds to exhibiting an element “term” of the type corresponding to that proposition. We regard the elements of this type as evidence or witnesses that the proposition is true. (They are sometimes even called proofs… (from Homotopy Type Theory – Univalent Foundations of Mathematics, section 1.11)

…Accordingly, logical operations on propositions have immediate analogs on types. For instance logical ‘and’ corresponds to forming the product type A×B(a proof of A and a proof of B), the universal quantifier corresponds to dependent product, the existential quantifier to dependent sum. In classical mathematics, the law of double negation corresponds to a global choice operator.

• This answer is completely wrong, as usual with you and as I had explained already: but instead of retracting it, you cast doubts on and downvote mine with a pretext. Congratulations, you do get your diploma! -- I formally complain about your behaviour as well as that of the moderators in charge, who delete my comments instead of (also) fixing the situation, watching out for abuse and reverting abusive voting. Commented Jul 4 at 11:06