%0 Generic %1 yamagata2014consistency %A Yamagata, Yoriyuki %D 2014 %K consistency proof %T Consistency proof of a feasible arithmetic inside a bounded arithmetic %U http://arxiv.org/abs/1411.7087 %X In this paper, we prove that $S^1_2$ can prove consistency of $PV^-$, the system obtained from Cook and Urquhart's $PV$ by removing induction. This apparently contradicts Buss and Ignjatović 1995, since they prove that $PV \notCon(PV^-)$. However, what they actually prove is unprovability of consistency of the system which is obtained from $PV^-$ by addition of propositional logic and $BASIC^e$-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 $\rho$ 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 $\rho$, we get $S^1_2$-proof of consistency of $PV^-$.

@misc{yamagata2014consistency, abstract = {In this paper, we prove that $S^1_2$ can prove consistency of $\text{PV}^-$, the system obtained from Cook and Urquhart's $\text{PV}$ by removing induction. This apparently contradicts Buss and Ignjatovi\'c 1995, since they prove that $\text{PV} \not\vdash \text{Con}(\text{PV}^-)$. However, what they actually prove is unprovability of consistency of the system which is obtained from $\text{PV}^-$ by addition of propositional logic and $BASIC^e$-axioms. On the other hand, our $\text{PV}^-$ is strictly equational and our proof relies on it. Our proof relies on big-step semantics of terms of $\text{PV}$. We prove that if $\text{PV} \vdash t = u$ and there is a derivation of $< t, \rho > \downarrow v$ where $\rho$ is an evaluation of variables and $v$ is the value of $t$, then there is a derivation of $< u, \rho > \downarrow v$. By carefully computing the bound of the derivation and $\rho$, we get $S^1_2$-proof of consistency of $\text{PV}^-$.}, added-at = {2014-12-24T06:32:02.000+0100}, author = {Yamagata, Yoriyuki}, biburl = {https://www.bibsonomy.org/bibtex/24e30919f55e72d8f26f3c79044d31111/t.uemura}, description = {[1411.7087] Consistency proof of a feasible arithmetic inside a bounded arithmetic}, interhash = {9b8f107576af564f620a6967a1d1a091}, intrahash = {4e30919f55e72d8f26f3c79044d31111}, keywords = {consistency proof}, note = {cite arxiv:1411.7087}, timestamp = {2014-12-24T06:32:02.000+0100}, title = {Consistency proof of a feasible arithmetic inside a bounded arithmetic}, url = {http://arxiv.org/abs/1411.7087}, year = 2014 }