Intuistionistic logic and constructivism

The key insight of the Curry-Howard correspondence or the concept of 'propositions as types' is that there is a direct correspondence between logic and its operators and type theory and its operators.

This may at first seem strange and quite exotic (and it kind of is), but that's only because when one thinks of 'logic', it is most common -- by far -- to think of classical logic whereby every proposition (a statement which can be argued to be true or false) is assigned a truth value which mathematicians attempt to discover. A rather different logic is actually necessary to understand the Curry-Howard correspondence, namely: intuistionistic logic.

Intuitionism is the philosophical approach (in the philosophy of mathematics) whereby mathematical objects, including theorems and proofs are seen as human constructions instead of human discoveries. In other words, a group for instance is a lot more like a machine made up of pieces put together than Newton's second law of motion discovered based on empirical evidence of such law being respected in the Universe (there is obviously a lot more to be said about mathematics, technology, and physics, but for a layman in philosophy, this should get the point across).

In intuitionistic logic, propositions are not assigned truth values which are left to be 'discovered' by the mathematician, instead, propositions are said to have a proof or not have one (yet?). Roughly speaking, if a proposition has a proof, then it's true, and if it cannot have one, then it's false. However, it's unhealthy to think of intuistionistic logic as such because the ultimate goal of it is not to determine a truth value for a proposition, but instead to merely construct a proof of it.

A 'trivial' tautology has only one possible proof: that it just is a tautology, while a contradiction cannot have any proof at all. A slightly more elaborate proposition might have more than one proof. For example, proving an implication can be done by at least two ways: assuming the premise and deriving the conclusion, or composing other implications in a series; in general, this may lead us to 2 distinct proofs. This already gives more 'structure' to intuistionistic logic than is possible with classical logic, but more importantly, it allows for the expression of proofs as objects to be compiled and constructed.

The Curry-Howard correspondence

The Curry-Howard correspondence is a reformulation of intuistionistic logic within type theory. In essence, a proposition is to be read as a type, and a proof is to be read as an object of that type. Just as we can construct the type of natural numbers (below), we can construct proofs of a proposition.

Nat = Zero | (Succ Nat)

When a proposition has a proof, we say that the type is inhabited (there is at least one element of that type). Conversely, when no proof exists for a proposition, we say that the type is uninhabited.

Below is a table with some basic correspondences

Most texts on the subject never discuss much philosophy behind this or why it makes sense, so let's try to see why that is something you might like to invest yourself into.

Principally, one should realize that intuistionistic logic in type theory does not have propositions as its basic objects, but rather proofs. A proof is to be of a proposition, instead of a proposition having a proof. This also reflects a major conceptual distinction between type theory and set theory, an element is simply of a type, while a set merely contains elements with no type. Working with intuistionistic logic in type theory is about computing, combining, transforming proofs, not propositions.

From this perspective, a correct grouping of proof that makes sense is to consider proofs having the type of the proposition that they prove: if you can make a proof of B from some proof of A, you better be able to make one for any proof of A because if you're concluding B from A, then any proof of A should suffice. In general, anything that you can do with some proof of A must be doable with all proofs of A; therefore, it is best to say that your operations work on the type of proofs of A. Once you realize that, you realize also that the type of proofs of A corresponds directly to the proposition A itself, and you land on the Curry-Howard correspondence.