[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Calculus in CQC_THE1

On Fri, Jan 16, 2004 at 09:29:29AM +0100, 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?

Is anybody planning to answer Patrick?


-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr