Re: [mizar] Weak types

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

Dear Andrzej,

>I do not know if the subject is right because it seems
>nothing to do with 'weak types' of Fairouz .

You are right, the "weak types" of Rob Nederpelt and, yes,
Fairouz Kamareddine, are something differently entirely.

I used the term because I couldn't think of a better one, and
because Josef was using this one.  What I mean is "possibly
empty type".  Actually for me the non-weak types (strong
types?) are the strange ones really, they are the ones that
should have a special adjective.

It would be very interesting to know how type theorists look
at our discussion (probably they would think that we both are
crazy :-))  For them possibly empty types are utterly normal.
In fact without them, the Curry-de Bruijn-Howard isomorphism
wouldn't work (every statement would be true, because the type
of the proofs of that statement would always be non-empty.)

>I would like to be more precise what we talk about. It looks
>to me that the whole problem is that you (and Josef and maybe
>some others) what to be allowed to write
>
>     for h being Isomorphism of G,H holds ...
>
>instead of
>  
>    for h being Homomorphism of G,H st h is_an_isomorphism_of G,H holds

Yes, for example!  And

    let h be Isomorphism of G,H;

instead of

    let h be Homomorphism of G,H;
    assume h is_an_isomorphism_of G,H;

>Or you really want weak types?

In the sense of Rob and Fairouz?  No!

>The controversy is well known in logic. E.g. Andrzej
>Grzegorczyk in his 'Logika matematyczna' argues (I have not
>his book here, so take it cum grano salis) that logic should
>deal with formulas valid in non empty domain.

But does he address the issue of _dependent_ domains, where
the domain is dependent on a parameter?  I can imagine that
having a type that is empty no matter what the arguments are
is a bit silly.  But I want types that sometimes are empty and
sometimes are not empty, depending on the parameters.

In HOL one also doesn't have "weak types" either.  But _there_
I don't have a big problem with it, as _there_ the type system
is so weak that it doesn't hurt me.  However, once one has
dependent types in the system, like you have in Mizar (and
like one has in type theory, for that matter), really you
don't want to restrict yourself to types that have to be
non-empty no matter what the argument turns out to be.

>So, if we treat types as a mean to restrict the domain they
>should be non empty.

I would expect Grzegorczyk only was talking about many sorted
logic without parameters to the sorts.  In that case I don't
think I would object to what he's writing.

>If introducing weak types resulted in the faster growth of MLL,

Well, introducing mode definitions _would_ be a lot easier.
Just make it into an "weak" mode, and then there is no need to
do all the work that you generally have to do to prove the
inhabitation of the type.  Similarly you could skip proving
all those tiresome clusters until you really need to establish
non-emptyness of the relevant type to make a specific proof work.

(Of course you will claim that it would lower the _quality_ of
MML, if people would do that.  But it would grow! :-))

>I tried the introspection and I think that the main reason
>that I do not want weak types is that the texts when we are
>using them become so obscure.

I don't see why.  In Coq types don't have to be empty, and
_that_ is not a reason that Coq texts are obscure.  (Just in
case someone from the Coq community is reading this: please
note that the type of "reasons that Coq texts are obscure"
might very well be empty :-))

>If I have no problem with
>    for x being element of A holds ...
>(I use 'element' for weak type) if A is empty, the I am rather reluctant 
>to write
>    let x be element of A;
>in such a case.

But are you reluctant to write

    let x be set such that x in A;

It's exactly the same.  _Exactly_ the same!

>I am not certain if I understand the impact of weak types on
>the natural deduction.

One would need to be very careful there, I agree.  But I don't
think it's impossible to get it right, and it would be a huge
improvement.

>Anyway, I do not like the idea of local constants with an
>empty type.

But do you like reasoning in under a false assumption?  Again,
it's exactly the same kind of thing.

>And I definitely do not like the idea of ground terms that do
>not exist.

If I reason

    let x, y be Real;
    assume x > y;
    assume y > x + 1;

and I'm talking about a "ground term" 1/(x - y), then that
ground term doesn't exist either.

>The rule dictum de omni is not valid anymore, to use
>               for x being Theta holds P[x]
>             ------------------------------------
>                       P[a]
>I have to prove 'ex x st x is Theta' or something like this.

Only if the "x" doesn't actually occur in the "P[x]" (because
else the "a" would be a witness for the existential statement.)

