Re: I am trying to figure out...

Cytowanie freek <[email protected]>:
>> Mizar does not allow for meaningless types like
>>
>>    an empty non empty set
>>    an element of the empty set
>>    a function from a non empty set into the empty set
>
> I disagree that they're meaningless!  They're just empty.
A rose by any other name ...
> Is the empty _set_ a meaningless _set?_  No, of course it
> isn't.  And likewise an empty type is not a meaningless type.

The empty set has quite precise meaning. And what is

   the empty non empty set?
>
> In Coq I can do

Why we should mimic Coq?

>>
>>       x is element of A
>>
>> and    x in A?
>
> For the same reasons that one now has types in Mizar:
>
>     1. to have the system automatically infer that certain
>        predicates hold (using the types in definitions
>        and registrations)
>
>     2. to disambiguate overloaded syntax
>

OK It is a valid argument.

>> However we need arguments to change it, not to keep it
>> as it is. I do not claim that it is not possible that we
>> eventually find such arguments.
>
> For me the argument is that the types can have much more
> natural defintions.  Now, often when I want to define a
> type, Mizar won't allow me to write what should be there,
> and then I just give up.
>

You can always use a permissive definition. Like we do with

   Element of ...
or
   Function of ..., ...

So, actually it is a technicality.

>
>> The problem is that it is difficult to anticipate the
>> consequences of changing the approach.
>

I ment something like this:

In checker to get the contradiction between a universal formula we
remove quatifiers and substitute for bound variables free variables.

Than we try to find a substitution for free variables that contradicts 
the other premises.

If we allow for types with the empty denotation, then we should 
additionally check if all free variables have non empty types. Quite 
unnnatural, isn't it?

In general we cannot infer

       for x being theta holds alfa
       -------------------------------
             alfa

when x does not occur in alfa

I guess that in Coq such inferences are not allowed in general.

It means that we cannot remove fictitious quantifiers.


> We've had this discussion before, I'm sure.  My excuses
> for being triggered.


No problem, we get better understanding the different approaches. I 
appreciate it.

Regards,
Andrzej