Abstract:
Given a proof in a Hilbert-type system by the scheme of this proof we understand a corresponding list of remarks explaining, for each formula, whether it is axiom and under which schema, and if derived by a rule, by which rule and using which premisses. Let $T$ be a Hilbert-type axiomatic theory whose language contains function symbol of arity $\geqslant2$. For $T$ it is not decidable, whether a formula $A$ has a proof in $T$ with a given schema. Let $T'$ be a Hilbert-type axiomatic theory whose language does not contain function symbols of arity $\geqslant2$. For $T'$ it is decidable whether a formula $A$ has a proof in $T'$ with a given schema.