What is included with this book?
Preface | p. xiii |
Introduction | p. 1 |
The Predicate Calculus and the System LK | p. 9 |
Propositional Calculus | p. 9 |
Gentzen's Propositional Proof System PK | p. 10 |
Soundness and Completeness of PK | p. 12 |
PK Proofs from Assumptions | p. 13 |
Propositional Compactness | p. 16 |
Predicate Calculus | p. 17 |
Syntax of the Predicate Calculus | p. 17 |
Semantics of Predicate Calculus | p. 19 |
The First-Order Proof System LK | p. 21 |
Free Variable Normal Form | p. 23 |
Completeness of LK without Equality | p. 24 |
Equality Axioms | p. 31 |
Equality Axioms for LK | p. 32 |
Revised Soundness and Completeness of LK | p. 33 |
Major Corollaries of Completeness | p. 34 |
The Herbrand Theorem | p. 35 |
Notes | p. 38 |
Peano Arithmetic and Its Subsystems | p. 39 |
Peano Arithmetic | p. 39 |
Minimization | p. 44 |
Bounded Induction Scheme | p. 44 |
Strong Induction Scheme | p. 44 |
Parikh's Theorem | p. 44 |
Conservative Extensions of I¿_{0} | p. 49 |
Introducing New Function and Predicate Symbols | p. 50 |
<$$$>: A Universal Conservative Extension of I¿_{0} | p. 54 |
Defining y = 2^{x} and BIT(i, x) in I¿_{0} | p. 59 |
I¿_{0} and the Linear Time Hierarchy | p. 65 |
The Polynomial and Linear Time Hierarchies | p. 65 |
Representability of LTH Relations | p. 66 |
Characterizing the LTH by I¿_{0} | p. 69 |
Buss's S^{i}_{2}; Hierarchy: The Road Not Taken | p. 70 |
Notes | p. 71 |
Two-Sorted Logic and Complexity Classes | p. 73 |
Basic Descriptive Complexity Theory | p. 74 |
Two-Sorted First-Order Logic | p. 76 |
Syntax | p. 76 |
Semantics | p. 78 |
Two-Sorted Complexity Classes | p. 80 |
Notation for Numbers and Finite Sets | p. 80 |
Representation Theorems | p. 81 |
The LTH Revisited | p. 86 |
The Proof System LK^{2} | p. 87 |
Two-Sorted Free Variable Normal Form | p. 90 |
Single-Sorted Logic Interpretation | p. 91 |
Notes | p. 93 |
The Theory V^{0} and AC^{0} | p. 95 |
Definition and Basic Properties0 of V^{i} | p. 95 |
Two-Sorted Functions | p. 101 |
Parikh's Theorem for Two-Sorted Logic | p. 104 |
Definability in V^{0} | p. 106 |
¿ ^{1}_{1}-Definable Predicates | p. 115 |
The Witnessing Theorem for V^{0} | p. 117 |
Independence Follows from the Witnessing Theorem for V^{0} | p. 118 |
Proof of the Witnessing Theorem for V^{0} | p. 119 |
<$$$>: Universal Conservative Extension of V^{0} | p. 124 |
Alternative Proof of the Witnessing Theorem for V^{0} | p. 127 |
Finite Axiomatizability | p. 129 |
Notes | p. 130 |
The Theory V^{1} and Polynomial Time | p. 133 |
Induction Schemes in V^{i} | p. 133 |
Characterizing P by V^{1} | p. 135 |
The "If" Direction of Theorem VI.2.2. | p. 137 |
Application of Cobham's Theorem | p. 140 |
The Replacement Axiom Scheme | p. 142 |
Extending V^{1} by Polytime Functions | p. 145 |
The Witnessing Theorem for V^{1} | p. 147 |
The Sequent System LK^{2}-<$$$> | p. 150 |
Proof of the Witnessing Theorem for V^{1} | p. 154 |
Notes | p. 156 |
Propositional Translations | p. 159 |
Propositional Proof Systems | p. 160 |
Treelike vs Daglike Proof Systems | p. 162 |
The Pigeonhole Principle and Bounded Depth PK | p. 163 |
Translating V^{0} to bPK | p. 165 |
Translating ¿^{B}_{0} Formulas | p. 166 |
<$$$> and LK^{2}-<$$$> | p. 169 |
Proof of the Translation Theorem for V^{0} | p. 170 |
Quantified Propositional Calculus | p. 173 |
QPC Proof Systems | p. 175 |
The System G | p. 175 |
The Systems G_{0} and G^{*}_{i} | p. 179 |
Extended Frege Systems and Witnessing in G^{*}_{1} | p. 186 |
Propositional Translations for V^{i} | p. 191 |
Translating V^{0} to Bounded Depth G^{*}_{0} | p. 195 |
Notes | p. 198 |
Theories for Polynomial Time and Beyond | p. 201 |
The Theory VP and Aggregate Functions | p. 201 |
The Theory <$$$> | p. 207 |
The Theory VPV | p. 210 |
Comparing VPV and V^{1} | p. 213 |
VPV Is Conservative over VP | p. 214 |
TV^{0} and the TV^{i} Hierarchy | p. 217 |
TV^{0} ⊆ VPV | p. 220 |
Bit Recursion | p. 222 |
The Theory V^{1}-HORN | p. 223 |
TV^{1} and Polynomial Local Search | p. 228 |
KPT Witnessing and Replacement | p. 237 |
Applying KPT Witnessing | p. 239 |
More on V^{i} and TV^{i} | p. 243 |
Finite Axiomatizability | p. 243 |
Definability in the V^{?} Hierarchy | p. 245 |
Collapse of V^{?} vs Collapse of PH | p. 253 |
RSUV Isomorphism | p. 256 |
The Theories S^{i}_{2} and T^{i}_{2} | p. 256 |
RSUV Isomorphism | p. 258 |
The # Translation | p. 260 |
The b Translation | p. 262 |
The RSUV Isomorphism between S^{i}_{2} and V^{i} | p. 263 |
Notes | p. 266 |
Theories for Small Classes | p. 267 |
AC^{0} Reductions | p. 269 |
Theories for Subclasses of P | p. 272 |
The Theories VC | p. 273 |
The Theory <$$$> | p. 274 |
The Theory <$$$> | p. 278 |
Obtaining Theories for the Classes of Interest | p. 280 |
Theories for TC^{0} | p. 281 |
The Class TC^{0} | p. 282 |
The Theories VTC^{0}, <$$$>, and <$$$> | p. 283 |
Number Recursion and Number Summation | p. 287 |
The Theory VTC^{0}V | p. 289 |
Proving the Pigeonhole Principle in VTC^{0} | p. 291 |
Denning String Multiplication in VTC^{0} | p. 293 |
Proving Finite Szpilrajn's Theorem in VTC^{0} | p. 298 |
Proving Bondy's Theorem | p. 299 |
Theories for AC^{0} (m) and ACC | p. 303 |
The Classes AC^{0} (m) and ACC | p. 303 |
The Theories V^{0}(2), <$$$>, and <$$$> | p. 304 |
The "onto" PHP and Parity Principle | p. 306 |
The Theory VAC^{0} (2)V | p. 308 |
The Jordan Curve Theorem and Related Principles | p. 309 |
The Theories for AC^{0} (m) and ACC | p. 313 |
The Modulo m Counting Principles | p. 316 |
The Theory VAC^{0} (6)V | p. 318 |
Theories for NC^{1} and the NC Hierarchy | p. 319 |
Definitions of the Classes | p. 320 |
BSVP and NC^{1} | p. 321 |
The Theories VNC^{1}, <$$$>, and <$$$> | p. 323 |
VTC^{0} ⊆ VNC^{1} | p. 326 |
The Theory VNC^{1} V | p. 333 |
Theories for the NC Hierarchy | p. 335 |
Theories for NL and L | p. 339 |
The Theories VNL, <$$$>, and <$$$> | p. 339 |
The Theory V^{1}-KROM | p. 343 |
The Theories VL, <$$$>, and <$$$> | p. 351 |
The Theory VLV | p. 356 |
Open Problems | p. 358 |
Proving Cayley-Hamilton in VNC^{2} | p. 358 |
VSL and VSL <$$$> VL | p. 358 |
Denning [X/Y] in VTC^{0} | p. 360 |
Proving PHP and Count_{m′} in V^{0} (m) | p. 360 |
Notes | p. 360 |
Proof Systems and the Reflection Principle | p. 363 |
Formalizing Propositional Translations | p. 364 |
Verifying Proofs in TC^{0} | p. 364 |
Computing Propositional Translations in TC^{0} | p. 373 |
The Propositional Translation Theorem for TV^{i} | p. 377 |
The Reflection Principle | p. 382 |
Truth Definitions | p. 383 |
Truth Definitions vs Propositional Translations | p. 387 |
RFN and Consistency for Subsystems of G | p. 396 |
Axiomatizations Using RFN | p. 403 |
Proving -Simulations Using RFN | p. 407 |
The Witnessing Problems for G | p. 408 |
VNC^{1} and G^{*}_{0} | p. 410 |
Propositional Translation for VNC^{1} | p. 410 |
The Boolean Sentence Value Problem | p. 414 |
Reflection Principle for PK | p. 421 |
VTC^{0} and Threshold Logic | p. 428 |
The Sequent Calculus PTK | p. 428 |
Reflection Principles for Bounded Depth PTK | p. 433 |
Propositional Translation for VTC^{0} | p. 434 |
Bounded Depth GTC^{0} | p. 441 |
Notes | p. 442 |
Computation Models | p. 445 |
Deterministic Turing Machines | p. 445 |
L, P, PSPACE, and EXP | p. 447 |
Nondeterministic Turing Machines | p. 449 |
Oracle Turing Machines | p. 451 |
Alternating Turing Machines | p. 452 |
Uniform Circuit Families | p. 453 |
Bibliography | p. 457 |
Index | p. 465 |
Table of Contents provided by Ingram. All Rights Reserved. |