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

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

Dear Andrzej,

>I am surprised, I recall a paper by Benjamin Werner
>in which he proved the equivalence of Coq and Tarski-
>Grothendieck.

Really?  I always thought that Coq only had countably many
universes, while Mizar has arbitrarily large ones.

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

I wasn't talking about AC.  (Who would want to do mathematics
without AC?)  I was talking about a choice _operator._  So
a functor that given a non empty set gives you an element
of that set.  In Mizar one can define such a functor (as
you taught me):

  environ
   vocabularies NEWTON;
   notations XBOOLE_0, SUBSET_1;
   constructors TARSKI, SUBSET_1;
   registrations XBOOLE_0;
   requirements BOOLE, SUBSET;

  begin
   reserve X for non empty set;

  definition
   let X such that A1: contradiction;
   func choose X -> Element of X means contradiction;
   correctness by A1;
  end;

  theorem choose X in X;

AC just states that there _exists_ a choice function,
but a choice operator actually allows you to define one.
That is much stronger.  (And too strong to my taste.)

Freek