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

[Jesse Alama <alama@stanford.edu>]

"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.)

Also, using mmlquery I found all the theorems and definitions that make
use of the attribute `strongly_inacessible' (see
http://mmlquery.mizar.org/mml/current/card_fil.html#V6 ) (or, in the
presence of GCH, `inacessible', see
http://mmlquery.mizar.org/mml/current/card_fil.html#T31).  None of the
theorems I found corresponds to statement (2) above.

Jesse

-- 
Jesse Alama (alama@stanford.edu)