[FOM] Alternative Foundations/philosophical

[henk]

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 
proofs.
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