Studying something related to Logic, I got wondered what a proof is. Learning Set Theory as the only foundation of Mathematics in high school or in college, I think it is a little natural to get confused. in Set theory, mathematical objects and logic are separated; we first define mathematical objects using some set of axioms then define a deductive system on top of them.
However, it seems unnatural to have the two separate layers; we can find ourselves often deal a proof of a certain lemma as some kind of object. Especially when we design an algorithm out of a proof, we certainly do deal the proof as an object that yields a function.
Program extraction is another field of study that requires much attention. However, in some sense, we all do program extraction; I think many of us have an experience of writing a program out of a mathematical proof. Let us consider a statement \(L\) and two proofs \(a, b\) of \(L\). The point is, seeing \(a\) and \(b\) as objects, whether we can say the proofs are different. Suppose a program designed from \(a\) takes \(n^3\) and a program designed from \(b\) takes \(exp(n)\) (whatever the \(n\) is). Then, why can’t we say the two proofs are different? If a proof is not an object, how can we say that two proofs are different?
Type theory can be thought as an alternative foundation of mathematics that merges the separation: objects and proofs. Although there are different aspects of seeing Type Theory; e.g., a foundation of constructive mathematics. I think the aspect of ‘proof as object’ is the most ‘touching’ one.
There are many things to talk about in Type Theory. However, to be focused on the spirit of ‘proof as object’, let us see a simple example. Suppose we have two objects \(a\) and \(b\). We want to argue whether the two objects are the same. In Set Theory, \(a\) and \(b\) are some objects that may live in some set \(S\). The proof of the statement \(a = b\) will be constructed following some rules in a deductive system which live outside of the object construction.
In Type Theory, given two elements \(a, b : T\) (it says \(a\) and \(b\) of type \(T\)), the statement \(a = b\) is also a type. We call it an equality (or identity) type of \(T\) and \(a, b\). A proof of \(a = b\) is an element of the equality type. Hence, the proof \(p : a = b\) itself is a mathematical object just like \(a\) and \(b\) are. Hence, the statement reads, ‘given two elements \(a, b\) of type \(T\), can you find an element of type \(a = b\)?’
Seeing a proof \(p : a = b\) as an object, we can imagine the following: given \(p, q : a = b\), arguing \(p = q\) is again a type. Yes, we can have \(r, s : p = q\) and again argue whether \(r = s\) and so on… This observation leads the attention to Homotopy Type Theory, which is not the topic here; however, is surely interesting.
The equality type is a fundamental type former in Type Theory; given a type and two elements of it, it returns a type. Similarly, there are other type formers which enable us to have counterparts of product, co-product, existential and universal quantifiers. Maybe introducing \(\Sigma\) and \(\Pi\) dependent types in Martin-Löf dependent type theory would be an interesting topic for the next posting?