[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] 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