Re: [mizar] non necessarily non empty types

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

I have changed the 'Subject'. In WTT (developed by Rob Nederpelt) 'weak types' means something
else.

Josef Urban wrote:

>
> > > ex M being Cardinal st M is_measurable implies
> > > for N being MeasurableCardinal holds N is inaccessible.
> >
> > Maybe you need:
> >
> >   pred ZFM means ex M being Cardinal st M is_measurable
> >
> > and then to use it as antecedent of the implication.
>
> Giving a funny thing a nice name does not make it less funny,
> provided one understands what is going on (and that should be the case).

What is 'the funny thing'?  'ex M being Cardinal st M is_measurable' :-)

BTW. Thomas Jech had advice me to use ZFM rather than TG (QED Workshop in ANL).

I believe that we have to distinguish two cases:
 (1) the existence of large cardinals or any additional axiom of the set theory
 (2) 'regular mathematics' like the problem with defining isomorphism.

In the first case I rather prefer to state explicitly
     ZFM implies X
if X is proved using the Axiom of Measurability
Similarly
     GCH implies ...
and so on. But of course we may introduce a directive in Mizar that says which axioms are
actually used.
(In fact I would like to stratify MML into the part depending on ZFC and needing TG, maybe we
should use even finer stratification)

Regards,
Andrzej