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.