I was frustrated by my inability to get anything out of the brief writeup about Voevodsky’s univalent foundations in this month’s Notices. Fortunately, one of our graduate students, who has been reading the homotopy type theory book, has promised to explain it to me. I’m excited!
Already, hardly understanding anything, I have learned one interesting thing about type theory. (I haven’t yet learned anything about homotopy type theory.) It asks us to throw aside assertions like “P is true” as the basic objects of mathematical interest, and instead to concentrate on assertions like “p is a proof of P.”
In this context, what is conjunction? To say “x is a proof of P and Q” is to say that x is a pair (p,q) where p is a proof of P and q is a proof of Q.”
What is disjunction? In other words, what do we mean by “a proof of P or Q”? Well, there are two kinds of proofs of P or Q; there are proofs of P, and there are proofs of Q.
And this is why intuitionistic logic (which as I understand it is the kind of logic you get when you take this point of view seriously) rejects the law of the excluded middle. In the logic I know, you can just check from the truth table that (P or not-P) is always true, so (P or not-P) is the same thing as T.
But in type land, a proof of (P or not-P) must be either a proof of P or a proof of not-P. If neither of these is available, then there’s no proof of (P or not-P), so it can’t be the same as T.
I know in some sense this seems tautological — but I do find it rather striking as an illustration of an actual substantial difference between the two set-ups.
As Vladimir teaches me more, I’ll keep posting!
P.S.: by the way: in type theory, a proof of an implication “P implies Q” is a function from proofs of P to proofs of Q. (Or does it have to be an explicit algorithm that returns a proof of Q given a proof of P? I don’t know.) This is not the same as a proof of “not-P or Q”, which would have to be either a proof of not-P or a proof of Q, a completely different thing. So the logical account of implication I’m used to also dies!
On the other hand, a proof of Q is a proof of (not-P or Q). What’s more, if I have a proof q of Q, then the constant function sending every proof of P to q is a proof of (P implies Q).
I think the above paragraph is a correct proof in the type-theoretic sense of (Q implies (not-P or Q)) and also (Q implies (P implies Q)). What do you think?
(Note that I haven’t told you what a type is yet. That’s because I don’t know. I told you, I only understand one thing so far.)
Quomodocumque 