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