R. Parikh has shown that in the predicate calculus without function symbols it is possible to decide whether or not a given formula A is provable in a Hilbert-style proof of k lines. He has also shown that for any formula A(x1, …, xn) of arithmetic in which addition and multiplication are represented by three-place predicates, {(a1, …, an): A(a1, …, an) is provable from the axioms of arithmetic in k lines} is definable in (N,′, +,0). See [2].In §1 of this paper it is shown that if S is a definable set of n-tuples in (N,′, +, 0), then there is a formula A(x1, …, xn) and a number k so that (a1 …, an) ∈ S if and only if A(a1 …, an) can be proved in a proof of complexity k from the axioms of arithmetic. The result does not depend on which formalization of arithmetic is used or which (reasonable) measure of proof complexity. In particular, this gives a converse to Parikh's result.In §II, a measure of proof complexity is given which is based on counting the quantifier steps in semantic tableaux. The idea behind this measure is that A is k provable if in the attempt to construct a counterexample one meets insurmountable difficulties in the definition of the appropriate Skolem functions over sets of cardinality ≤ k. A method is given for deciding whether or not a sentence A in the full predicate calculus is k provable. The question for the full predicate calculus and Hilbert-style systems of proof remains open.
Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic
