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

[Freek Wiedijk <freek@cs.ru.nl>]

Jesse:

>Does the MML contain any statements of the form "if A then
>T", where A is a statement known to be independent of
>Tarski-Grothendieck set theory (TG)?

I would expect it to be easy to get something like that from
the theorems in CARD_LAR.  Existence of a Mahlo cardinal
isn't provable in Tarski-Grothendieck set theory, is it?

I always want to formalize Freiling's "proof" of the negation
of the continuum hypothesis.  Has that been done yet in MML?

Freek