The consistency of arithmetic from a point of view of constructive tableau method with strong negation, Part I: the system without complete induction

Abstract

In this Part I, we shall prove the consistency of arithmetic without complete induction from a point of view of strong negation, using its embedding to the tableau system $\mathbf{SN}$ of constructive arithmetic with strong negation without complete induction, for which two types of cut elimination theorems hold. One is $\mathbf{SN}$-cut elimination theorem for the full system $\mathbf{SN}$. The other is $\mathbf{PCN}$-cut elimination theorem for a proposed subsystem $\mathbf{PCN}$ of $\mathbf{SN}$. The disjunction property and the E-theorem (existence property) for $\mathbf{SN}$ are also proved. As a novelty, we shall give a simple proof of a restricted version of $\mathbf{SN}$-cut elimination theorem as an application of the disjunction property, using $\mathbf{PCN}$-cut elimination theorem.

39 pages