Some Results on the Length of Proofs

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