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

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?
>
>  
>
I am so sorry. My previous message was an answer rather to Thomas 
Forster's question:

>You mean that if there is a proper class of strong inaccessibles then AC 
>follows..?   Surely you can't mean that!?!

Original proof of Tarski is formalised in WELLSET1. But the Grzegorz's proof (WELLORD2) is based on a quite
simple idea. Let U be a universe (CLASSES2), consider
     On U 
the set of all ordinal numbers in U, it does not belong to U, so U and On U are equipotent.
But On U is well-ordred, so U is well-ordered, too.

U is transitive, every set that belongs to U is well-ordered as well.

Regards,
Andrzej

>