[FOM] Mirna Dzamonja on an alleged "crisis" in foundations

[José Manuel Rodríguez Caballero]

The crisis in contemporary mathematics is not in its foundations, but in
accumulation of mistakes, because there are many papers and books, written
by important mathematicians, with mistakes and gaps. Some of these mistakes
are because of the use of the word "obvious". As Barkley Rosser said: if
Church says it is obvious, they've all noticed it for an hour; if Weyl says
it's obvious, von Neumann can prove it; if Lefschetz says it's obvious,
then it's fake.

The initial motivation of Voevodsky was to develop mathematics in a proof
assistant in order to avoid these mistakes. His own mistakes in homotopy
theory were his main motivation.

Which is the best type theory for a proof assistant in order to develop
mathematics? This is not a question about foundations of mathematics, but
about computer science. Therefore, I agree with Tim that HoTT has nothing
to do with a crisis in foundations of mathematics. The crisis exists, but
it is elsewhere.

Of course, proof assistants are related to foundations of mathematics,
because a proof assistant need its own foundation. Finally, I think that to
develop metamathematics in a proof assistant is not obvious at all, e.g.,
if I prove in a proof assistant, say using HoTT, that first order
arithmetic is consistent, what I really proved is that the consistency of
first order arithmetic is weaker than the consistency of my proof
assistant.

Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190305/6138afc4/attachment.html>