Arithmetic, proof theory, and computational complexity
 Responsibility
 edited by Peter Clote and Jan Krajíček.
 Imprint
 New York : Clarendon Press ; Oxford, England ; New York : Oxford University Press, 1993.
 Physical description
 428 p.
 Series
 Oxford logic guides 23
Online
Available online
At the library
SAL3 (offcampus storage)
Stacks
Request (opens in new tab)
Call number  Note  Status 

QA9.54 .A75 1992  Available 
More options
Description
Creators/Contributors
 Contributor
 Clote, Peter.
 Krajíček, Jan.
Contents/Summary
 Contents

 Preface
 1. Open Problems
 2. Note on the Existence of Most General Semiunifiers
 3. Kreisel's Conjecture for L31 (including a postscript by George Kreisel)
 4. Number of Symbols in Frege Proofs with and without the Deduction Rule
 5. Algorithm for Boolean Formula Evolution and for Tree Contraction
 6. Provably Total Functions in Bounded Arithmetic Theories Ri3, Ui2 and Vi2
 7. On Polynomial Size Frege Proofs of Certain Combinatorial Principles
 8. Interpretability and Fragments of arithmetic
 9. Abbreviating Proofs Using Metamathematical Rules
 10. Open Induction, Tennenbaum Phenomena, and Complexity Theory
 11. Using Herbrandtype Theorems to Separate Strong Fragments of Arithmetic
 12. An Equivalence between Second Order Bounded Domain Bounded Arithmetic and First Order Bounded Arithmetic
 13. Integer Parts of Real Closed Exponential Fields (extended abstract)
 14. Making Infinite Structures Finite in Models of Second Order Bounded Arithmetic
 15. Ordinal Arithmetic in I
 16. RSUV Isomorphism
 17. Feasible Interpretability.
 (source: Nielsen Book Data)
 Publisher's summary

This book principally concerns the rapidly growing area of what might be termed "Logical Complexity Theory", the study of bounded arithmetic, propositional proof systems, length of proof, etc and relations to computational complexity theory. Issuing from a twoyear NSF and Czech Academy of Sciences grant supporting a monthlong workshop and 3day conference in San Diego (1990) and Prague (1991), the book contains refereed articles concerning the existence of the most general unifier, a special case of Kreisel's conjecture on lengthofproof, propositional logic proof size, a new alternating logtime algorithm for boolean formula evaluation and relation to branching programs, interpretability between fragments of arithmetic, feasible interpretability, provability logic, open induction, Herbrandtype theorems, isomorphism between first and second order bounded arithmetics, forcing techniques in bounded arithmetic, ordinal arithmetic in L D o . Also included is an extended abstract of J P Ressayre's new approach concerning the model completeness of the theory of real closed exponential fields. Additional features of the book include (1) the transcription and translation of a recently discovered 1956 letter from K Godel to J von Neumann, asking about a polynomial time algorithm for the proof in ksymbols of predicate calculus formulas (equivalent to the PNP question), (2) an OPEN PROBLEM LIST consisting of 7 fundamental and 39 technical questions contributed by many researchers, together with a bibliography of relevant references.
(source: Nielsen Book Data)
Subjects
 Subjects
 Proof theory.
 Computational complexity.
Bibliographic information
 Publication date
 1993
 ISBN
 0820519650
 0198536909 (cloth) :
 9780198536901 (cloth)
 9780820519654