Cirquent calculus deepened

A new version of the paper is now available at
                                      http://arxiv.org/abs/0709.1308
A substantial change of perspective has taken place: classical logic can be 
seen as a natural conservative fragment of resource logics in the form of deep 
cirquent calculus. It is an extreme special case of cirquent-based resource 
logics where "everything is shared". And the approach of linear logic is 
another imperfect extreme where "nothing is shared". Cirquent calculus is thus 
a general unifying framework.

Those who earlier took interest in this paper, might want to at least read the 
(totally new) introductory section of the new version.

                                                      G.Japaridze
                                         Cirquent calculus deepened
                                                       Abstract

Cirquent calculus is a new proof-theoretic and  semantic framework, whose main 
distinguishing feature is being based on circuit-style structures (called 
cirquents), as opposed   to the more traditional approaches that deal with 
tree-like objects such as formulas or sequents. Among its advantages are 
greater efficiency, flexibility and expressiveness. This paper presents a 
detailed elaboration of a deep-inference cirquent logic, which is naturally and 
inherently resource conscious. It shows that classical logic, both 
syntactically and semantically, can be seen to be just a special, conservative 
fragment of this more general and, in a sense, more basic logic --- the logic 
of resources in the form of cirquent calculus. The reader will find various 
arguments in favor of switching to the new framework, such as arguments showing 
the insufficiency of the expressive power of linear logic or other 
formula-based approaches to developing resource logics, exponential 
improvements over the traditional approaches in both representational and proof 
complexities offered by cirquent calculus (including the existence of 
polynomial size cut-, substitution- and extension-free cirquent calculus proofs 
for the notoriously hard pigeonhole principle), and more. Among the main 
purposes of this paper is to provide an introductory-style  starting point for 
what, as the author wishes to hope, might have a chance to become a new line of 
research in proof theory --- a proof theory based on circuits instead of 
formulas.

Giorgi Japridze
http://www.csc.villanova.edu/~japaridz/