Proof Theory

ISBN-13: 9783642664755 / Angielski / Miękka / 2011 / 302 str.

K. Sch Tte; J. N. Crossley

Opis

This book was originally intended to be the second edition of the book "Beweis- theorie" (Grundlehren der mathematischen Wissenschaften, Band 103, Springer 1960), but in fact has been completely rewritten. As well as classical predicate logic we also treat intuitionistic predicate logic. The sentential calculus properties of classical formal and semiformal systems are treated using positive and negative parts of formulas as in the book "Beweistheorie". In a similar way we use right and left parts of formulas for intuitionistic predicate logic. We introduce the theory of functionals of finite types in order to present the Gi:idel interpretation of pure number theory. Instead of ramified type theory, type-free logic and the associated formalization of parts of analysis which we treated in the book "Beweistheorie", we have developed simple classical type theory and predicative analysis in a systematic way. Finally we have given consistency proofs for systems of lI~-analysis following the work of G. Takeuti. In order to do this we have introduced a constni'ctive system of notation for ordinals which goes far beyond the notation system in "Beweistheorie".

Spis treści

A. Pure Logic.- I. Fundamentals.- § 1. Classical Sentential Calculus.- 1. Truth Functions.- 2. Sentential Forms.- 3. Complete Systems of Connectives.- 4. A Formal Language for the Sentential Calculus.- 5. Positive and Negative Parts of Formulas.- 6. Syntactic Characterization of Valid Formulas.- § 2. Formal Systems.- 1. Fundamentals.- 2. Deducible Formulas.- 3. Permissible Inferences.- 4. Sentential Properties of Formal Systems.- 5. The Formal System CS of the Classical Sentential Calculus.- II. Classical Predicate Calculus.- § 3. The Formal System CP.- 1. Primitive Symbols.- 2. Inductive Definition of the Formulas.- 3. P-Forms and N-Forms.- 4. Positive and Negative Parts of a Formula.- 5. Axioms.- 6. Basic Inferences.- § 4. Deducible Formulas and Permissible Inferences.- 1. Generalizations of the Axioms.- 2. Weak Inferences.- 3. Further Permissible Inferences.- 4. Defined Logical Connectives.- §5. Semantics of Classical Predicate Calculus.- 1. Classical Models.- 2. The Consistency Theorem.- 3. The Completeness Theorem.- 4. The Satisfiability Theorem.- 5. Syntactic and Semantic Consequences.- III. Intuitionistic Predicate Calculus.- § 6. Formalization of Intuitionistic Predicate Calculus.- 1. The Formal System IP1.- 2. The Formal System IP2.- 3. Left and Right Parts of Formulas.- 4. The Formal System IP3.- § 7. Deducible Formulas and Permissible Inferences in the System IP3.- 1. Generalizations of the Axioms.- 2. Weak Inferences.- 3. More Permissible Inferences.- 4. Special Features of Intuitionistic Logic.- 5. Properties of Negation.- 6. Syntactic Equivalence.- § 8. Relations between Classical and Intuitionistic Predicate Calculus.- 1. Embedding IP3 in CP.- 2. Interpretation of CP in IP3.- § 9. The Interpolation Theorem.- 1. Interpolation Theorem for the System IP3.- 2. Interpolation Theorem for the System CP.- 3. Finitely Axiomatisable Theories.- 4. Beth’s Definability Theorem.- IV. Classical Simple Type Theory.- § 10. The Formal System CT.- 1. The Formal Language.- 2. Chains of Subterms.- 3. Axioms and Basic Inferences.- 4. Deducible Formulas and Permissible Inferences.- 5. The Cut Rule.- §11. Deduction Chains and Partial Valuations.- 1. Definition of Deduction Chains.- 2. Partial Valuations.- 3. Principal Lemmata.- § 12. Semantics.- 1. Total Valuations over a System of Sets.- 2. Soundness Theorem.- 3. Extending a Partial Valuation.- 4. Completeness Theorem and Cut Rule.- B. Systems of Arithmetic.- V. Ordinal Numbers and Ordinal Terms.- § 13. Theory of Ordinals of the 1st and 2nd Number Classes.- 1. Order Types of Well-Ordered Sets.- 2. Axiomatic Characterization of the 1st and 2nd Number Classes.- 3. Zero, Successor and Limit Numbers and Supremum.- 4. Ordering Functions.- 5. Addition of Ordinals.- 6. ?-Critical Ordinals.- 7. Maximal ?-Critical Ordinals.- § 14. A Notation System for the Ordinals Terms.- § 17. The Formal System FT of Functionals of Finite Type.- 1. The Formal Language.- 2. Deduction Procedures.- 3. The Consistency of the System FT.- 4. Fundamental Deduction Rules.- 5. Addition and Multiplication.- 6. The Indentity Functional I? and ?-Abstraction.- 7. The Predecessor Functional and the Arithmetic Difference.- 8. The Recursor.- 9. Simultaneous Recursion.- 10. The Characteristic Term of a Basic Formula.- VII. Pure Number Theory.- § 18. The Formal System PN for Pure Number Theory.- 1. The Formal Language.- 2. The Deduction Procedure.- 3. Basic Properties of Deducibility.- 4. Properties of Negation.- 5. Positive and Negative Parts of Formulas.- 6. The Consistency of the System PN.- § 19. Interpretation of PN in FT.- 1. Sequences of Terms of the System FT.- 2. The Formal System QFT.- 3. Interpreting Formulas.- 4. Interpretations of the Axioms of the System PN.- 5. Interpretations of the Basic Inferences in the System PN.- C. Subsystems of Analysis.- VIII. Predicative Analysis.- § 20. Systems of ?11-Analysis.- 1. The Formal Language of Second Order Arithmetic.- 2. The Formal System DA.- 3. Deducible Formulas and Permissible Inference of the System DA.- 4. The Semi-Formal System DA*.- 5. Embedding DA in DA*.- 6. General Properties of Deduction in the System DA*.- 7. Subsystems of DA and DA*.- §21. Deductions of Transfinite Induction.- 1. Formalisation of Transfinite Induction.- 2. Deductions in EN.- 3. Deductions in EN*.- 4. Deductions in EA and EA*.- 5. The Formula? [P, Q, t].- 6. Deductions in DA.- 7. Deductions in DA*.- § 22. The Semi-Formal System RA* for Ramified Analysis.- 1. The Formal Language.- 2. The Deduction Procedures.- 3. Weak Inferences.- 4. Elimination of Cuts.- 5. Further Properties of Deductions.- 6. Interpretations of EA* and DA* in RA*.- § 23. The Limits of the Deducibility of Transfinite Induction.- 1. Orders of Deductions of Induction in RA*.- 2. The Limiting Numbers of the Systems EN, EA and DA.- 3. The Autonomous Ordinal Terms of the Systems EN*, EA* and DA*.- 4. The Autonomous Ordinal Terms of the System RA*.- 5. The Limits of Predicativity.- IX. Higher Ordinals and Systems of ?11-Analysis.- § 24. Normal Functions on a Segment ?* of the Ordinals.- 1. Axiomatic Characterization of the Segment ?* of the Ordinals.- 2. Basic Properties of ?*.- 3. Definition of the Functions ?a.- 4. Properties of the ? Functions.- 5. The Sets ?(?)and ??Functions.- § 25. A Notation System for Ordinals Based on the ?? Functions.- 1. The Set ?(?) of Ordinals.- 2. Sets of Coefficients.- 3. The Systems T* and OT* of Terms.- 4. Subsystems ?(?)of ?(?).- 5. The Ordinal, ?0.- 6. Relations between Cr (?) and In (?).- §26. Level-Lowering Functions of the Ordinals.- 1. Basic Concepts.- 2. Properties of the Sets of Coefficients.- 3. The Ordinal Term di?.- 4. The Natural Sum.- 5. Deduction Functions.- § 27. The Formal System GPA for a Generalized ?11-Analysis.- 1. The Formal Language.- 2. Axioms, Basic Inference and Substitution Inferences.- 3. Deductions.- 4. Orders of Normal Deductions.- 5. Transformations of Normal Deductions.- 6. Reducible Normal Deductions.- 7. Singular Normal Deductions.- 8. Reduction of a Suitable Cut.- 9. The Consistency of the System GPA.- 10. The Subsystem PA of GPA.- § 28. The Semi-Formal System PA*.- 1. Axioms and Basic Inferences of the System PA*.- 2. The Strength of a Formula.- 3. Basic Deductions in the System PA*.- 4. Embedding of PA in PA*.- 5. Elimination of Strong Cuts in PA*.- 6. Normal Deductions in the System PA*.- 7. Reducible Normal Deductions.- 8. Elimination of Cuts in PA*.- § 29. Proof of Well-Ordering.- 1. A Constructive Proof of Well-Ordering for Subsystems of ?(?).- 2. The Formal System ID n of n-Fold Iterated Inductive Definitions.- 3. Formalization of the Proof of Well-Ordering of ?(N) in IDN.- 4. Embedding IDn in a Subsystem of PA.