Proof Analysis: A Contribution to Hilbert's Last Problem

by Negri, Sara; Von Plato, Jan

• ISBN13: 9781107008953
• ISBN10: 1107008956
• Edition: 1st
• Format: Hardcover
• Copyright: 2011-11-21
• Publisher: Cambridge Univ Pr

Summary

This book continues from where the authors' previous book, Structural Proof Theory, ended. It presents an extension of the methods of analysis of proofs in pure logic to elementary axiomatic systems and to what is known as philosophical logic. A self-contained brief introduction to the proof theory of pure logic is included that serves both the mathematically and philosophically oriented reader. The method is built up gradually, with examples drawn from theories of order, lattice theory and elementary geometry. The aim is, in each of the examples, to help the reader grasp the combinatorial behaviour of an axiom system, which typically leads to decidability results. The last part presents, as an application and extension of all that precedes it, a proof-theoretical approach to the Kripke semantics of modal and related logics, with a great number of new results, providing essential reading for mathematical and philosophical logicians.

Table of Contents

Preface	p. ix
Prologue: Hilbert's last problem	p. 1
Introduction	p. 3
The idea of a proof	p. 3
Proof analysis: an introductory example	p. 4
Outline	p. 9
Proof Systems Based on Natural Deduction
Rules of proof: natural deduction	p. 17
Natural deduction with general elimination rules	p. 17
Normalization of derivations	p. 23
From axioms to rules of proof	p. 29
The theory of equality	p. 32
Predicate logic with equality and its word problem	p. 35
Notes to Chapter 2	p. 37
Axiomatic systems	p. 39
Organization of an axiomatization	p. 39
Relational theories and existential axioms	p. 46
Notes to Chapter 3	p. 49
Order and lattice theory	p. 50
Order relations	p. 50
Lattice theory	p. 52
The word problem for groupoids	p. 57
Rule systems with eigenvariables	p. 62
Notes to Chapter 4	p. 67
Theories with existence axioms	p. 68
Existence in natural deduction	p. 68
Theories of equality and order again	p. 71
Relational lattice theory	p. 73
Notes to Chapter 5	p. 82
Proof Systems Based on Sequent Calculus
Rules of proof: sequent calculus	p. 85
From natural deduction to sequent calculus	p. 85
Extensions of sequent calculus	p. 97
Predicate logic with equality	p. 106
Herbrand's theorem for universal theories	p. 110
Notes to Chapter 6	p. 111
Linear order	p. 113
Partial order and Szpilrajn's theorem	p. 113
The word problem for linear order	p. 119
Linear lattices	p. 123
Notes to Chapter 7	p. 128
Proof Systems for Geometric Theories
Geometric theories	p. 133
Systems of geometric rules	p. 133
Proof theory of geometric theories	p. 138
Barr's theorem	p. 144
Notes to Chapter 8	p. 145
Classical and intuitionistic axiomatics	p. 147
The duality of classical and constructive notions and proofs	p. 147
From geometric to co-geometric axioms and rules	p. 150
Duality of dependent types and degenerate cases	p. 155
Notes to Chapter 9	p. 156
Proof analysis in elementary geometry	p. 157
Projective geometry	p. 157
Affine geometry	p. 173
Examples of proof analysis in geometry	p. 180
Notes to Chapter 10	p. 181
Proof Systems for Non-Classical Logics
Modal logic	p. 185
The language and axioms of modal logic	p. 185
Kripke semantics	p. 187
Formal Kripke semantics	p. 189
Structural properties of modal calculi	p. 193
Decidability	p. 201
Modal calculi with equality, undefinability results	p. 210
Completeness	p. 213
Notes to Chapter 11	p. 219
Quantified modal logic, provability logic, & other non-classical logics	p. 222
Adding the quantifiers	p. 222
Provability logic	p. 234
Intermediate logics	p. 239
Substructural logics	p. 249
Notes to Chapter 12	p. 251
Bibliography	p. 254
Index of names	p. 262
Index of subjects	p. 264
Table of Contents provided by Ingram. All Rights Reserved.