[FOM] 'Salvaging' Voevodsky's talk
williamtait at mac.com
Thu Jun 9 12:28:55 EDT 2011
> What I have been trying to say over and over again is that Voevodsky has implied that his foundational views could provide a way out should PA be found to be inconsistent. And that this is silly given the now admitted fact that his systems prove con(PA).
I think his idea of a 'way out' is wrong, but not as silly as you make out. Surely he knew from the beginning that the Martin-Löf type theory, as it has always been formulated, includes PA.
I understand him to be saying the following: PA is just a formal system and if it is inconsistent, then none of its formal deductions are reliable: false things can be proved without an explicit inconsistency appearing. He wants to say that this will not happen in type theory: the 'proofs' of a sentence \phi in type theory are not just strings of symbols, but are objects of type \phi that we actually construct and we can check that we have made a proper construction of such an object (a pair, a function, etc.). So even if there is an inconsistency in the large, individual proofs in type theory can be checked for reliability. For example, to see that a particular term (proof) t of type \forall x \phi(x) really yields a function of that type, one need 'only' to show that tn computes to an object of type \phi(n) for each number n.
Again, I am certainly not endorsing this idea, but I don't think it is quite silly.
> He also suggested that serious efforts to prove the inconsistency of PA are worthwhile.
I don't think that this is relevant to the issue that we have been discussing; but I do hope that all such efforts fail!
Finally, Martin, please excuse my previous petulance.
More information about the FOM