Re: [mizar] weak types

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

Removing the fictitious variables is a comparatively new feature, and I
hope that
we remove the removing.

Let us look what the UNIFIER (the third pass of the CHECKER, the name is
no good
because it is rather pattern matching) does.

It chooses the main premise (a universal sentence), goes to atomic  (or
existential) sentences, finds the list of substitutions that contradict
them and
then goes to the root joining (for a conjunction) or merging (for a
disjunction)
list of substitutions. In that way, when it reaches the root, and the
resulting
list is non empty, it is a contradiction. The precise definition: look to
SUBSTLAT
and HEYTING2 articles by Adam Grabowski.

( Maybe I should remind (not Josef or Freek) that CHECKER is a disprover,
to check
an inference of the form
     P_1, ...,P_k   |-   Q
it adds 'not Q' to premises and looks for the contradiction. )

So, the quantifiers are ignored. If you have as a premise
       for x being S, y be T holds P[x]
you may infer P[a]. If T was empty, the sentence above would be true for
any P[.].
It is basically the same as
Freek's example. Is it a deeper reason?

The typical way to cope with the situation is to use permissiveness

 definition let G,H be Group such that
A: G,H are_isomorphic;
   mode Isomorphism of G,H means
    .....;
   existence by A;
 end;

You may look to NATTRA_1 to see how it is used to introduce e.g. mode
    natural_transformation of F1,F2
between functors F1 and F2.

Andrzej


Josef Urban wrote:

> Hi Freek,
>
> > Also, you don't get anymore from "for x holds P[]" (where x
> > doesn't occur in P[]) that "P[]" itself has to hold.
>
> Yes, this is now hard-wired at least in the checker (removing fictitious
> variables).
>
> > >Or is there any deeper reason for avoiding them?
> >
> > It would be surprising.  PVS and Coq and NuPRL all support
> > types that can be empty.
>

.....

> On the other hand, maybe that the removing of fictitious variables is
the
> only hard-wired obstacle, so in that case a straightforward
> reimplementation might be even cheaper (and cleaner).