Non-Commutative Infinitary Peano Arithmetic

Makoto Tatsuta & Stefano Berardi
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 non-commutative sequents, called non-commutative infinitary Peano arithmetic, so that the system becomes equivalent to Peano arithmetic with the omega-rule if the the exchange rule is added to this system. This...