Издательство Cambridge University Press, 1996, -353 pp.
The discovery of the set-theoretic paradoxes around the tu of the century, and the resulting uncertainties and doubts conceing the use of high-level abstractions among mathematicians, led D. HUbert to the formulation of his programme: to prove the consistency of axiomatizations of the essential parts of mathematics by methods which might be considered as evident and reliable because of their elementary combinatorial ("finitistic") character.
Although, by Godel's incompleteness results, Hilbert's programme could not be carried out as originally envisaged, for a long time variations of Hilbert's programme have been the driving force behind the development of proof theory. Since the programme called for a complete formalization of the relevant parts of mathematics, including the logical steps in mathematical arguments, interest in proofs as combinatorial structures in their own right was awakened. This is the subject of structural proof theory; its true beginnings may be dated from the publication of the landmark-paper Gentzen [1935].
Nowadays there are more reasons, besides Hilbert's programme, for studying structural proof theory. For example, automated theorem proving implies an interest in proofs as combinatorial structures; and in logic programming, formal deductions are used in computing.
There are several monographs on proof theory (Schiitte [1960,1977], Takeuti [1987], Pohlers [1989]) inspired by Hilbert's programme and the questions this engendered, such as "measuring" the strength of subsystems of analysis in terms of provable instances of transfinite induction for definable well- orderings (more precisely, ordinal notations). Pohlers [1989] is particularly recommended as an introduction to this branch of proof theory.
Girard [1987b] presents a wider panorama of proof theory, and is not easy reading for the beginner, though recommended for the more experienced.
The present text attempts to fill a lacuna in the literature, a gap which exists between introductory books such as Heindorf [1994], and textbooks on mathematical logic (such as the classic Kleene [1952a], or the recent van Dalen [1994]) on the one hand, and the more advanced monographs mentioned above on the other hand.
Our text concentrates on the structural proof theory of first-order logic and its applications, and compares different styles of formalization at some length. A glimpse of the proof theory of first-order arithmetic and second-order logic is also provided, illustrating techniques in relatively simple situations which are applied elsewhere to far more complex systems.
As preliminary knowledge on the part of the reader we assume some familiarity with first-order logic as may be obtained from, for example, van Dalen [1994]. A slight knowledge of elementary recursion theory is also helpful, although not necessary except for a few passages. Locally, other preliminary knowledge will be assumed, but this will be noted explicitly.
Introduction.
N-systems and H-systems.
Gentzen systems.
Cut elimination with applications.
Refinements.
Normalization for natural deduction.
Resolution.
Categorical logic.
Modal and linear logic.
Proof theory of arithmetic.
Second-order logic.
The discovery of the set-theoretic paradoxes around the tu of the century, and the resulting uncertainties and doubts conceing the use of high-level abstractions among mathematicians, led D. HUbert to the formulation of his programme: to prove the consistency of axiomatizations of the essential parts of mathematics by methods which might be considered as evident and reliable because of their elementary combinatorial ("finitistic") character.
Although, by Godel's incompleteness results, Hilbert's programme could not be carried out as originally envisaged, for a long time variations of Hilbert's programme have been the driving force behind the development of proof theory. Since the programme called for a complete formalization of the relevant parts of mathematics, including the logical steps in mathematical arguments, interest in proofs as combinatorial structures in their own right was awakened. This is the subject of structural proof theory; its true beginnings may be dated from the publication of the landmark-paper Gentzen [1935].
Nowadays there are more reasons, besides Hilbert's programme, for studying structural proof theory. For example, automated theorem proving implies an interest in proofs as combinatorial structures; and in logic programming, formal deductions are used in computing.
There are several monographs on proof theory (Schiitte [1960,1977], Takeuti [1987], Pohlers [1989]) inspired by Hilbert's programme and the questions this engendered, such as "measuring" the strength of subsystems of analysis in terms of provable instances of transfinite induction for definable well- orderings (more precisely, ordinal notations). Pohlers [1989] is particularly recommended as an introduction to this branch of proof theory.
Girard [1987b] presents a wider panorama of proof theory, and is not easy reading for the beginner, though recommended for the more experienced.
The present text attempts to fill a lacuna in the literature, a gap which exists between introductory books such as Heindorf [1994], and textbooks on mathematical logic (such as the classic Kleene [1952a], or the recent van Dalen [1994]) on the one hand, and the more advanced monographs mentioned above on the other hand.
Our text concentrates on the structural proof theory of first-order logic and its applications, and compares different styles of formalization at some length. A glimpse of the proof theory of first-order arithmetic and second-order logic is also provided, illustrating techniques in relatively simple situations which are applied elsewhere to far more complex systems.
As preliminary knowledge on the part of the reader we assume some familiarity with first-order logic as may be obtained from, for example, van Dalen [1994]. A slight knowledge of elementary recursion theory is also helpful, although not necessary except for a few passages. Locally, other preliminary knowledge will be assumed, but this will be noted explicitly.
Introduction.
N-systems and H-systems.
Gentzen systems.
Cut elimination with applications.
Refinements.
Normalization for natural deduction.
Resolution.
Categorical logic.
Modal and linear logic.
Proof theory of arithmetic.
Second-order logic.