Re: [mizar] Calculus in CQC_THE1

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Dear Patrick,

I did not have time to have a look at the problem you ask about, I just 
noticed that in your article, you often state theorems about 
"reconsidered variables".
Unfortunately, this is just another undocumented and uncontrolled trap in 
Mizar, you get into your theorems what Mizarians call "local constants", 
and such theorems are either unusable or causing things like segmentation 
faults when used in other articles.
The solution is either not to export the propositions (not to use 
"theorem"), or use in them only "reserve"-d variables. "Variables" given 
by "set", like your "set x = [4,0];" are also OK, if the right hand side 
does not contain the "local constants" - they are just macros which are 
expanded (but if you "reconsider" them, they are not).

Best,
Josef


On Fri, 16 Jan 2004, Patrick Braselmann wrote:

> Dear Mizar- Forum,
> 
> I have problems with the correctness of the claculus in CQC_THE1. When
> you admit free variables in the antecedents
> (in CQC_THE1 it is X) the substituation rule is not a correct rule in
> the normal sense. I attached the Mizar file and the abstract of the
> proof.
> I proved the correctness of this calculus when you don´t allow free
> variables in X.  Clearly the attention is that X stands for axioms.
> At last I gave up working with the calculus and have formalized a
> sequent calculus.
> Does someone know something more about correctness of the caclulus in
> CQC_THE1?
> 
> With best regards
> 
> Patrick Braselmann
>