On Mon, 31 Dec 2007, Freek Wiedijk wrote:
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?
There are two problems: The first is when given new cool foundations which allegedly capture "all the old stuff", translate the old stuff to the new foundations. That's just a test of the claim that the new foundations are so cool, and that they can deal with anything the old foundations dealt with.
The second problem is that the formalisms and proofs might really be different. If I use choice for something which does not need it, just because it is convenient (and I don't care anyway), I really end up with a different proof. The same e.g. with constructive proofs. In some cases there may be an algorithm transforming the old proofs to new (e.g. constructive, without-choice, etc.) proofs, but in other cases your formalism really forces you to come up with a whole new proof (or realize that there is none), creating (and possibly formalizing) new mathematics.
Josef