[mizar] Re: mode definition/"the" question

[Jesse Alama <jesse.alama@gmail.com>]

On 2011-08-26 14:51:39 +0000, Adam Naumowicz said:

> On Fri, 26 Aug 2011, Artur Kornilowicz wrote:
>
> > Hence, having
> >
> > Lm2: the FOO1 is empty by DefFOO2;
> >
> > Mizar does not know how IT could be substituted - there is no term of 
> > type FOO2 around.
> >
> > The solution is to add a reference to a statement with a variable of 
> > type FOO2, for example:
> >
> > the FOO2 = the FOO2; then
> > Lm2: the FOO1 is empty by DefFOO2;
>
> This example shows that it might be useful to automatically add all the 
> global choice terms for the types occurring into the universe of 
> discourse. But the question is how useful it would be in general and 
> what would be the cost of the extra processing in the checker.

That sounds like a nice idea.  I agree it's not clear how useful that 
such a change would be.

I was able to think my way through the problem along the lines that 
Artur suggested.  Thanks.

I also found a different proof:

Lm0: the FOO2 is FOO2
    iff
    (the FOO1 is empty & the FOO2 is non empty) by DefFOO2;

the FOO1 is empty by Lm0;

I think I prefer Artur's approach to mine.

--
Jesse Alama
http://centria.di.fct.unl.pt/~alama/