Re: mode definition/"the" question

On Thu, 25 Aug 2011, Jesse Alama wrote:

> Consider the vocabulary file
>
> ===== [ witness.voc ] =====
> MFOO1
> MFOO2
> ===========================
>
> and the article
>
> ===== [ witness.miz ] ===============================================
> environ
>
> vocabularies TARSKI, XBOOLE_0, WITNESS;
> notations TARSKI, XBOOLE_0;
> constructors TARSKI, XBOOLE_0;
> registrations XBOOLE_0;
> theorems TARSKI, XBOOLE_0;
>
> begin
>
> definition
> mode FOO1
> means :DefFOO1:
> ex y being set st it is empty & y is non empty;
> existence
> proof
>   A: the non empty set is non empty;
>   take the empty set;
>   thus thesis by A;
> end;
> end;
>
> definition
> mode FOO2
> means :DefFOO2:
> the FOO1 is empty & it is non empty;
> existence by DefFOO1;
> end;
>
> Lm1: the FOO1 is empty by DefFOO1;
> Lm2: the FOO1 is empty by DefFOO2;
> Lm3: ex x being set st the FOO1 is empty by DefFOO2;
> Lm4: ex x being set st the FOO1 is empty & x is non empty by DefFOO2;
> =====================================================================
>
> My puzzle is that the four theorems at the end are all flagged as *4.  I put 
> these statements in increasing level of surprisingness.  Any explanation for 
> why all of these are rejected by the checker?  (FWIW, I'm testing this on 
> mizar 7.12.01-4.166.1132, on darwin.)  I'm actually most interesed in why Lm2 
> is rejected, but all of these are a puzzle to me.
>
> Thanks,
>
> Jesse


Hi Jesse,

For every definition Mizar generates so called 'definitional theorem',
which in the case of FOO2 is

for IT being set holds IT is FOO2 iff
the FOO1 is empty & IT is non empty;

So, every reference to DefFOO2 is the reference to the above theorem.

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;

Other cases are similar.

Best regards
Artur