2 Apr 2008 23:55
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.
(Continue reading)
RSS Feed