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

TL;DR

This paper proves the consistency of arithmetic without complete induction using a constructive tableau method with strong negation, establishing cut elimination, disjunction property, and existence property.

Contribution

It introduces a novel proof of consistency for arithmetic without complete induction via tableau systems and cut elimination theorems, with simplified proofs leveraging the disjunction property.

Findings

Proved the consistency of arithmetic without complete induction.

Established cut elimination theorems for the tableau system SN and its subsystem PCN.

Demonstrated the disjunction property and existence property for SN.

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 $\bf SN$ of constructive arithmetic with strong negation without complete induction, for which two types of cut elimination theorems hold. One is $\bf SN$-cut elimination theorem for the full system $\bf SN$. The other is $\bf PCN$-cut elimination theorem for a proposed subsystem $\bf PCN$ of $\bf SN$. The disjunction property and the E-theorem (existence property) for $\bf SN$ are also proved. As a novelty, we shall give a simple proof of a restricted version of $\bf SN$-cut elimination theorem as an application of the disjunction property, using $\bf PCN$-cut elimination theorem.