Re: [mizar] a term representing the extension of a type

[Jesse Alama <alama@stanford.edu>]

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> I think the problem is that the type "0-chain of p" does not
> syntactically widen to "Element of ..." . I checked just now, and it
> seems that non-emptiness is no longer a problem. So yes, this really
> has to be done syntactically in the (re)definition of "0-chain of"
> like
>
> mode 0-chain of p -> Element of foo means ....
>
> If it is e.g. just a proved theorem, Mizar will take no notice.

I see now, thanks.  If I choose to not redefine 0-chain of p, what
form should the theorem take?  My first guess is:

for x being 0-chain of p holds x is Element of <something>

Does that look right?

By the way, why does the use of the fraenkel operator require that my
term c of type 0-chain of p also have type `Element of X' for some
term X of type `non empty'?  Does the mizar logic become inconsistent
if we drop this general requirement on the use of the fraenkel
operator?

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*4: This inference is not accepted