[FOM] Alternative Foundations/philosophical

henk henk at cs.ru.nl
Sun Mar 16 17:09:13 EDT 2014

Harvey asked:

In particular, I am interested in whether the following is true: 
Anything of general intellectually
interest ing foundational aim that you can achieve with alternative 
foundations you can achieve
better (more clearly, more generally understandable, more coherently, 
more powerfully, etc.)
with the usual foundations.

Now I happen to find interesting foundations that actually do represent 
By work of Gr\'egoire and Th\'ery a primality test has been fully 
represented in Coq.
As an example they actually formally proved (and checked this proof in 
Coq) that

2^{4223}-1 is a prime.

I claim you cannot achieve this (actual---not in 
principle---representation) in a system based on ZFC
(without having to rebuild this theory considerably).

Henk Barendregt

More information about the FOM mailing list