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
