Re: [mizar]Possibly empty types

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

Dear Andrzej,

I now realize that the way I look at Mizar types is probably
very different from the way that you look at them, and that I
never made that explicit.  So let's do that now.

For you, I think, the Mizar logic is an extension of many
sorted logic.  So you have multiple sorts, and _also,_ as a
generalization they get parameters, they get widening, they
get attributes, etc. etc.

But for me it's not like that at all.  The Mizar logic is
_one_ sorted, because it's the language of set theory, which
is one sorted.

For me the "types" really are just predicates that the system
keeps track of for you.  So every mode M with n arguments, it
"really" is about a predicate is_M_of that has one left and n
right arguments, and _that_ is really what your are talking
about when you do Mizar.

For instance, to the mode

	Element of

corresponds, "internally", the predicate

	is_Element_of

(... which of course is almost, but not quite, entirely unlike
the predicate

	in

:-))

If you look at it like that, then that "explains" how to look
at the rule that you mentioned:

>>>             for x being Theta of X holds P[x]
>>>           ------------------------------------
>>>                     P[a]

So this "really" is about the deduction:

             for x being set st x is_Theta_of X holds P[x]
           ------------------------------------------------
                     P[a]

where the system deduces

	a is_Theta_of X

for you itself.  And of course, without x occurring in P[x]
and without any a, that is not a valid deduction.

If you look at the meaning of Mizar that way, you can see that
there is no worry whatsoever about the logic-with-possibly-
empty-types being meaningless or contradictory.

Freek