Geodesic
Schemes of proof in Hilbert-type axiomatic theories
Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part 3, Tome 174 (1988), pp. 132-146

Voir la notice de l'article 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. 
@article{ZNSL_1988_174_a5,
     author = {V. P. Orevkov},
     title = {Schemes of proof in {Hilbert-type} axiomatic theories},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {132--146},
     publisher = {mathdoc},
     volume = {174},
     year = {1988},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1988_174_a5/}
}
TY  - JOUR
AU  - V. P. Orevkov
TI  - Schemes of proof in Hilbert-type axiomatic theories
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1988
SP  - 132
EP  - 146
VL  - 174
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1988_174_a5/
LA  - ru
ID  - ZNSL_1988_174_a5
ER  - 
%0 Journal Article
%A V. P. Orevkov
%T Schemes of proof in Hilbert-type axiomatic theories
%J Zapiski Nauchnykh Seminarov POMI
%D 1988
%P 132-146
%V 174
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ZNSL_1988_174_a5/
%G ru
%F ZNSL_1988_174_a5
V. P. Orevkov. Schemes of proof in Hilbert-type axiomatic theories. Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part 3, Tome 174 (1988), pp. 132-146. http://geodesic.mathdoc.fr/item/ZNSL_1988_174_a5/