论有界算术中等式理论的一致性证明
On proving consistency of equational theories in Bounded Arithmetic
AI总结：
该研究针对基于递归函数符号、允许替换但禁止归纳的纯等式理论PETS，证明有界算术理论$S^1_2$可证其一致性，所采用的基于近似值的PETS模型方法或具独立研究意义。
摘要：
我们研究允许替换但禁止归纳的纯等式理论（记为PETS），其函数符号基于递归定义。我们证明有界算术理论$S^1_2$可证明PETS的一致性。我们的方法采用基于近似值的PETS模型，近似值类似有界算术中的域理论概念，这可能具有独立研究价值。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
