Schemes of proof in Hilbert-type axiomatic theories
Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part 3, Tome 174 (1988), pp. 132-146
Citer cet article
Voir la notice du chapitre de livre provenant de la source Math-Net.Ru
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.