On proving consistency of equational theories in Bounded Arithmetic
Arnold Beckmann, Yoriyuki Yamagata
TL;DR
This work addresses the problem of proving the consistency of pure equational theories with substitution but without induction (PETS) inside bounded arithmetic. It introduces a domain-theory-inspired approximation semantics and frame-based models to interpret equational reasoning under feasibility constraints, enabling formal soundness proofs. The main result shows that $\ ext{S}^{1}_2$ proves the consistency of $ extbf{PETS}( ext{Ax})$, with a stronger $\ ext{S}^{2}_2$-level soundness analysis and a refinement to $\ ext{S}^{1}_2$ via instruction-based formalization of derivations. Together, these contributions provide a novel method for establishing consistency of restricted equational theories within the bounded-arithmetic hierarchy and suggest connections to domain-theoretic ideas in a computationally feasible setting.
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.