Proof schemata in Hilbert-type axiomatic theories

A derivation schema in an axiomatic theory is defined as a finite sequence of analysis of applications of rules and axioms. A derivation by a schema U is any derivation whose list of analyses of applications of rules and axioms is precisely U. A derivation schema is admissible if a corresponding derivation can be constructed. Let G be a Hilbert-type axiomatic theory. The following problems are considered: a) to decide whether a given derivation scheme is admissible in G; b) to decide whether a formula is derivable by a given derivation schema in G. In the usual formulations of the predicate calculus without equality, the first problem is shown to be decidable, the second undecidable.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova Akad. Nauk SSSR, Vol. 174, pp. 132–146, 1988.