On Fri, 4 Jan 2008, Robert M. Solovay wrote:
On Fri, 4 Jan 2008, Jesse Alama wrote:"Robert M. Solovay" <solovay@Math.Berkeley.EDU> writes:1) The existence of Mahlo cardinals is not provable in TG. 2) The existence of arbitraily large inaccessible cardinals is provable in TG.I was unable to find any proofs in the MML of these facts, so it looks like we have some nice candidates for theorems to go into the MML. Judging from mmlquery, the only article that seems to have anything to do with Mahlo cardinals is CARD_LAR, as Freek mentioned. And, by inspection, none of those theorems matches (1) above. Of course, that's what we would expect of mizar, since it is based on TG. What additional hypotheses are needed to prove (1)? (The proof can't go through in TG.)One can prove in Peano Arithmetic that "If TG is consistent, TG does not prove the existence of Mahlo cardinals". (A fortiori, the stated result is provable in TG.) The key observation, which is well-known, is that if there is a Mahlo cardinal there is an in accessible cardinal which is the supremum of the inaccessible cardinals which are less than it. (Throughout this and the previous letter, by "inaccessible" I mean "strongly inaccessible".)As Alama correctly observes, my claim 1) is not provable in TG since it entails the consistency of TG.
in CARD_LAR, there are proofs that (strongly)Mahlo is (strongly) inaccessible, and that strongly inaccessible is a model of ZF (that uses lots of work done by Grzegorz in some earlier articles)
Josef