ON PROVING CONSISTENCY OF EQUATIONAL THEORIES IN BOUNDED ARITHMETIC

Abstract We consider equational theories based on axioms for recursively defining functions, with rules for equality and substitution, but no form of induction—we denote such equational theories as PETS for pure equational theories with substitution . An example is Cook’s system PV without its rule for induction. We show that the Bounded Arithmetic theory $\mathrm {S}^{1}_2$ proves the consistency of PETS . Our approach employs model-theoretic constructions for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.