The aim of this work is to develop the tool of logical deduction schemata and use it to establish upper and lower bounds on the complexity of proofs and their transformations in axiomatized theories. The main results are establishment of upper bounds on the elongation of deductions in cut eliminations; a proof that the length of a direct deduction of an existence theorem in the predicate calculus cannot be bounded above by an elementary function of the length of an indirect deduction of the same theorem; a complexity version of the existence property of the constructive predicate calculus; and, for certain formal systems of arithmetic, restrictions on the complexity of deductions that guarantee that the deducibility of a formula for all natural numbers in some finite set implies the deducibility of the same formula with a universal quantifier over all sufficiently large numbers.
Readership: Research mathematicians
Author(s): V. P. Orevkov
Series: Translations of Mathematical Monographs, Vol. 128
Publisher: American Mathematical Society
Year: 1993
Language: English
Pages: C+vi+153+B
Cover
Translations of Mathematical Monographs 128
Complexity of Proofs and Their Transformations in Axiomatic Theories
Copyright ®1993 by the American Mathematical Society
ISBN 0-8218-4576-4
QA9.54.07413 1993 511.3-dc20
LCC 93-11139 CIP
Contents
Introduction
CHAPTER I Upper Bounds on Deduction Elongation in Cut Elimination
§1. The calculi KGL(2L) and IGL(2t)
§2. Measures of the complexity of proofs
§3. Admissibility of structural rules
§4. Cut elimination in KGL(S) and IGL(S)
§5. The calculi KH(Qt) and IH(Qt)
CHAPTER II Systems of Term Equations with Substitutions
§6. Systems of term equations with substitutions. Main lemmas
§7. Extension tree of aCTS-system
§8. Representation of enumerable sets by TS-systems
§9. Upper bounds on the height of natural solutions of systems of linear Diophantine equations
§10. Upper bound on the periodicity index of solutions of CTS-systems
§11. An algorithm deciding the existence of solutions of restricted substitution width
CHAPTER III Logical Deduction Schemata in Axiomatized Theories
§12. Systems of equations in formulas
§13. Deduction schemata in axiomatized Hilbert-type theories
§14. Deducibility of a formula in accordance with a given schema
§15. Deduction schemata in Gentzen calculi
CHAPTER IV Bounds for the Complexity of Terms Occurring in Proofs
§17. Comparison of the lengths of direct and indirect proofs of existence theorems in the predicate calculus
§18. Complexity version of the existence property of the constructive predicate calculus
CHAPTER V Proof Strengthening 'Theorems
§19. Proof strengthening theorems in finitely axiomatized theories
§20. Proof strengthening theorems in formal arithmetic
§21. Upper and lower bounds on lengths of deductions in formal arithmetics
References
Back Cover
