Data di Pubblicazione:
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 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 1-backtracking 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 Sigma-0-1 excluded middle.
Tipologia CRIS:
04A-Conference paper in volume
Keywords:
non commutative logic; substructural logic; classical logic
Elenco autori:
M. Tatsuta; S. Berardi
Link alla scheda completa:
Titolo del libro:
Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings
Pubblicato in: