Abstract
Does there exist any sequent calculus such that it is a subclassical logic and it becomes classical logic when the exchange rules are added? The first contribution of this paper is answering this question for infinitary Peano arithmetic. This paper defines infinitary Peano arithmetic with noncommutative sequents, called noncommutative infinitary Peano arithmetic, so that the system becomes equivalent to Peano arithmetic with the omegarule if the the exchange rule is added to this system. This system is unique among other noncommutative systems, since all the logical connectives have standard meaning and specifically the commutativity for conjunction and disjunction is derivable. This paper shows that the provability in noncommutative infinitary Peano arithmetic is equivalent to Heyting arithmetic with the recursive omega rule and the law of excluded middle for Sigma01 formulas. Thus, noncommutative infinitary Peano arithmetic is shown to be a subclassical logic. The cut elimination theorem in this system is also proved. The second contribution of this paper is introducing infinitary Peano arithmetic having antecedentgrouping and no right exchange rules. The first contribution of this paper is achieved through this system. This system is obtained from the positive fragment of infinitary Peano arithmetic without the exchange rules by extending it from a positive fragment to a full system, preserving its 1backtracking game semantics. This paper shows that this system is equivalent to both noncommutative infinitary Peano arithmetic, and Heyting arithmetic with the recursive omega rule and the Sigma01 excluded middle.
BibTeX  Entry
@InProceedings{tatsuta_et_al:LIPIcs:2011:3255,
author = {Makoto Tatsuta and Stefano Berardi},
title = {{NonCommutative Infinitary Peano Arithmetic}},
booktitle = {Computer Science Logic (CSL'11)  25th International Workshop/20th Annual Conference of the EACSL},
pages = {538552},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897323},
ISSN = {18688969},
year = {2011},
volume = {12},
editor = {Marc Bezem},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3255},
URN = {urn:nbn:de:0030drops32551},
doi = {10.4230/LIPIcs.CSL.2011.538},
annote = {Keywords: proof theory, cut elimination, intuitionistic logic, infinitary logic, recursive omega rules, substructural logic}
}
Keywords: 

proof theory, cut elimination, intuitionistic logic, infinitary logic, recursive omega rules, substructural logic 
Collection: 

Computer Science Logic (CSL'11)  25th International Workshop/20th Annual Conference of the EACSL 
Issue Date: 

2011 
Date of publication: 

31.08.2011 