[FOM] foundations meeting/FOMUS/discussion
Louis Garde
louis.garde at free.fr
Sat Mar 26 02:56:24 EDT 2016
Le 26/03/2016 02:53, Joe Shipman a écrit :
> Let's make this extremely concrete. I am going to pick two very
> well-known theorems of different levels of difficulty. Can people who
> think HoTT is a useful "alternative foundation" for mathematics please
> say whether or not
>
> (1) the Prime Number Theorem can be rigorously proved using
> foundations involving HoTT and no set theory without significantly
> more effort than the standard development requires, counting effort
> "from the ground up"
>
> (2) the Fundamental Theorem of Algebra can be rigorously proved using
> foundations involving HoTT and no set theory without significantly
> more effort than the standard development requires, counting effort
> "from the ground up"
Le 26/03/2016 00:39, Martin Davis a écrit :
> In the ongoing discussion here on FOM, I don't think the distinction
> has always been made between a foundation suitable as the starting
> point of metamathematical investigations, and one suited for use in a
> computerized proof verification system for use by mathematicians in
> certifying the correctness of their work.
If you understand "foundation" as the framework language in which you
are doing your daily mathematical work, there is no doubt that set
theory is sometimes simpler and more efficient than HoTT - and vice-versa !
In computer science, you select - or even design - your computing
language so that it best fits what you want to do with it. I expect that
the same holds for mathematics: many different mathematical languages
can co-exist, and this is just fine. Nobody is saying that set theory
should be dismissed and replaced with HoTT, no set-theoretic proof
becomes wrong or inacceptable in HoTT. HoTT just brings a different
point of view that is worth knowing, you are then free to decide when to
use it or not for your daily work.
From the "philosophical" or "metamathematical" point of view, the
treatment of logical consequence as a function is a key concept that you
have in HoTT, but not in classical set theory.
Therefore from this point of view HoTT is, I think, an enrichment of set
theory.
Louis.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160326/46ab1c40/attachment-0001.html>
More information about the FOM
mailing list