License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2012.183
URN: urn:nbn:de:0030-drops-36723
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3672/
Go to the corresponding LIPIcs Volume Portal

Chaudhuri, Kaustuv ; Hetzl, Stefan ; Miller, Dale

A Systematic Approach to Canonicity in the Classical Sequent Calculus

pdf-format:
18.pdf (0.5 MB)

Abstract

The sequent calculus is often criticized for requiring proofs to
contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps-such as instantiating a block of quantifiers-by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity: proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings, and atomic flows are examples of such revolutionary formalisms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means of abstracting away the details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that make the foci as parallel as possible are canonical. Moreover, such proofs are isomorphic to expansion proofs - a well known, minimalistic, and parallel generalization of Herbrand
disjunctions - for classical first-order logic. This technique is a
systematic way to recover the desired essence of any sequent proof
without abandoning the sequent calculus.

BibTeX - Entry

@InProceedings{chaudhuri_et_al:LIPIcs:2012:3672,
  author =	{Kaustuv Chaudhuri and Stefan Hetzl and Dale Miller},
  title =	{{A Systematic Approach to Canonicity in the Classical Sequent Calculus}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{183--197},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{Patrick C{\'e}gielski and Arnaud Durand},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3672},
  URN =		{urn:nbn:de:0030-drops-36723},
  doi =		{10.4230/LIPIcs.CSL.2012.183},
  annote =	{Keywords: Sequent Calculus, Canonicity, Classical Logic, Expansion Trees}
}

Keywords: Sequent Calculus, Canonicity, Classical Logic, Expansion Trees
Collection: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
Issue Date: 2012
Date of publication: 03.09.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI