Basic Proof Theory ( Cambridge Tracts in Theoretical Computer Science )

Publication series ：Cambridge Tracts in Theoretical Computer Science

Author： A. S. Troelstra; H. Schwichtenberg

Publisher： Cambridge University Press‎

Publication year： 2000

E-ISBN: 9781316044537

P-ISBN(Paperback): 9780521779111

Subject： O141.2 proof theory

Keyword：一般性问题

Language： ENG

Access to resources Favorite

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Basic Proof Theory

Description

This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included.

Chapter

1.2 Simple type theories

1.3 Three types of formalism

N-systems and H-systems

2.1 Natural deduction systems

2.2 Ni as a term calculus

2.3 The relation between C, I and M

2.4 Hilbert systems

2.5 Notes

Gentzen systems

3.1 The G1- and G2-systems

3.2 The Cut rule

3.3 Equivalence of G- and N-systems

3.4 Systems with local rules

3.5 Absorbing the structural rules

3.6 The one-sided systems for C

3.7 Notes

Cut elimination with applications

4.1 Cut elimination

4.2 Applications of cutfree systems

4.3 A more efficient calculus for Ip

4.4 Interpolation and definable functions

4.5 Extensions of G1-systems

4.6 Extensions of G3-systems

4.7 Logic with equality

4.8 The theory of apartness

4.9 Notes

Bounds and permutations

5.1 Numerical bounds on cut elimination

5.2 Size and cut elimination

5.3 Permutation of rules for classical logic

5.4 Permutability of rules for Gli

5.5 Notes

Normalization for natural deduction

6.1 Conversions and normalization

6.2 The structure of normal derivations

6.3 Normality in G-systems and N-systems

6.4 Extensions with simple rules

6.5 E-logic and ordinary logic

6.6 Conservativity of predicative classes

6.7 Conservativity for Horn clauses

6.8 Strong normalization for →Nm and λ→

6.9 Hyperexponential bounds

6.10 A digression: a stronger conversion

6.11 Orevkov's result

6.12 Notes

Resolution

7.1 Introduction to resolution

7.2 Unification

7.3 Linear resolution

7.4 From Gentzen system to resolution

7.5 Resolution for Ip

7.6 Notes

Categorical logic

8.1 Deduction graphs

8.2 Lambda terms and combinators

8.3 Decidability of equality

8.4 A coherence theorem for CCC's

8.5 Notes

Modal and linear logic

9.1 The modal logic S4

9.2 Embedding intuitionistic logic into S4

9.3 Linear logic

9.4 A system with privileged formulas

9.5 Proofnets

9.6 Notes

Proof theory of arithmetic

10.1 Ordinals below ε₀

10.2 Provability of initial cases of TI

10.3 Normalization with the omega rule

10.4 Unprovable initial cases of TI

10.5 TI for non-standard orderings

10.6 Notes

Second-order logic

11.1 Intuitionistic second-order logic

11.2 Ip² and λ2

11.3 Strong normalization for Ni²

11.4 Encoding of λ2Ωinto λ2

11.5 Provably recursive functions of HA²

11.6 Notes

Solutions to selected exercises

Bibliography

Symbols and notations

Index

The users who browse this book also browse

Description

Chapter

The users who browse this book also browse

No browse record.