CONSISTENCY PROOF OF AN ARITHMETIC WITH SUBSTITUTION INSIDE A BOUNDED ARITHMETIC
Yoriyuki Yamagata · arXiv (Cornell University) · 2016
This paper presents a proof that a theory of bounded arithmetic of Buss's hierarchy is capable of proving the consistency of a system based on Cook and Urquhart's equational theory of a feasible arithmetic from which induction has been removed but retains substitution. This result improves Beckmann's result which proves consistency of such a system without substitution inside a bounded arithmetic of Buss's hierarchy. Our proof relies on the notion of of the terms that appear in the theory of Cook and Urquhart. In our work, we first prove that, in the system under consideration, if an equation is proved and either its left or right hand side is computed, then there is a corresponding computation for its right or left hand side, respectively. By carefully computing the bound of the size of the computation, the proof inside a bounded arithmetic of this theorem is obtained, from which the consistency of the system is readily proven. This result apparently implies separation of bounded arithmetics because Buss and Ignjatovi\'c stated that it is not possible to prove the consistency of such a system in the weakest theory of Buss's hierarchy. However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours. On the other hand, the system we considered is strictly equational, which is a property on which our proof relies.