Given a theory T, let 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 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. References