The k-Provability Problem for Gentzen-Style Sequent Systems William M. Farmer 1989 Abstract The k-provability problem for a formal system F is to determine, given an integer k >= 1 and a formula phi in the language of F, whether or not there is a proof of phi in F containing at most k lines (i.e., formulas or sequents). In this paper we consider the k-provability problem for Gentzen-style sequent systems which contain a finite number of axiom schemata (including individual axioms) and a finite number of rules of inference. We prove that the k-provability problem is decidable for Gentzen's sequent calculus LK without cut plus a finite number of individual axioms.