[FOM] 'Salvaging' Voevodsky's talk

[Martin Davis]

Steven Awodey wrote:
 >As I said, the work going on in Homotopy Type Theory and Univalent
 >Foundations is entirely independent of the issue of the consistency of
 >PA.  Voevodsky's work on the homotopy theory of schemes also employs
 >methods that would prove con(PA) -- and nothing follows from that,
 >either.

What does follow is that this work does not 
provide an alternative foundation should PA turn 
out to be inconsistent. Unless I'm badly 
confused, it was Voevodsky himself who suggested that it did so.

 > ... I find it very  unfortunate that the FOM 
community is being made aware of these
 > interesting and important recent developments through the lens of this
 > irrelevant question about the consistency of PA.

I agree completely, but remark again that it was 
Voevodsky himself who introduced this "lens" as appropriate.

 >I urge readers of  this list to keep these things separate.

Again I agree. I think that it is wonderful that 
a mathematician of Voevodsky's scope, power, and 
status is interested in foundational issues. But 
experts like you who are working along his lines 
do, I believe, have a responsibility to help him 
on foundational matters where he seems 
uninformed. One such matter seems to have been 
his apparent belief that the systems whose 
promise he is investigating are immune to Gödel unprovability of consistency.

Best wishes,
Martin

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