GRADUATE TEXTS IN COMPUTER SCIENCE A/agarandPeriyasamy, Specification of Software Systems AptandO/derog, Verification of Sequential and Concurrent Programs, Second Edition Backandvon Wright, Refinement Calculus Fitting, First-Order Logic and Automated Theorem Proving, Second Edition Immerman, Descriptive Complexity Liand Vitanyi, An Introduction to Kolmogorov CompleXity and Its Applications, Second Edition Munakata, Fundamentals ofthe New Artificial Intelligence Nerode andShore, Logic for Applications, Second Edition Schneider, On Concurrent Programming Smith, A Recursive Introduction to the Theory of Computation Socher-Ambrosius andJohann, Deduction Systems.
Anii Nerode Richard A. Shore Department of Mathematics Cornell University White Hali Ithaca, NY 14853-7901 USA Seri es Editors David Gries Fred B. Schneider Department of Computer Science Cornell University Upson Hali Ithaca, NY 14853-7501 USA Library of Congress Cataloging-in-Publicatlon Data Nerode, Anii, 1932- Logic for applications I Anii Nerode and Richard A. Shore p. cm. - (Graduate texts in computer seienee) Ineludes bibliographieal references and index. ISBN 978-14612-6855-0 ISBN 978-14612-0649-1 (eBook) DOI 10.1007/978-14612-0649-1 1. Computer science-Mathematics. 2. Logic, Symbolic and mathematical. 1. Shore, Richard A., 1946- II. Title. III. Series. OA76.9.M35N47 1997 005.1 '01 'S113-de20 9643297 Printed on acid-Iree paper. © 1997 Springer Seience+Business Media New York Originally published by Springer-Verlag New York, Ine. in 1997 Softcover reprint of the hardcover 2nd edition 1997 AII rights reserved. 111is work may not be translated or copied in whole or in part without the written permission of the publisher Springer-Science+Business Media, LLC, except for brief excerpts in connection with reviews or scholarly analysis. Use in connection with any form of information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed is forbidden. 111e use of general descriptive names, trade names, trademarks, etc., in this publication, even il the former are noi especially identified, is not ta be taken as a sign that such names, as understood by the Trade Marks and Merchandise Marks Act, may accordingly be used freely by anyone. Production managed by Victoria Evarretta; manulacturlng supervised by Jacqui Ashri. Photocomposed copy prepared Irom the authors' LaTeX fIles. 9876543 ISBN 978-14612.Q855-0 .
Preface In writing this book, our goal was to produce a text suitable for a first course in mathematical logic more attuned than the traditional textbooks to the re cent dramatic growth in theapplications oflogic to computerscience. Thus, our choice oftopics has been heavily influenced by such applications. Ofcourse, we cover the basic traditional topics: syntax, semantics, soundnes5, completeness and compactness as well as a few more advanced results such as the theoremsof Skolem-Lowenheim and Herbrand. Muchofour book, however, deals with other less traditional topics. Resolution theorem proving plays a major role in our treatment oflogic especially in its application to Logic Programming and PRO LOG. Wedealextensivelywiththemathematicalfoundations ofall threeofthese subjects. In addition, we include two chapters on nonclassical logics - modal and intuitionistic - that are becoming increasingly important in computer sci ence. We develop the basic material on the syntax and semantics (via Kripke frames) for each of these logics. In both cases, our approach to formal proofs, soundness and completeness uses modifications ofthe same tableau method in troduced for classical logic. We indicate how it can easily be adapted to various other special types ofmodal logics. A number ofmore advanced topics (includ ing nonmonotonic logic) arealso brieflyintroduced both in the nonclassicallogic chapters and in the material on Logic Programming and PROLOG.
vi Preface devoted to homework problems and programming instruction. Alternatively, the materialon resolution theorem proving and Logic Programmingcan be replaced bythechapterson modal and intuitionistic logictoget a rather different course.
Preface vii :- '0 :-~--: :-< "'_ I . _ I :-< 0-::"'---' ~---;",-,--';"" I a, 'I tv I7I ----r'-I ,I ,I , I I , I , , , , I I , :i:'-. I , J:\=/'"=. ;:= ;:= ? =' ----- ----'P----9' - ~ ~/r 6 // ;:=--: ~ ,:/ ;=: ~'~;/l ~~!/ " I I I ,:<'/~ ------_:-< ;:= I a, 00 -.I I I I I I I I.
viii Preface systematictableauxin1.4. Similarly, the materialon set-theoretic procedures in Chapter VI (new in this edition) can be covered at any point. Only one section (§6) assumes a familiarity with predicate logic and that issimplyto list a formal version ofthe axioms. In this chapter, §§1-5 and §7 contain the basic set theory needed for this book and most undergraduate courses. The remaining sections, §§8-11, develop the theory ofinfinite (and even uncountable) ordinals, cardinals and transfinite recursion including some versions of the axiom of choice. This material should suffice as a background in set theory for most graduate courses in mathematics and computer science but is not used in the rest ofthis book.