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 and two proofs of . The point is, seeing and as objects, whether we can say the proofs are different. Suppose a program designed from takes and a program designed from takes (whatever the 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 and . We want to argue whether the two objects are the same. In Set Theory, and are some objects that may live in some set . The proof of the statement will be constructed following some rules in a deductive system which live outside of the object construction.
In Type Theory, given two elements (it says and of type ), the statement is also a type. We call it an equality (or identity) type of and . A proof of is an element of the equality type. Hence, the proof itself is a mathematical object just like and are. Hence, the statement reads, ‘given two elements of type , can you find an element of type ?’
Seeing a proof as an object, we can imagine the following: given , arguing is again a type. Yes, we can have and again argue whether 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 and dependent types in Martin-Löf dependent type theory would be an interesting topic for the next posting?