Chaudhuri, Kaustuv ;
Hetzl, Stefan ;
Miller, Dale
A Systematic Approach to Canonicity in the Classical Sequent Calculus
Abstract
The sequent calculus is often criticized for requiring proofs to
contain large amounts of lowlevel 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 stepssuch as instantiating a block of quantifiersby irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically noninterfering 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. Proofnets, 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 firstorder logic. The essential element of our approach is the use of a multifocused sequent calculus as the means of abstracting away the details from classical cutfree sequent proofs. We show that, among the multifocused proofs, the maximally multifocused 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 firstorder 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 = {183197},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897422},
ISSN = {18688969},
year = {2012},
volume = {16},
editor = {Patrick C{\'e}gielski and Arnaud Durand},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3672},
URN = {urn:nbn:de:0030drops36723},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.183},
annote = {Keywords: Sequent Calculus, Canonicity, Classical Logic, Expansion Trees}
}
Keywords: 

Sequent Calculus, Canonicity, Classical Logic, Expansion Trees 
Seminar: 

Computer Science Logic (CSL'12)  26th International Workshop/21st Annual Conference of the EACSL

Issue date: 

2012 
Date of publication: 

2012 