Re: [mizar] non necessarily non empty types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

> > > > 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' :-)

OK, so more correctly, I should have said: 
"Hiding a part of a funny thing under a nice name ..."

I think that normal mathematical understanding is, that in such cases the 
antecedent (ZFM) is simply unnecesary, and adding it makes it ... - well, 
choose your word :-).

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

The two may overlap, GCH is closer, and Choice already influences (2) 
pretty much (especially in Mizar).
The related problem is that I sometimes do not know (and do not care for) 
the exact existence condition, or the proof is hard. I may know that the 
domain is non empty in many good cases, and do not like creating a 
special-purpose condition like: "assume that this thing exists".
The weak type is more natural for me.

Josef