1 Search Results for "Tatsuta, Makoto"

Document

DOI: 10.4230/LIPIcs.CSL.2011.538

Non-Commutative Infinitary Peano Arithmetic

Authors: Makoto Tatsuta and Stefano Berardi

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

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.

Cite as

Makoto Tatsuta and Stefano Berardi. Non-Commutative Infinitary Peano Arithmetic. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 538-552, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{tatsuta_et_al:LIPIcs.CSL.2011.538,
  author =	{Tatsuta, Makoto and Berardi, Stefano},
  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 =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.538},
  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}
}

Refine by Author
1 Berardi, Stefano
1 Tatsuta, Makoto

Refine by Classification

Refine by Keyword
1 cut elimination
1 infinitary logic
1 intuitionistic logic
1 proof theory
1 recursive omega rules
Show More...

Refine by Type
1 document

Refine by Publication Year
1 2011

1 Search Results for "Tatsuta, Makoto"

Non-Commutative Infinitary Peano Arithmetic

Abstract

Cite as

Thanks for your feedback!

Could not send message