[FOM] 'Salvaging' Voevodsky's talk

[Martin Davis]

Bill Tait wrote:
 >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?

Dear Bill,

I apologize for anything I may have written that gave you the 
impression that I didn't perfectly well understand the situation 
regarding consistency proofs as you described it (and as I had been 
teaching it for decades).

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). He also 
suggested that serious efforts to prove the inconsistency of PA are worthwhile.

Of course I am happy to grant Voevodsky every courtesy, and as I have 
written, I am delighted that he chooses to work on foundational issues.

With warm regards, and just a little impatience as well,
Martin

Martin Davis
Professor Emeritus, Courant-NYU
Visiting Scholar, UC Berkeley
eipye + 1 = 0