A unification-theoretic method for investigating the \(k\)-provability problem (Q1814133)

The \(k\)-provability problem for first-order axiomatic systems with a finite number of axiom schemata and a finite number of rules of inference is investigated. The \(k\)-provability problem is to determine, given a natural number \(k\) and a formula \(F\), whether or not there is a proof of \(F\) containing at most \(k\) lines. In order to make this notion precise, the notion of a Parikh system is introduced. The author notes that almost all first-order axiomatic systems that are to be found in the literature (including Peano arithmetic) can be formulated as Parikh systems. Various ways of classifying Parikh systems are proposed. Also, three different ways of formulating first-order logics --- two of which lead to Parikh systems with decidable \(k\)-provability problems --- are presented. The major part of the paper is devoted to develop a method for investigating the \(k\)-provability problem that utilizes techniques and concepts from unification theory. By solving various subproblems of the unification problem (which is undecidable), the author solves the \(k\)-provability problem for a variety of Parikh systems including several formulations of Peano arithmetic.