[Proof Complexity] [Preprint] Consistency proof of a feasible arithmetic inside a bounded arithmetic

山形賴之 yoriyuki.yamagata at aist.go.jp
Thu Nov 27 02:32:18 CET 2014

Dear list,

My new preprint, "Consistency proof of a feasible arithmetic inside a
bounded arithmetic", is now available from ArXiv

In this paper, we prove that S12 can prove consistency of PV−, the
system obtained from Cook and Urquhart's PV by removing induction.
This apparently contradicts Buss and Ignjatovi\'c 1995, since they
prove that PV⊬Con(PV−). However, what they actually prove is
unprovability of consistency of the system which is obtained from PV−
by addition of propositional logic and BASICe-axioms. On the other
hand, our PV− is strictly equational and our proof relies on it. Our
proof relies on big-step semantics of terms of PV. We prove that if
PV⊢t=u and there is a derivation of <t,ρ>↓v where ρ is an evaluation
of variables and v is the value of t, then there is a derivation of
<u,ρ>↓v. By carefully computing the bound of the derivation and ρ, we
get S12-proof of consistency of PV−.

Any comment and criticism are appreciated.


Yoriyuki Yamagata (Senior Researcher)
National Institute of Advanced Industrial Science and Technology (AIST)

More information about the Proof-Complexity mailing list