Re: [mizar] [Thomas Forster] Re: [FOM] Historical Queries on AC

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

Jesse Alama wrote:

> Judging from Forster's reaction and questions that I've received from
> subscribers to the FOM mailing list concerning my post on TG, it looks
> like there's some surprise that Choice is a theorem of TG.  The surprise
> is that the universe axiom implies AC.  That was my intuition as well;
> those two don't seem to be related to each other.  Can anyone provide an
> intuitive sketch of why that follows?
>
>  
It is in Tarski's paper:

Alfred Tarski
On Well-ordered Subsets of any Set,
Fundamenta Mathematicae, vol.32 (1939), pp.176-183

Actually his goal was to prove that the existence of sufficiently large 
cardinals is enough to get Axiom of Choice, look to
the title of 1938 paper:

Alfred Tarski
Ueber unerreichbare Kardinalzahlen,
Fundamenta Mathematicae, vol.30 (1938), pp.68-89

When Tarski was accused that he can prove the Axiom of Choice only 
because of the specific form of Axiom A
(roughly speaking the existence of universal classes) then he had 
introduced  the Axioms B (existence of arbitrary large strongly 
inaccessible cardinals) and proved the _equivalence_ of both axioms (A 
and B).

I am in Nagano now, and my access to the literature is a bit restricted, 
could anybody look to 1939 paper?

However, I believe that the proof of the correctness of 'Rank' 
(CLASSES1:def 6) does not depend on TARSKI:9 (or ZFMISC_1:136, if you 
like), or it should not, and then the theorem

theorem :: CARD_LAR:37
 M is strongly_inaccessible implies Rank M is being_Tarski-Class;

does the trick. (Still, we have to look to references in the proof of 
CARD_LAR:37 - particularly to the references to the theorems in CLASSES1 
- if they are independent of TARSKI:9).

Josef, what you think, it is ypur article: CARD_LAR, so you know better.

Regards,
Andrzej