[FOM] 'Salvaging' Voevodsky's talk

[joeshipman at aol.com]

What does Francis Sergeraert think of this work in computable homotopy 
theory?

His groundbreaking work in this area in the 90's was very unfairly 
disparaged by the Algebraic Topology community because they were 
ignorant of the foundational issues related to computation to a similar 
degree as Voevodsky seems ignorant of the foundational issues related 
to consistency.

-- JS


-----Original Message-----
From: Steve Awodey <awodey at cmu.edu>
To: fom at cs.nyu.edu
Sent: Wed, Jun 8, 2011 1:35 pm
Subject: Re: [FOM] 'Salvaging' Voevodsky's talk


> 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 
_______________________________________________ 
FOM mailing list 
FOM at cs.nyu.edu 
http://www.cs.nyu.edu/mailman/listinfo/fom