arXiv · 2010.07368
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 $\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.
Explore related subjects
Keep this discovery
Takao Inoué. 2020-10-14. The consistency of arithmetic from a point of view of constructive tableau method with strong negation, Part I: the system without complete induction. https://arxiv.org/abs/2010.07368
Cite the original work for its findings. Save a collection to share your selection of sources.