[Proof Complexity] new preprint

Arnold Beckmann a.beckmann at swansea.ac.uk
Thu Mar 10 09:46:11 CET 2022

Dear colleagues,

A new preprint, "On proving consistency of equational theories in Bounded Arithmetic", by Yoriyuki Yamagata and me, is available at


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.

Suggestions and comments are most welcome!


Yr Athro | Professor Arnold Beckmann FLSW
Coleg Gwyddoniaeth | College of Science
Prifysgol Abertawe | Swansea University


More information about the Proof-Complexity mailing list