arXiv · 2203.04832
On proving consistency of equational theories in Bounded Arithmetic
Abstract
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.
Explore related subjects
Keep this discovery
Arnold Beckmann, Yoriyuki Yamagata. 2022-03-09. On proving consistency of equational theories in Bounded Arithmetic. https://doi.org/10.1017/jsl.2025.6
Cite the original work for its findings. Save a collection to share your selection of sources.