[FOM] 'Salvaging' Voevodsky's talk

[William Tait]

Dear Martin,

I am going back to this earlier response of yours to Steve Awodey. 
 
> But, is it indeed true that you are working with system(s) that prove con(PA)?
> If so, Voevodsky's speculations are neither "interesting" nor "provocative", but merely misinformed.

I thought that I had answered this in an earlier message. But, since you do not seem to have understood what I wrote, let me state it again: 

It would be very hard to deny that there is a mathematical proof of Cons_{PA}. If that is not proved, then one would have to reject the proof of other Pi^0_1 propositions that are obtained in weak subsystems of second-order number theory. Lets just agree that that is unreasonable. 

I also think that it is just silly to think that Voevodsky would not agree with this.

But there is a meaning of "proving the consistency of PA" according to which it is not merely giving a "mathematical proof" of Cons_{PA}. For _as a proof of consistency of PA_,  a proof of Cons_{PA} may be (and in the event must be) circular: it may use (uses) at least the methods of proof whose consistency is in question. This, in essence, was Poincare's objection (1905) to Hilbert's early (1904) thoughts about proving consistency of axiomatic theories.

So the consistency problem is (was) to find some noncircular grounds for establishing Cons_{PA}. In the early 1920's Hilbert thought that he had a way around circularity: namely one would prove consistency of PA (qua axiomatic theory)  on the grounds of a quite different conception of mathematics than the axiomatic conception, namely one based upon intuition rather  than axioms. 

However one is to understand this, the program failed and one is left with the positive view that there is no possibility of a noncircular consistency proof of Cons_{PA}. 

Why not extend to Voevodsky the courtesy of assuming that this is what he meant?

With best regards, but some impatience,
Bill