[mizar] Revising UPROOTS: Global Choine

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

In his excellent analysis of inaccessible cardinals in Mizar prof. Solovay
complained that it cannot be done inside Mizar, because of the
Axiom of Choice.

I had proposed TG as the axiomatics mostly because it allows for
a proper development of category theory. But the fact that in it
we can prove AC was a little bit more than just a bonus.

The proof of AC was done twice in MML
i. by Nowak & Bialecki, following the original proof of Tarski
   (WELLSET1)
ii. by Bancerek, the proof similar to the one in Morse-Kelley set theory:
    using the fact that the set of all ordinals in a Tarski class
      has the same cardinality as the class itself. Tarski's Axiom A
      is related to the Size Axiom in MK
   (WELLORD2)

Then Rudnicki introduced an absolutely permissive functor

 let S be set;
 assume
Z:  contradiction;
 func choose S -> Element of S means
  not contradiction;
 correctness by Z;

(now in SUBSET_1)

and it became obvious that, using the Replacement, we can prove AC in MML
without Tarski's Axioms A.

Actually we may consider a generic definition

 let ... ;
 assume
Z: contradiction;
   func the \mi of ... -> \mi of ... means
    not contradiction;
 correctness by Z;

for an arbitrary mode \mi.

It cannot be formulated in Mizar, but we can formulate all
instances of it.

In the most recent version of Mizar (7.10.01) this generic definition is 
built-in (implemented by Czeslaw Bylinski).
So, for arbitrary type \theta we can use the term

             the \theta

The only fact about it that Mizar knows is:

             the \theta is \theta.

I guess it can be called Global Choice (Mizar types mimic classes).

It is already used in XBOOLE_0

 func {} -> set equals
 the empty set;

and in SUBSET_1:

 let S be set;
 func choose S -> Element of S equals
  the Element of S;

Recently I observed that it can also be used for the definition
of the 'canFS' functor in UPROOTS:

 let A be finite set;
 func canFS(A) -> FinSequence of A equals
  the bijective FinSequence of A;

The original definition is rather complicated:

 let A be finite set;
 func canFS(A) -> FinSequence of A means
 len it = card A &
 ex f being FinSequence st len f = card A &
 (f.1 = [choose A, A \ {choose A}] or card A = 0) &
 (for i being Element of NAT st 1 <= i & i < card A for x being set
 st f.i = x holds f.(i+1) = [choose x`2, x`2 \ {choose x`2}]) &
 for i being Element of NAT st i in dom it holds it.i = (f.i)`1;

But the work done by the Authors of UPROOTS is not completely wasted. The
new definition needs the registration

 let A be finite set;
 cluster bijective FinSequence of A;

and to prove the existence condition of the registration I have copied
and simplified the proof of the existence condition of
the original definition and the prove of

theorem :: UPROOTS:5
 for A being finite set holds rng canFS(A) = A;

We also need that the FinSequence is one-to-one, but it
can be justified using the Pigeon Hole Principle (FINSEQ_4:77),
that the Authors of UPROOTS had not noticed.
There is a gain: the article gets shorter by more that 200 lines.

The original definition is used only to state that

for A being finite set holds len canFS A = card A;

So, after the revision it should be a theorem. It can be proved in two lines,
again using FINSEQ_4:77.

Regards,
Andrzej Trybulec