Re: [mizar] Once more: empty types

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Jesse Alama wrote:
> I would love MIZAR even more if types were allowed to be empty because
> it would make some formalizations more natural.
>
> What, though, are the costs?  I suppose that the developers would have
> to edit a good deal of code.  But, putting that issue aside, what would
> be the logical costs (if any) of allowing non-empty types?  Would there
> be some familiar logical steps that wouldn't "go through" if types were
> allowed to be empty?

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

I am serious. The only reasonable treatment of p.e. types is to 
eliminate them. 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.


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. (I assume that x is reserved for a p.e. type T).
With soft type it means

                    for x holds x is_T implies P[x]
                  ___________________________________

                      ex x st x is_T & P[x]

so obviously we need

                ex x st x is_T
to apply it.

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.

In Mizar it is the same rule:

                  for x holds P[x], for x holds not P[x]
               ___________________________________________

                       contradiction.

So both cannot be used. Not a big deal, you probably have no term tau
with type T, so the only possible application is when x does not occur
in P[x] and it is the case that Josef wrote about.

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 = {}

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

The logic we do in a non empty domain. I would like to have the same
logic for restricted quantifiers.

Regards,
Andrzej