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

Re: [mizar] Re: AC and strongly inaccessible cardinals


Bob,

thanks a lot for digging into this thouroughly.

A couple of superficial remarks:
- The Mizar proof of AC from TG (i.e. ZF + existence of Tarski classes) by Grzegorz Bancerek seems worth mentioning for this, the link is: http://mmlquery.mizar.org/mml/4.100.1011/wellord2.html#T26
- A while ago, I also did small edits to http://en.wikipedia.org/wiki/Tarski-Grothendieck_set_theory reflecting the TG implies AC proof, someone could clarify that WP article wrt. these Tarski_class vs. Universe subtleties
- I am indeed guilty of allowing inaccessible (and even measurable) cardinals to be countable in Mizar. The reason why I did it is that I wanted to allow some example theorems (like aleph 0 is inaccessible) for debugging the definitions. It would be nice to blame also the Mizar type system, which makes work with nonempty types easier, but it was my first article, and I only gradually became aware of that problem. Also, limit cardinals had already been defined in Mizar to inlude 0 and aleph 0.
- I have worked in Mizar as in ZFC, and was not interested in additional TG issues. My goal in CARD_LAR was its final theorem (Rank of uncountable strongly inaccessible cardinal is a model of ZF: http://mmlquery.mizar.org/mml/4.100.1011/card_lar.html#T40), and I just wanted to re-use lots of previous Grzegorz's results (uncountable Universe is a model of ZF: http://mmlquery.mizar.org/mml/4.100.1011/zf_refle.html#T7). So CARD_LAR:37 and CARD_LAR:39 are quick hacks to get me there, not attempts to decide anything foundational.
- The references to Mizar proof items (like "A4") are not stable across various MML versions. For the recent MML (4.100.1011) the MML links are: 


	theorem :: CARD_LAR:37


http://mmlquery.mizar.org/mml/4.100.1011/card_lar.html#T37


	The proof of CARD_LAR:37 appeals
	to CARD_LAR:36 in the justification of the proof of claim A4.
this is now A6, this URL (after clicking on the proof of T37): http://mmlquery.mizar.org/mml/4.100.1011/card_lar.html#E4:52_2 


	In the proof of CARD_LAR:36


http://mmlquery.mizar.org/mml/4.100.1011/card_lar.html#T37


appeal is made to CARD_3:62 in the proof of claim  A9.


this is now A8, this URL (again after proof unpacking):
http://mmlquery.mizar.org/mml/4.100.1011/card_lar.html#E7:51


	In the proof of CARD_3:62


http://mmlquery.mizar.org/mml/4.100.1011/card_3.html#T62


	appeal is made to WELLORD2:26 in the proof of claim A6.
remained A6, URL after proof unpacking: http://mmlquery.mizar.org/mml/4.100.1011/card_3.html#E8:63 



	But WELLORD2:26 simply asserts that every set can be
	well-ordered which is well known to be an equivalent of the
	axiom of choice.
this is the Grzegorz's proof of AC mentioned above: http://mmlquery.mizar.org/mml/4.100.1011/wellord2.html#T26 



	Finally, here are the cites for the Mizar definition of
	"strongly inaccessible cardinal".


http://mmlquery.mizar.org/mml/4.100.1011/card_fil.html#V6


	The definition of "cardinal" and of "the cardinal of a set X"
	are give in the article CARD_1 and are thoroughly based on the
	axiom of choice.


http://mmlquery.mizar.org/mml/4.100.1011/card_1.html


	Cardinal exponetiation (the notation is exp(M,N)) is defined in
	the familiar way in CARD_2 as the cardinal number of the set
	of functions which map N to M.


http://mmlquery.mizar.org/mml/4.100.1011/card_2.html#K3


Josef