Re: [mizar]Possibly empty types

[Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>]

Dear Freek,

Freek Wiedijk wrote:

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.

  

So, let us better use "possibly empty types". In any message to a type construction systems mailing list I will call Mizar types "non empty types" (I would would like "strong', but ...), I promise.

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

  

Interesting.

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!

  

No, not in the sense of Rob and Fairouz. The point is if you want "apparent possibly non empty types" like
'Isomorphism of G,H' above (when the actual type is 'Homomorphism of G,H') or you want to have
'intrinsic possibly empty type'.

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.

  

I want. :-)
Maybe I will change the opinion, but as yet I want.

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.

  

No, he wrote about regular, 1-sorted logic. What I mean that typed quantifiers (with parameters or not) might be thought as a restriction of the domain (actually it is chosen semantics in Mizar). So when all quantifiers are typed in the same way you got the logic restricted to the denotation of the type, and I believe it should be the same logic as for the type set.

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!
  

It might the problem. It is not.

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;
  

One of possible valuation of x,y is 0, 1, and 1/(0-1) = -1 definitely exists. Well, the first assumption is false.
So what, we quite often use false assumptions.

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

  

Of course when I say that the 'term exists' I mean that it has a meaning. I suppose you too.

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

  

I assume  that you can construct a term 'a' with type Theta. If you cannot , at least in a consistent context,
that is OK with me. So, the crucial question:
do you want to allow ground terms that have empty type?

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

  

It is not what I was writing above. The fictitious bound variables are allowed in Mizar, it rather problem of
maintenance of MML. However they are removed in the CHECKER, that of course cannot be allowed
if types may be empty.

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.

  

Again, "a" with empty type?

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.

  

You are probably right, that it is more natural. But also less useful.

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!"

  

I sort of understand what you write. The problem is that I believe that CH is true :-)

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

  

What is the problem with an empty set? Of course there are non empty sets, too. E.g.
 {{}}, { {}, {{}} }

 However you right, some people have problems. If I recall Bertrand Russel argued that
"the empty set of ducks" and "the empty set of geese" are the same. If he argued, the I suppose
somebody had a different opinion.

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

  

Not at all. It shows that sometimes breaking permissiveness might be more practical, even if
less natural, than keeping to permissiveness.

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

  

A logical equivalent, but semantic correlates are different.

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.

  

A bold claim.

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

  

"A horror! "
But after some explanations:
"let us suppose that we have real, mathematical
        'element of ...'
whatever it means. Then we may define an unorthodox
         Element of X :
                   element of X if X <> {}
                   {} otherwise
According our experience in Mizar the second is more useful"
The answer may be:
"If you say so"

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 happens. But it is stupid, isn't it?

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

  

Yes, 'x is_element_of {}' is meaningful, no problem with predicates.

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!

  

S, what I have written was obscure. I meant that some mathematician claim, against the logic, that the sentence
                for x being element of {} holds x = x
is false. Even if they agree that, according to logic,  the sentence
               for x being set st x in {} holds x = x
is true.

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.

  

 I have a feeling that we made a progress.
At least I think that I understand now a bit better what is the logic of empty types.

Regards,
Andrzej