论文标题
从建设性图表法的角度来看，算术的一致性具有强烈的否定，第一部分：无归纳的系统
The consistency of arithmetic from a point of view of constructive tableau method with strong negation, Part I: the system without complete induction
论文作者
论文摘要
在本第I部分中，我们将在强烈的否定的角度证明算术的一致性，而没有完全诱导的一致性，将其嵌入到Tableau System中$ \ bf sn $ \ bf SN $具有强大的否定而没有完全诱导的情况下，这两种类型的剪切消除定理持有。一个是$ \ bf sn $ -cut消除定理，用于完整系统$ \ bf sn $。另一个是$ \ bf pcn $ -cut消除定理，用于拟议的子系统$ \ bf pcn $ $ \ bf sn $。还证明了$ \ bf sn $的分离属性和E理论（存在属性）。作为新颖性，我们将使用$ \ bf pcn $ -cut消除定理提供一个简单的证明$ \ bf sn $ - 切除定理的限制版本。
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.
