On proving consistency of equational theories in Bounded Arithmetic

TL;DR

This paper demonstrates that the Bounded Arithmetic theory $S^1_2$ can prove the consistency of pure equational theories with recursive function definitions, using models inspired by domain theory.

Contribution

It introduces a novel approach employing models based on approximate values to prove consistency of PETS in bounded arithmetic.

Findings

$S^1_2$ proves the consistency of PETS.

Models based on approximate values are effective for this proof.

The approach may have broader applications 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.