[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] I am trying to figure out...

Cytowanie freek <freek@cs.ru.nl>:

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