Re: [mizar] Calculus in CQC_THE1

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Tue, Jan 27, 2004 at 04:41:44PM +0100, Josef Urban wrote:
> 
> Hi,
> 
> 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 still do not understand it all, but having both
>  Th11: {'not' (P!l1)} |- 'not' (P!l2)
> and
>  Th7: {'not' (P!l1)} |= 'not' (P!l2) implies contradiction
> 
> where P!l1 is just P[x,y], looks very suspicious to me.
> 
> > 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.
> 
> If I am not missing something, the CQC stuff also does not allow function 
> symbols - it would be nice to have them too in some more standard first 
> order logic formalization.
> 
> > Does someone know something more about correctness of the caclulus in
> > CQC_THE1?
> 
> I was hoping someone from Bialystok participating on that series would 
> explain it.
> Btw. this is a reason why to put some references into the articles, so 
> that one could compare things with the book that served for the 
> formalization, when strange definition occurs.

I was hoping that some of the original authors of CQC-things would respond but
they are not active in Mizar anymore I think.   This is what I answered Patrick
in a private e-mail:

 - I am afraid that all this is based on a misunderstanding.  I cannot speak
 - for what the authors of the CQC articles meant but I am afraid they intended
 - consistency as
 - 
 -         X |- p implies (J |= X implies J |= p)
 - 
 - when you have no free variables in X and p and thus your definitions
 - should have been:
 - 
 -         definition let A,J,X;
 -           pred J |= X means :Def1: p in X implies J |= p;
 -         end;
 - 
 -         definition let X,p;
 -           pred X |= p means :Def2:
 -            J |= X implies J |= p;
 -         end;
 - 
 - but then your argument collapses.
 - 
 - I am only guessing, let us wait, maybe someone knows better.

I can be wrong as I barely know the stuff.


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