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

On Sat, 12 Jan 2008, Andrzej Trybulec wrote:

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

http://matwbn.icm.edu.pl/ksiazki/fm/fm32/fm32115.pdf (both papers are now 
linked from the wikipedia page at 
http://en.wikipedia.org/wiki/Tarski-Grothendieck_set_theory).

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

I agree that it should not depend on full TARSKI:9, but don't have time to 
investigate if AC was (perhaps even accidentally) used. I have the 
"recursive dependence" functionality implemented so far only for theorems, 
not for e.g. registrations and correctness of definitions (we should 
really do that - see 
http://mizar.uwb.edu.pl/forum/archive/0008/msg00000.html, eight years ago! 
.

Josef