Abstract
This paper gives a comprehensive and coherent view on permutability in the intuitionistic sequent calculus with cuts. Specifically we show that, once permutability is packaged into appropriate global reduction procedures, it organizes the internal structure of the system and determines fragments with computational interest, both for the computationasproofnormalization and the computationasproofsearch paradigms. The vehicle of the study is a lambdacalculus of multiary proof terms with generalized application, previously developed by the authors (the paper argues this system represents the simplest fragment of ordinary sequent calculus that does not fall into mere natural deduction). We start by adapting to our setting the concept of normal proof, developed by Mints, Dyckhoff, and Pinto, and by defining natural proofs, so that a proof is normal iff it is natural and cutfree. Natural proofs form a subsystem with a transparent CurryHoward interpretation (a kind of formal vector notation for lambdaterms with vectors consisting of lists of lists of arguments), while searching for normal proofs corresponds to a slight relaxation of focusing (in the sense of LJT). Next, we define a process of permutative conversion to natural form, and show that its combination with cut elimination gives a concept of normalization for the sequent calculus. We derive a systematic picture of the full system comprehending a rich set of reduction procedures (cut elimination, flattening, permutative conversion, normalization, focalization), organizing the relevant subsystems and the important subclasses of cutfree, normal, and focused proofs.
BibTeX  Entry
@InProceedings{espritosanto_et_al:LIPIcs:2018:9852,
author = {Jos{\'e} Esp{\'i}rito Santo and Maria Jo{\~a}o Frade and Lu{\'i}s Pinto},
title = {{Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {10:110:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770651},
ISSN = {18688969},
year = {2018},
volume = {97},
editor = {Silvia Ghilezan and Herman Geuvers and Jelena Ivetić},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9852},
URN = {urn:nbn:de:0030drops98523},
doi = {10.4230/LIPIcs.TYPES.2016.10},
annote = {Keywords: sequent calculus, permutative conversion, CurryHoward isomorphism, vector of arguments, generalized application, normal proof, natural proof, cut eli}
}
Keywords: 

sequent calculus, permutative conversion, CurryHoward isomorphism, vector of arguments, generalized application, normal proof, natural proof, cut eli 
Collection: 

22nd International Conference on Types for Proofs and Programs (TYPES 2016) 
Issue Date: 

2018 
Date of publication: 

05.11.2018 