Products Proof Theory and Logical Complexity Book information Product description Author information and services Ordering information Bibliographic information Conditions of sale Volume information Volume I Book-related information Submit your book proposal Other books in same subject area Support & contact About Elsevier Select your view

	PROOF THEORY AND LOGICAL COMPLEXITY Volume I Description This volume is the first in a series which will, in the future, be published jointly by Bibliopolis, Edizioni di Filosofia e Scienze spa, Napoli, and under the North-Holland imprint by Elsevier Science Publishers, Amsterdam. This is the first of a two-part work covering the main ideas and techniques of proof theory. This volume is introductory, starting with Hilbert (whose second problem in the famous list of problems of 1900 was the consistency of number theory), describing Hilbert's program and its demise at the hands of Gödel. It then proceeds with Gentzen's result (the Hauptsatz is the main result of Part I) and improvements and generalizations to ω-logic. Volume II will cover more advanced logics. Contents Introduction: Elementary Proof Theory. The Fall of Hilbert's Program. Hilbert's Program. Recursive Functions. The First Incompleteness Theorem. The Second Incompleteness Theorem. Exercises. Annex: Intuitionism. Part I: Σ 0 1 Proof Theory. The Calculus of Sequents. Definitions. Completeness of the Sequent Calculus. The Cut-Elimination Theorem. The Subformula Property. Intuitionistic Sequent Calculus. Herbrand's Theorem. Generalization. Annex: Natural Deduction. The Church-Rosser Property. Strong Normalization. The Semantics of Sequent Calculus. Completeness of the Cut-Free Rules. Three-Valued Models. Three-Valued Logic. Annex: Takeuti's Conjecture. Limitations of Takeuti's Conjecture. Three-Valued Equivalence. Cut-Free Analysis. Three-Valued Semantics and Generalized Logics. Applications of the ``Hauptsatz''. The Interpolation Lemma. The Reflection Schema of PA. Elementary Consistency Proofs. 1-Consistency. Annex: The Hauptsatz in a Concrete Case. Normalization in HA. Normalization for NL2J. Part II: Π 1 1 Proof Theory. Π 1 1 Formulas and Well-Foundedness. The Projective Hierarchy. Well-Founded Trees. Well-Orders. Equivalents of (Σ0 1-CA*). Recursive Well-Orders. Hyperarithmetical Sets. Annex: Kleene's 0. Hierarchies Indexed by 0. Paths Through 0. The Classification Problem. The ω-Rule. ω-Logic. The Cut-Elimination Theorem. Bounds for Cut-Elimination. Equivalents for (Σ0 1-CA*). Annex: The Calculus Lω1ω. Cut-Elimination in Lω1ω. The Ordinal ε o and Arithmetic. Ordinal Analysis of PA. Extensions to other Systems. Ordinals and Theories. Annex: Gödel's System T. Functional Interpretation. Spector's Interpretation. No Conterexample Interpretation. An Application. Bibliography. Analytical Index. Bibliographic & ordering Information Hardbound, 504 pages, publication date: OCT-1990 ISBN: 0-444-98715-0 Imprint: NORTH-HOLLAND Price and Ordering Price: EUR 144 USD 144 Books and book related electronic products are priced in US dollars (USD), euro (EUR), and Great Britain Pounds (GBP). USD prices apply to the Americas. EUR prices apply in Europe. GBP prices apply to the UK and all other countries. Customers who order on-line from the Americas will be invoiced in USD and all other countries will be invoiced in GBP. See also information about conditions of sale & ordering procedures, and links to our regional sales offices.