[FOM] 'Salvaging' Voevodsky's talk
martin at eipye.com
Wed Jun 8 18:25:43 EDT 2011
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,
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.
Professor Emeritus, Courant-NYU
Visiting Scholar, UC Berkeley
eipye + 1 = 0
More information about the FOM