**Translations of Mathematical Monographs**

1993;
153 pp;
Hardcover

MSC: Primary 03;

**Print ISBN: 978-0-8218-4576-9
Product Code: MMONO/128**

List Price: $84.00

AMS Member Price: $67.20

MAA Member Price: $75.60

**Electronic ISBN: 978-1-4704-4536-2
Product Code: MMONO/128.E**

List Price: $79.00

AMS Member Price: $63.20

MAA Member Price: $71.10

# Complexity of Proofs and Their Transformations in Axiomatic Theories

Share this page
*V. P. Orevkov*

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.

#### Table of Contents

# Table of Contents

## Complexity of Proofs and Their Transformations in Axiomatic Theories

- Cover Cover11
- Title page iii4
- Contents v6
- Introduction 18
- Chapter I. Upper bounds on deduction elongation in cut elimination 916
- Chapter II. Systems of term equations with substitutions 3138
- Chapter III. Logical deduction schemata in axiomatized theories 8188
- Chapter IV. Bounds for the complexity of terms occurring in proofs 119126
- Chapter V. Proof strengthening theorems 131138
- References 151158
- Back Cover Back Cover1162