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

[山形賴之]

Dear list,

My new preprint, "Consistency proof of a feasible arithmetic inside a
bounded arithmetic", is now available from ArXiv
http://arxiv.org/abs/1411.7087

Abstract
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.

Best,


--
Yoriyuki Yamagata (Senior Researcher)
National Institute of Advanced Industrial Science and Technology (AIST)
http://staff.aist.go.jp/yoriyuki.yamagata/en/