This book on methods of cut-elimination contains a thorough and rigorous analysis of reductive cut-elimination methods and an in-depth presentation of the recent method CERES developed by the authors. It includes a detailed complexity analysis and comparison of CERES and of reductive methods. It presents several applications of CERES—to interpolation, fast cut-elimination, generalization of proofs and to the analysis of mathematical proofs. Finally, it provides an extension of CERES to non-classical logics, in particular to finitely-valued logics and to Gödel logic.
Methods of Cut-Elimination
TRENDS IN LOGIC Studia Logica Library VOLUME 34 Managing Editor Ryszard Wójcicki, Institute of Philosophy and Sociology, Polish Academy of Sciences, Warsaw, Poland Editors Wieslaw Dziobiak, University of Puerto Rico at Mayagüez, USA Melvin Fitting, City University of New York, USA Vincent F. Hendricks, Department of Philosophy and Science Studies, Roskilde University, Denmark Daniele Mundici, Department of Mathematics “Ulisse Dini”, University of Florence, Italy Ewa Orłowska, National Institute of Telecommunications, Warsaw, Poland Krister Segerberg, Department of Philosophy, Uppsala University, Sweden Heinrich Wansing, Institute of Philosophy, Dresden University of Technology, Germany
SCOPE OF THE SERIES Trends in Logic is a bookseries covering essentially the same area as the journal Studia Logica – that is, contemporary formal logic and its applications and relations to other disciplines. These include artificial intelligence, informatics, cognitive science, philosophy of science, and the philosophy of language. However, this list is not exhaustive, moreover, the range of applications, comparisons and sources of inspiration is open and evolves over time. Volume Editor Heinrich Wansing
For further volumes: http://www.springer.com/series/6645
Matthias Baaz · Alexander Leitsch
Methods of Cut-Elimination
123
Matthias Baaz Vienna University of Technology Wiedner Hauptstraße 8-10 1040 Vienna Austria
[email protected]
Alexander Leitsch Vienna University of Technology Favoritenstraße 9 1040 Vienna Austria
[email protected]
ISBN 978-94-007-0319-3 e-ISBN 978-94-007-0320-9 DOI 10.1007/978-94-007-0320-9 Springer Dordrecht Heidelberg London New York c Springer Science+Business Media B.V. 2011 No part of this work may be reproduced, stored in a retrieval system, or transmitted in any form or by any means, electronic, mechanical, photocopying, microfilming, recording or otherwise, without written permission from the Publisher, with the exception of any material supplied specifically for the purpose of being entered and executed on a computer system, for exclusive use by the purchaser of the work. Printed on acid-free paper Springer is part of Springer Science+Business Media (www.springer.com)
Contents 1 Preface 1.1 The History of This Book . . . . . . . . . . . . . . . . . . . . 1.2 Potential Readers of This Book . . . . . . . . . . . . . . . . . 1.3 How to Read This Book . . . . . . . . . . . . . . . . . . . . .
1 1 1 2
2 Introduction
5
3 Preliminaries 3.1 Formulas and Sequents . . . . . . . . . . . . . . . . . . . . . . 3.2 The Calculus LK . . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Unification and Resolution . . . . . . . . . . . . . . . . . . . .
9 9 14 24
4 Complexity of Cut-Elimination 39 4.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 4.2 Proof Complexity and Herbrand Complexity . . . . . . . . . 44 4.3 The Proof S