Hardcover ISBN:  9780821845769 
Product Code:  MMONO/128 
List Price:  $165.00 
MAA Member Price:  $148.50 
AMS Member Price:  $132.00 
eBook ISBN:  9781470445362 
Product Code:  MMONO/128.E 
List Price:  $155.00 
MAA Member Price:  $139.50 
AMS Member Price:  $124.00 
Hardcover ISBN:  9780821845769 
eBook: ISBN:  9781470445362 
Product Code:  MMONO/128.B 
List Price:  $320.00 $242.50 
MAA Member Price:  $288.00 $218.25 
AMS Member Price:  $256.00 $194.00 
Hardcover ISBN:  9780821845769 
Product Code:  MMONO/128 
List Price:  $165.00 
MAA Member Price:  $148.50 
AMS Member Price:  $132.00 
eBook ISBN:  9781470445362 
Product Code:  MMONO/128.E 
List Price:  $155.00 
MAA Member Price:  $139.50 
AMS Member Price:  $124.00 
Hardcover ISBN:  9780821845769 
eBook ISBN:  9781470445362 
Product Code:  MMONO/128.B 
List Price:  $320.00 $242.50 
MAA Member Price:  $288.00 $218.25 
AMS Member Price:  $256.00 $194.00 

Book DetailsTranslations of Mathematical MonographsVolume: 128; 1993; 153 ppMSC: Primary 03
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.
ReadershipResearch mathematicians.

Table of Contents

Chapters

Introduction

Chapter I. Upper bounds on deduction elongation in cut elimination

Chapter II. Systems of term equations with substitutions

Chapter III. Logical deduction schemata in axiomatized theories

Chapter IV. Bounds for the complexity of terms occurring in proofs

Chapter V. Proof strengthening theorems


RequestsReview Copy – for publishers of book reviewsPermission – for use of book, eBook, or Journal contentAccessibility – to request an alternate format of an AMS title
 Book Details
 Table of Contents
 Requests
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.
Research mathematicians.

Chapters

Introduction

Chapter I. Upper bounds on deduction elongation in cut elimination

Chapter II. Systems of term equations with substitutions

Chapter III. Logical deduction schemata in axiomatized theories

Chapter IV. Bounds for the complexity of terms occurring in proofs

Chapter V. Proof strengthening theorems