Re: [mizar] theorems of the form "if A then T", where A is known to be independent of TG

["Robert M. Solovay" <solovay@Math.Berkeley.EDU>]

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.

	--Bob Solovay