Proof theory

Author(s)

• Schütte, K. (Kurt)

Bibliographic Information

Proof theory

Kurt Schütte ; translation from the German by J.N. Crossley

（Die Grundlehren der mathematischen Wissenschaften, Bd. 225）

Springer-Verlag, 1977

• : gw
• : us

Other Title

Beweistheorie

Note

Translation of Beweistheorie, rev. ed. Originally published as Beweistheorie: Berlin : Springer, 1960. (Die Grundlehren der mathematischen Wissenschaften ; Bd. 103)

Bibliography: p. [293]-296

Includes index

Description and Table of Contents

Table of Contents

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.

by "Nielsen BookData"

Details

• NCID: BA01358976
• ISBN:
  • 3540079114
  • 0387079114
• LCCN: 76045768
• Country Code: gw
• Title Language Code: eng
• Text Language Code: eng
• Original Language Code: ger
• Place of Publication: Berlin ; New York
• Pages/Volumes: xii, 302 p.
• Size: 25 cm
• Classification:
  • LCC : QA9.54
  • DC : 511/.3
• Subject Headings:
  • LCSH : Proof theory
• Parent Bibliography ID:
  • BA00007422