×

zbMATH — the first resource for mathematics

Proof analysis. A contribution to Hilbert’s last problem. (English) Zbl 1247.03001
Cambridge: Cambridge University Press (ISBN 978-1-107-00895-3/hbk; 978-1-107-41723-6/pbk; 978-1-139-00351-3/ebook). xi, 265 p. (2011).
This is a sequel to the authors’ book [Structural proof theory. Cambridge: Cambridge University Press (2001; Zbl 1113.03051)] and analyses formal proofs. The modern formulation of logic starts from logical axioms (like \(A\&B\to A\)) and proceeds linearly by using modus ponens and universalization. This is not very amenable to proof analysis. It was Gentzen who changed (formal) axioms into rules, and obtained brilliant results such as the cut-elimination theorem. But when mathematical axioms are involved, they are simply left as assumptions with no attempt at analysis. The authors endeavor to turn such axioms into rules in order to analyse proofs. Another object of analysis is nonclassical logics. The authors incorporate Kripke semantics into formal systems, and gain much perspicuity.
What kind of axioms (i.e., formulas) can be turned into rules? Certainly, not all of them. A pretty comprehensive class the authors arrive at is the geometric axioms: namely, universal closures of \(A\to B\), where \(\forall\), \(\neg\), and \(\rightarrow\) do not occur in \(A\) or \(B\). Universal axioms are (equivalent to) geometric ones, and some existence axioms (e.g., existence of three non-collinear points) in good formulations are geometric. The authors show eliminability of weakening, contraction, and cut rules in many cases, and the Herbrand theorem with a proviso. Proofs can be arranged: mathematical inference first, propositional next, and quantificational last. Hence, the word problem (i.e., the derivability of an atomic formula from other atomic formulas) comes into the scope of this work. There, the sub-term property must be established. Other applications include: non-derivability of the parallel line axiom of Euclid from others, Whitman’s theorem in lattice theory, and (the logic version of) Barr’s theorem of topos theory.
The book proceeds in a leisurely fashion, starting from natural deduction, then sequent calculus, before treating geometric axioms. It includes concrete axiomatic theories such as equality, order, lattice, groupoid, projective and affine geometries. A number of word problems are solved, including those of groupoids (without associativity) and of free lattices. (But those are simple cases. It will be nice and significant if this kind of analysis can explain why the word problem for one-relator groups is solvable [W. Magnus, J. Reine Angew. Math. 163, 141–165 (1930; JFM 56.0134.03)] and it is unsolvable in general; see, e.g., [W. W. Boone, Ann. Math. (2) 70, 207–265 (1959; Zbl 0102.00902)].)
For modal logics, the authors incorporate semantics into formal systems in the following manner. There are three kinds of formulas: \(wRo\) (from the world \(w\), one can reach the world \(o\)), \(a\in D(w)\) (\(a\) belongs to the domain of \(w\)), and \(w\):\(A\) (\(w\) forces \(A\)). The nature of frames is formalized as rules about \(R\), and modal axioms are turned into rules. Correspondence between the nature of frames and modal axioms becomes nothing but mutual derivability of rules. Eliminability of structural rules, and (semantic) completeness are shown. In this approach, comparisons of modal systems and intermediate logics are done systematically and easily. Geometric conditions for frames are shown to be responsible for interpolation in a number of logics. Very impressibly, a cut-free system for provability logic is established by means of a new notion, ‘range of a world’.
Hilbert’s last problem (24th) in the subtitle of this book has recently been discovered – state the authors; it asks “to develop a theory of proof methods in mathematics”. Certainly, this book is a considerable “contribution” to the problem.
The authors provide a 5\({1\over 2}\) page chapter-by-chapter description of the contents. They use bold-faced type in a wise and strategic way. There are only few typo-errors. Somewhat grave is that the cut rule is missing from Table 6.3, p. 89.

MSC:
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03F03 Proof theory, general (including proof-theoretic semantics)
03F07 Structure of proofs
03D40 Word problems, etc. in computability and recursion theory
03B30 Foundations of classical theories (including reverse mathematics)
PDF BibTeX XML Cite
Full Text: DOI