|
Zapiski Nauchnykh Seminarov LOMI, 1988, Volume 174, Pages 132–146
(Mi znsl4515)
|
|
|
|
This article is cited in 3 scientific papers (total 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.
Citation:
V. P. Orevkov, “Schemes of proof in Hilbert-type axiomatic theories”, Computational complexity theory. Part 3, Zap. Nauchn. Sem. LOMI, 174, "Nauka", Leningrad. Otdel., Leningrad, 1988, 132–146; J. Soviet Math., 55:2 (1991), 1610–1620
Linking options:
https://www.mathnet.ru/eng/znsl4515 https://www.mathnet.ru/eng/znsl/v174/p132
|
Statistics & downloads: |
Abstract page: | 167 | Full-text PDF : | 72 |
|