[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] [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