[FOM] 'Salvaging' Voevodsky's talk

[William Tait]

Dear Martin,

> 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.

Warm regards,
Bill