On proving consistency of equational theories in Bounded Arithmetic

DOI10.2178/JSL/1190150044arXiv2203.04832MaRDI QIDQ6393250

Publication date: 9 March 2022

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_{2}^{1}

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.

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30)

This page was built for publication: On proving consistency of equational theories in Bounded Arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6393250)