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.2011.538
URN: urn:nbn:de:0030-drops-32551
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3255/
Go to the corresponding LIPIcs Volume Portal

Tatsuta, Makoto ; Berardi, Stefano

Non-Commutative Infinitary Peano Arithmetic

pdf-format:
42.pdf (0.4 MB)

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 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 system is unique among other non-commutative 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 non-commutative infinitary Peano arithmetic is equivalent to Heyting arithmetic with the recursive omega rule and the law of excluded middle for Sigma-0-1 formulas. Thus, non-commutative 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 antecedent-grouping 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 1-backtracking game semantics. This paper shows that this system is equivalent to both non-commutative infinitary Peano arithmetic, and Heyting arithmetic with the recursive omega rule and the Sigma-0-1 excluded middle.

BibTeX - Entry

@InProceedings{tatsuta_et_al:LIPIcs:2011:3255,
  author =	{Makoto Tatsuta and Stefano Berardi},
  title =	{{Non-Commutative Infinitary Peano Arithmetic}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{538--552},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3255},
  URN =		{urn:nbn:de:0030-drops-32551},
  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

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