Re: [mizar] [Timothy Y. Chow] Re: [FOM] Formalization Thesis

[Freek Wiedijk <freek@cs.ru.nl>]

Josef:

>So if someone comes up with new super-cool foundations for
>math (and this is what various type-theorists tell us twice
>a day :-), we will very likely just translate the current
>corpus to it, do some serious debugging of the new (and old)
>formalism during the process, and continue formalizing.

Actually Mizar has stronger foundations than Coq, as Mizar
can prove the consistency of Coq.  So the translation of a
Mizar statement A to Coq sometimes would need to be something
like "some Mizar axioms imply A".  Not that this point
matters much in practice of course.

Personally I always worry about the choice operator, which is
implicitly present in Mizar.  I like foundations that don't
have that, but then how do you translate your formal
mathematics that implicitly is built on it?

Freek