Proof Theory and Logical Complexity: Vol. I (Studies in Proof Theory)

Front Matter......Page 005.djvu
Contents......Page 007.djvu
Forward......Page 009.djvu
Background & Notation......Page 021.djvu
Introduction: Elementary Proof Theory......Page 029.djvu
Hilbert's program......Page 033.djvu
Recursive functions......Page 038.djvu
The first incompleteness Theorem......Page 052.djvu
The second incompleteness theorem......Page 066.djvu
Exercises......Page 077.djvu
Annex: Intuitionism......Page 082.djvu
Part 1: $\sum_{0}^{1}$ Proof Theory......Page 091.djvu
2. The calculus of sequents......Page 095.djvu
Definitions......Page 097.djvu
Completeness of the sequent calculus......Page 102.djvu
The cut-elimination theorem......Page 105.djvu
The subformula property......Page 114.djvu
Intuitionistic sequent calculus......Page 116.djvu
Herbrand's theorem......Page 118.djvu
Generalization......Page 123.djvu
Annex: Natural deduction......Page 126.djvu
The Church-Rosser property......Page 135.djvu
Strong normalization......Page 150.djvu
3. The semantics of sequent calculus......Page 161.djvu
Completeness of the cut-free rules......Page 162.djvu
Three-valued logic......Page 168.djvu
Annex: Takeuti's conjecture......Page 176.djvu
Limitations of Takeuti's conjecture......Page 183.djvu
Three-valued equivalence......Page 202.djvu
Cut-free analysis......Page 204.djvu
Three-valued semantics and generalized logics......Page 205.djvu
The interpolation lemma......Page 209.djvu
The reflection schema of PA......Page 215.djvu
Elementary consistency proofs......Page 226.djvu
1-consistency......Page 228.djvu
Annex: The Hauptsatz in a concrete case......Page 237.djvu
Normalization in HA......Page 251.djvu
Normalization for NL^2J......Page 269.djvu
Part 2: $\prod_{1}^{1}$ Proof Theory......Page 285.djvu
The projective hierarchy......Page 289.djvu
Well-founded trees......Page 294.djvu
Well-orders......Page 297.djvu
Equivalents of $(\sum_{1}^{0}-CA*)$......Page 299.djvu
Recursive well-orders......Page 311.djvu
Hyperarithmetical sets......Page 316.djvu
Annex: Kleene's $\mathcal{O}$......Page 321.djvu
Hierarchies indexed by $\mathcal{O}$......Page 329.djvu
Paths Through $\mathcal{O}$......Page 335.djvu
The classification problem......Page 339.djvu
$\omega$-logic......Page 347.djvu
The cut-elimination theorem......Page 362.djvu
Bounds for cut-elimination......Page 375.djvu
Equivalents for $(\sum_{1}^{0}-CA*)$......Page 381.djvu
Annex: The calculus $L_\omega_1\omega$......Page 388.djvu
Cut elimination in $L_\omega_1\omega$......Page 393.djvu
Ordinal analysis of P A......Page 411.djvu
Extensions to other systems......Page 422.djvu
Ordinals and Theories......Page 435.djvu
Annex: Goedel's system F......Page 442.djvu
Functional interpretation......Page 459.djvu
Spector's interpretation......Page 477.djvu
No conterexamp1e interpretation......Page 480.djvu
An application......Page 484.djvu
Bibliography......Page 497.djvu
Analytical Index......Page 501.djvu