[FOM] foundations meeting/FOMUS/discussion

[Louis Garde]

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>