Re: mode definition/"the" question

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/