Re: [mizar] Once more: empty types

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

Dear Andrzej,

>The main cost when you allow possibly empty types is that
>you have no types :-)

Of course you still have types!  You mean: you do not have
_exactly_ the traditional logical rules anymore.

>That is the idea of soft types. They became syntactic 
>sugar. A bit more. You still can use them to reconstruct hidden 
>arguments and maybe to mimic other processing like widening.

... and all the other things that you use types for in Mizar.
You don't lose anything.  You just get that a few inference
rules become a tiny little bit different.

>To be more specific: no existential tautology. Particularly the 
>inference rule
>
>                   for x holds P[x]
>                   _________________     (1)
>
>                    ex x st P[x]
>
>does not hold.

That rule is not written by God on a stone or something.
You can have a perfectly usable logical system without
this rule.

>The inference rule (1) is a consequence of two rules
>
>                     for x holds P[x]
>                    ___________________     (2)
>                         P[tau]
>
>and
>
>                         P[tau]
>                     __________________     (3)
>
>                       ex x st P[x]
>
>
>so one of (2) or (3) must be invalid.

No, those rules _are_ valid.  The fact that you can write
a tau shows that the type is non empty.

>Let take typical example 'function from A to B', empty if
>B is empty but A is not. You can prove funny theorem
>
>        for A, B being set, f being Function of A,B
>             holds B = {} implies A = {}
>
>but it cannot be used to prove
>
>                B = {} implies A = {}

If this theorem is funny, then is

         for A, B, f being set st f in Funcs(A,B)
              holds B = {} implies A = {}
	
just as funny?  To me it's the same theorem.  (But the first
version allows one to write "f.x" while the second version
doesn't.  I _want to be able to write it in the first way._
While retaining the correct meaning.)  This statement should
not be considered funny, it should be provable.

And it _is_ provable!  Here is a trivial proof:

         for A, B being set, f being Function of A,B
              holds B = {} implies A = {}
         proof
           let A, B be set;
           let f be Function of A,B;
           assume A1: B = {};
           assume A <> {};
           then consider x being Element of A;
           f.x is Element of B;
           then f.x in B;
           hence contradiction by A1;
         end;

I don't see why this is funny.

(By the way the two steps that the current Mizar doesn't
like in this proof are "f.x is Element of B" from "f is
Function of A,B" and "x is Element of A", and "f.x in B"
from "f.x is Element of B".  To me _clearly_ if f is a
function from A to B and x is in A, then f.x is in B.
And _clearly_ if f.x is in B then in that case it is in B.)

(Also relprem says that the "then" in front of the consider
is not needed.  But it should!)

You are claiming that first order logic with possibly empty
sorts does not make sense.  That's just false.  It perfectly
makes sense.  It is just a tiny little bit non-standard.
And much better.

>I do not know if one can find more weird examples.

If you think that one is weird, then I'm sure you can.

>The logic we do in a non empty domain.

Traditionally first order logic one does in non empty
domains, yes.  But that's because it doesn't hurt there,
as the domain cannot do interesting things depending on
its parameters (there are none.)  In Mizar this situation
is very much different.

>I would like to have the same logic for restricted quantifiers.

So I would not :-)

Freek