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

[Jesse Alama <alama@stanford.edu>]

Freek Wiedijk <freek@cs.ru.nl> writes:

>>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'm afraid I don't know enough about TG to answer the question.
Andrzej?

>From what I understand, TG is equivalent to ZFC + "there exist
infinitely many strongly inacessible cardinals".  Yet I can't seem to
find a proof in the MML of "there exist infinitely many strongly
inaccessible cardinals".  The leads me to question my judgment: is that
statement actually a theorem of TG?  And, if so, is it in the MML?  If
not, it would be nice to see it there.

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

To my knowledge, it is not already in the MML.  What's the logical
structure of Freiling's claim?  There must be some hypothesis
independent of ZFC contained within it somewhere.  In any case,
Freiling's result would be a nice addition to the MML.

Jesse

-- 
Jesse Alama (alama@stanford.edu)