[Proof Complexity] new preprint

[Arnold Beckmann]

Dear colleagues,

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

https://arxiv.org/abs/2203.04832

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!

Best,
Arnold

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

http://www.swansea.ac.uk/staff/science/computer-science/a.beckmann/