Some results on the length of proofs

Abstract:

Given a theory T, let $\vdash _T^kA$ mean “A has a proof in T of at most k lines". We consider a formulation $P{A^\ast }$ of Peano arithmetic with full induction but addition and multiplication being ternary relations. We show that ${ \vdash ^k}A$ is decidable for $P{A^\ast }$ and hence $P{A^\ast }$ is closed under a weak $\omega$-rule. An analogue of Gödel’s theorem on the length of proofs is an easy corollary.