Re: [mizar] Calculus in CQC_THE1

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

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.

Best,
Josef