[FOM] 'Salvaging' Voevodsky's talk

[Martin Davis]

Steve Awodey writes:

 >as someone involved in the development of the homotopical interpretation
 >of constructive type theory and the univalent foundations program, I would
 >like to point out that this program is independent of Vladimir's
 >provocative speculations regarding the consistency of PA -- as interesting
 >as those may be.

Dear Steve,

I'm pleased that you are finding this work worthwhile and I look 
forward to see what will emerge from this effort.

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.

Best wishes,
Martin


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