[FOM] Computational set theory

[henk]

Harvey wrote:
> Can't we simply prove outright that all formalisms, including ZFC with abbreviation power,
> represent large computations awkwardly?
No.

1. In Gonthier's full formalization (in Coq) of the 4CT a large 
computation has been fully
represented.

2. In the formal checking of primality of natural numbers with 44.000 
digits by
Gr\'egoire and Th\'ery the primality test has been fully represented in 
Coq.
As an example they formally proved (and checked this proof in Coq) that

-------------------------------
2^{4223}-1 is a prime.
-------------------------------

("Certifying large prime numbers: a purely functional library for 
modular arithmetic.")

Those that claim that representing computable functions can be done also 
in ZFC are right,
even in a nice way it can be done.
But then one has to introduce a functional programming language within 
ZF. And to run such a
program (of say an efficient primality test) one essentially needs to 
write a compiler, because
at the end one doesn't like to rely on someone else's software.

In a computational foundations one needs to state and prove

(i) \forall x in A.P(x, F(x))
(ii) F(a)=b, for a specific a in A

In (i) F is a representation of a program in the foundational theory and 
P is its
(partial) specification. In (ii) one uses this program.

Henk