But then what's the point of having the "for x" in the first
place if it the "x" doesn't occur in the "P[x]".  Maybe we
should restrict Mizar in such a way that writing down formulas
in which a "for" is not allowed when the variable doesn't
occur in the body under it?  (That is a restriction that would
be just as silly and irritating as this "non empty types"
restriction.)

>So what the use we have for universal sentences if we cannot
>use them :-)

But you can use them!  You just need to come up with an "a"
for this rule, even when the "x" is not in the "P[x]".  That's
not _so_ strange.

>Still when we use 'Morphism of o1,o2' we should know that the
>corresponding hom set is non empty.

Why?

I also want to write "Function of X,Y" when X is non empty but
Y is (let's call it "function of X,Y" with a small "f" :-))
Why should that be forbidden?  It just makes everything much
more natural to have the "Function of" type be allowed for all
X and Y, and have it be empty in that specific case.

>When I look the formalization of the category theory in Coq I
>feel like in a realm of ghosts: what is real and when we are
>taking about nothing?  But of course it is my feeling, or a
>prejudice.

Yes, it's a prejudice :-)

When you're reasoning from an assumption like the continuum
hypothesis, (so you're proving a statement of the shape "CH
implies ...") you're in the same realm of ghosts.  But
_nothing_ in Mizar prevents you from doing that.  I someone
does that you _don't_ say: "Aha!  If you want to reason from
CH, then you first need to show that CH holds!  Because if it
cannot be shown to hold, then why would you be allowed to have
it as an assumption?  You're reasoning in a realm of ghosts!"

When you talk about the empty set, do you also feel like
you're in this realm of ghost?  "How can a set be _there,_
when there's nothing in it?  It has no substance!"  (I'm sure
that there are people who feel like that.  But it's nonsense.)

>>Ah.  I understand, I think.  It would mean that "Element of"
>>really should be defined in the following way:
>>
>> definition let X be set;
>>  assume
>> Z: X is non empty;
>>  mode Element of X -> set means
>> :Def1: it in X;
>>  existence by Z,XBOOLE_0:def 1;
>> end;

>It is the original definition. Afterwards we learned that
>breaking the permissiveness makes life much easier.

That shows that using permissive definitions is not a good
alternative to having proper "weak types" (in Josef's sense.)

>I think that the predicate 'meaningfulness_of_Element_for X'
>is rather
>	  ex IT being set st IT in X

That _is_ equivalent to "X is non empty", isn't it? :-)

>>But even this is crazy!  "Element of {}" is a perfectly
>>natural thing to write,
>
>It is natural for whom?

For many people.  For me.  For Josef, I would expect.  For all
people who do type theory.  For de Bruijn, I'm certain.  For a
lot of at least moderately clever people.

>I believe that a regular mathematician would say 'what you
>are talking about?'.

And if you show them that in Mizar you can prove that "{} is
Element of {}", then they _won't_ say that? :-)

It would be like you are reasoning by contradiction, and
saying "okay, let's assume so-and-so" and then someone who is
listening to your proof interrupting you with, "What are you
talking about?  You are trying to show that that isn't the
case!  So you can't assume that!  Because it is false!"

>It is of course a criticism of Mizar, too. The IMPS logic is
>closer to mathematical practice,

I don't think that this has anything to do with partial logic,
which is what the IMPS logic is about (among many other
interesting aspects), and which I think you are talking about
here.

The logic of type theory is very much a total logic, so it
doesn't handle partiality (the thing that IMPS adresses) well
at all.  But type theory has _no_ problems with empty types
whatsoever.

>Mathematician quite often treat a meaningless sentences as
>false

But "x is element of {}" (with the small "e") is _not_
meaningless at all.  It is false, but not because we _treat_
it as such.  Because it _is._

It is just as meaningless as "x in {}", which also is not
meaningless at all (but also just false).

>So maybe some mathematicians would claim that
>        for x being element of {} holds x = x
>is false, against the logic.

Then they would also have to say that

    for x being set st x in {} holds x = x

would be against logic!

>So, I think a natural reaction to the sentence
>       for h being Isomorphism of G,H holds ....
>is rather:  how do you know that G,H are_isomorphic?
>However, the mathematical language is so sloppy. Maybe it is
>assumed by default that G,H are isomorphic.

Yes, it is assumed, no matter what "h" is.  But only _inside_
the "for"!

Josef is right, there's really no point in arguing about this
again and again.  But I can't stop myself, I feel too strongly
about this!  Mizar is such a nice system, I want to be able to
like it.  And this point really is one of the main things that
is in the way of that.

Freek