An introduction to proof theory : normalization, cut-elimination, and consistency proofs / Paolo Mancosu, Sergio Galvan, Richard Zach.

Format:

Book

Author/Creator:

Mancosu, Paolo, author.

Galvan, Sergio, 1946- author.

Zach, Richard, author.

Contributor:

Edward Potts Cheyney Memorial Fund.

Language:

English

Subjects (All):

Proof theory.

Physical Description:

xii, 418 pages ; 24 cm

Edition:

First edition.

Place of Publication:

Oxford ; New York, NY : Oxford University Press, 2021.

Summary:

An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details of proofs worked out and examples and exercises to aid the reader's understanding.

Contents:

Machine generated contents note: 1. Introduction

1.1. Hilbert's consistency program

1.2. Gentzen's proof theory

1.3. Proof theory after Gentzen

2. Axiomatic calculi

2.1. Propositional logic

2.2. Reading formulas as trees

2.3. Sub-formulas and main connectives

2.4. Logical calculi

2.5. Inference rules

2.6. Derivations from assumptions and provability

2.7. Proofs by induction

2.8. The deduction theorem

2.9. Derivations as trees

2.10. Negation

2.11. Independence

2.12. An alternative axiomatization of J0

2.13. Predicate logic

2.14. The deduction theorem for the predicate calculus

2.15. Intuitionistic and classical arithmetic

3. Natural deduction

3.1. Introduction

3.2. Rules and deductions

3.3. Natural deduction for classical logic

3.4. Alternative systems for classical logic

3.5. Measuring deductions

3.6. Manipulating deductions, proofs about deductions

3.7. Equivalence of natural and axiomatic deduction

4. Normal deductions

4.1. Introduction

4.2. Double induction

4.3. Normalization for [ ̂], [⊃], -, A

4.4. The sub-formula property

4.5. The size of normal deductions

4.6. Normalization for NJ

4.7. An example

4.8. The sub-formula property for NJ

4.9. Normalization for NK

5. The sequent calculus

5.1. The language of the sequent calculus

5.2. Rules of LK

5.3. Constructing proofs in LK

5.4. The significance of CUT

5.5. Examples of proofs

5.6. Atomic logical axioms

5.7. Lemma on variable replacement

5.8. Translating NJ to LJ

5.9. Translating LJ to NJ

6. The cut-elimination theorem

6.1. Preliminary definitions

6.2. Outline of the lemma

6.3. Removing Mixes directly

6.4. Reducing the degree of mix

6.5. Reducing the rank

6.6. Reducing the rank: example

6.7. Reducing the degree: example

6.8. Intuitionistic sequent calculus LJ

6.9. Why MIX?

6.10. Consequences of the Hauptsatz

6.11. The mid-sequent theorem

7. The consistency of arithmetic

7.1. Introduction

7.2. Consistency of simple proofs

7.3. Preliminary details

7.4. Overview of the consistency proof

7.5. Replacing inductions

7.6. Reducing suitable cuts

7.7. A first example

7.8. Elimination of weakenings

7.9. Existence of suitable curs

7.10. A simple example

7.11. Summary

8. Ordinal notations and induction

8.1. Orders, well-orders, and induction

8.2. Lexicographical orderings

8.3. Ordinal notations up to ε0

8.4. Operations on ordinal notations

8.5. Ordinal notations are well-ordered

8.6. Set-theoretic definitions of the ordinals

8.7. Constructing ε0 from below

8.8. Ordinal arithmetic

8.9. Trees and Goodstein sequences

9. The consistency of arithmetic, continued

9.1. Assigning ordinal notations < ε0 to proofs

9.2. Eliminating inductions from the end-part

9.3. Removing weakenings

9.4. Reduction of suitable cuts

9.5. A simple example, revisited

A. The Greek alphabet

B. Set-theoretic notation

C. Axioms, rules, and theorems of axiomatic calculi

C.1. Axioms and rules of inference

C.2. Theorems and derived rules

D. Exercises on axiomatic derivations

D.1. Hints for Problem 2.7

D.2. Hints for Problem 2.18

D.3. Exercises with quantifiers

E. Natural deduction

E.1. Inference rules

E.2. Conversions

F. Sequent calculus

G. Outline of the cut-elimination theorem.

Notes:

Includes bibliographical references and index.

Local Notes:

Acquired for the Penn Libraries with assistance from the Edward Potts Cheyney Memorial Fund.

ISBN:

9780192895943

019289594X

9780192895936

0192895931

OCLC:

1241731958

Publisher Number:

99988991233