[FOM] 'Salvaging' Voevodsky's talk

[Steve Awodey]

 > 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


Dear Martin,

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.

The use of Martin L\"of type theory to directly formalize homotopy  
theory, and the resulting possibility of computational foundations for  
homotopy theory, and much more, represent an exciting new development  
in foundations, and Voevodsky's creative insights, mathematical  
sophistication, and dedicated hard work have already made huge  
contributions to the foundations of mathematics.  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 urge readers of  
this list to keep these things separate.

Best regards,

Steve