RUS  ENG
Full version
JOURNALS // Zapiski Nauchnykh Seminarov POMI // Archive

Zap. Nauchn. Sem. LOMI, 1988 Volume 174, Pages 132–146 (Mi znsl4515)

This article is cited in 3 papers

Schemes of proof in Hilbert-type axiomatic theories

V. P. Orevkov


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.

UDC: 510.66


 English version:
Journal of Soviet Mathematics, 1991, 55:2, 1610–1620

Bibliographic databases:


© Steklov Math. Inst. of RAS, 2025