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

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Freek:

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.

  

I am surprised, I recall a paper by Benjamin Werner in which he proved the equivalence of Coq and Tarski-Grothendieck.
It had been presented on a  conference in Sendai, maybe 1995.

I used to be on the FOM list. I am not now, I do not know why?  So, I cannot take part in the discussion. However, it seems
that the fact that MML is based on the TG set theory is not known to FOM volk

On the other hand I would like to cite a part of William Messing message:

  http://cs.nyu.edu/pipermail/fom/2007-December/012389.html

As someone who uses the "cohomological machine" in my everyday 
mathematics, I would personally prefer to state the Formalization Thesis 
in ZFC + Grothendieck's axioms for universes.  This because, as is well 
known and as I discussed in the thread concerning FLT, as soon as one is 
led to consider, for two categories C and D, the category HOM(C, D) 
whose objects are the functors F:C --> D and whose morphisms are the 
natural transformations between two such functors, size issues 
immediately come in to play.  Needless to say this is even more true if 
one looks at higher category theory, as is increasingly being done by 
topologists in connection with homotopy theory and stable homotopy theory.

As you see there is some support for TG.

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?

  

The Axioms of Choice is a theorem in TG.

Regards,
Andrzej