Proof theory and logical complexity  v. 1

Jean-Yves Girard

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 Godel. It then proceeds with Gentzen's result (the Hauptsatz is the main result of Part I) and improvements and generalizations to omega-logic. Volume II will cover more advanced logics.

「Nielsen BookData」より


  • 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: Sigma 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 NL 2 J. Part II: Pi 1 1 Proof Theory. Pi 1 1 Formulas and Well-Foundedness. The Projective Hierarchy. Well-Founded Trees. Well-Orders. Equivalents of (Sigma 0 1 -CA * ). Recursive Well-Orders. Hyperarithmetical Sets. Annex: Kleene's 0. Hierarchies Indexed by 0. Paths Through 0. The Classification Problem. The omega-Rule. omega-Logic. The Cut-Elimination Theorem. Bounds for Cut-Elimination. Equivalents for (Sigma 0 1 -CA * ). Annex: The Calculus Lomega 1 omega. Cut-Elimination in Lomega 1 omega. The Ordinal epsilon o and Arithmetic. Ordinal Analysis of PA. Extensions to other Systems. Ordinals and Theories. Annex: Godel's System T. Functional Interpretation. Spector's Interpretation. No Conterexample Interpretation. An Application. Bibliography. Analytical Index.

「Nielsen BookData」より


書名 Proof theory and logical complexity
著作者等 Girard, Jean-Yves
Girard J.-Y.
シリーズ名 Studies in proof theory : monographs
巻冊次 v. 1
出版元 Bibliopolis
刊行年月 c1987-
ページ数 v.
大きさ 25 cm
ISBN 0444987150
NCID BA01438918
※クリックでCiNii Booksを表示
言語 英語
出版国 イタリア

Clip to Evernote