math.LO
The consistency of arithmetic from a point of view of constructive tableau method with strong negation, Part I the system without complete induction. 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.