Re: Calculus of structures and sequent calculus

Yves (et al.)

> : is there some kind of definition for the fact that a formal system 
> describes proofs in classical/linear/intuitionistic/etc. logic?
>
> If so, this yields a way to separate formalisms from logics. And thus 
> to separate debates like CoS>sequents and linear>classical. This is of 
> interest for me, since I do not understand arguments in the second one.
>
One has to be careful here.  For instance, the single and multiple
conclusioned systems of intuitionistic logic prove the same theorems
but have very different proof theories:in the former cut-reduction is 
deterministic,
 and in the latter non-deterministic in the same way as classical logic
(one can formulate the critical "lafont example").

So there is no way (as I see it) to say that two formal systems describe 
the same proof theory
without reference to some semantics of proofs: a mathematical object
in which we interpret proofs (and so can make decisions about proof 
equality).
I have shown in my paper submitted to LICS that SKSg can have the same 
proof theory
as the classical sequent calculus; I hope to show soon that the new deep 
system for
intuitionistic logic can have the same proof theory as the 
multiple-conclusioned intuitionistic
sequent calculus.

Richard


-- 
No virus found in this outgoing message.
Checked by AVG Anti-Virus.
Version: 7.0.300 / Virus Database: 265.8.7 - Release Date: 10/02/2005