Proof Methods for Modal and Intuitionistic Logics
"Necessity is the mother of invention. " Part I: What is in this book - details. There are several different types of formal proof procedures that logicians have invented. The ones we consider are: 1) tableau systems, 2) Gentzen sequent calculi, 3) natura
- PDF / 31,881,616 Bytes
- 563 Pages / 439.911 x 666.559 pts Page_size
- 32 Downloads / 222 Views
SYNTHESE LIBRARY
STUDIES IN EPISTEMOLOGY, LOGIC, METHODOLOGY, AND PHILOSOPHY OF SCIENCE
Managing Editor: JAAKKO HINTIKKA, Florida State University, Tallahassee
Editors: DONALD DAVIDSON, University of California GABRIEL NUCHELMANS, University of Leyden WESLEY C. SALMON, University of Pittsburgh
VOLUME 169
MELVIN FITTING Herbert H. Lehman College of the City University of New York
PROOF METHODS FOR MODA L AND INTUITIONISTIC LOGICS
.....
SPRINGER-SCIENCE+BUSINESS MEDIA, B.V .
''
Library of Congress Cataloging in Publication Data Fitting, Melvin Chris. Proof methods for modal and intuitionistic logics. (Synthese library; v. 169) Bibliography: p. Includes index. 1. Proof theory. 2. Modality (Logic) 3. Intuitionistic mathematics. 1. Title. QA9.54.F57 1983 511.3 83-4409 ISBN 978-90-481-8381-4 ISBN 978-94-017-2794-5 (eBook) DOI 10.1007/978-94-017-2794-5
Ali Rights Reserved Copyright © 1983 by SpringerScience+BusinessMediaDordrecht Originally pub1ished by D. Reide1 Pub1isbing Company, Dordrecbt, Holland in 1983 No part of the material protected by this copyright notice may be reproduced or utilized in any form or by any means, electronic or mechanical, including photocopying, recording or by any information storage and retrieval system, without written permission from the copyright owner
TABLE OF CONTENTS
1
INTRODUCTION CHAPTER ONE I BACKGROUND
1. 2. 3. 4.
Propositional Formulas Models A Unifying Notation Classical Semantic Tableaus
11 14 22 29
CHAPTER TWO I ANALYTIC MODAL TABLEAUS AND CONSISTENCY PROPERTIES
1. 2. 3. 4. 5. 6.
Tableau Rules for K, K4, T, S4, D and D4 Uniform Modal Notation Correctness A Note on Completeness Proofs Consistency Properties forK, K4, T, S4, D and D4 Tableau Completeness
33 41 43 46 48 60
CHAPTER THREE I LOGICAL CONSEQUENCE, COMPACTNESS, INTERPOLATION, AND OTHER TOPICS
1. 2.
3.
4. 5. 6. 7. 8.
9. 10. 11. 12.
Introduction Logical Consequence Strong Tableau Completeness Compactness Theorems The Deduction Theorem Gentzen Systems Symmetric Gentzen Systems The Craig Interpolation Lemma Other Interpolation Theorems The Beth Definability Theorem Further Consequences of Interpolation Theorems Decidability
v
64 65 70 74 77 81 88
93 99 105 110 115
vi
TABLE OF CONTENTS CHAPTER FOUR
I AXIOM SYSTEMS AND NATURAL DEDUCTION
1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13. 14. 15. 16.
Introduction A Classical Propositional Axiom System An Underlying Modal Logic Results about the Logic U The Logic K Axiomatized Correctness and Completeness of the K Axiomatization The Logics K4, T, S4, D and D4 Axiomatization Finite Axiomatizability, Part I Finite Axiomatizability, Part II A Classical Natural Deduction System Some Results about Natural Deduction A Note on Modal Natural Deduction Rules 1-style Natural Deduction Rules 1-style Completeness and Correctness A-style Natural Deduction Rules A-style Completeness and Correctness CHAPTER FIVE
118 118 123 127 130 134 137 141 148 153 162 170 171 176 184 187
I NON-ANALYTIC LOGICS
1. Introduction 2. Synthetic KB, DB, B and S5 Tableaus 3. Semi-
