论文标题
证明有限算术中方程理论的一致性
On proving consistency of equational theories in Bounded Arithmetic
论文作者
论文摘要
我们认为允许替代但禁止归纳的纯正方程理论，我们根据其功能符号的递归定义表示为宠物。我们表明，有限的算术理论$ s^1_2 $证明了宠物的一致性。我们的方法基于界限算术中类似于域理论的概念的近似值，采用宠物的模型，这可能具有独立的利益。
We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory $S^1_2$ proves the consistency of PETS. Our approach employs models for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.
