Logic in Computer Science (Hantao Zhang, Jian Zhang) (z-library.sk, 1lib.sk, z-lib.sk)

Logic in Computer Science Hantao Zhang · Jian Zhang

Logic in Computer Science

Hantao Zhang • Jian Zhang Logic in Computer Science

Hantao Zhang Department of Computer Science University of Iowa Iowa City, IA, USA Jian Zhang Institute of Software Chinese Academy of Sciences Beijing, China ISBN 978-981-97-9815-5 ISBN 978-981-97-9816-2 (eBook) https://doi.org/10.1007/978-981-97-9816-2 © The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025 This work is subject to copyright. All rights are solely and exclusively licensed by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. This Springer imprint is published by the registered company Springer Nature Singapore Pte Ltd. The registered company address is: 152 Beach Road, #21-01/04 Gateway East, Singapore 189721, Singapore If disposing of this product, please recycle the paper.

Preface Mathematical logic is an important basis for mathematics, computer Science, and artificial intelligence. The application of logic as a problem-solving tool is an important aspect of education of computer scientists and engineers. This book provides a comprehensive introduction to various logics, including the classical propositional logic and first-order predicate logic, as well as equational logic, temporal logic, and Hoare logic. The focus of the book is to present algorithms in the form of proof procedures for the classical logics and decision procedures for checking the satisfiability of logical formulas. A large portion of the book is devoted to the introduction of software tools based on these algorithms and the practical problems which can be solved by these tools in constraint satisfaction, formal verification, and artificial intelligence. The book assumes no background in logic. It is appropriate for (junior and senior) undergraduate and graduate students majoring in computer science or mathematics. Each chapter has about a dozen or so exercises to help the reader understand the materials. The first chapter of the book is a general introduction of logic (with a bias toward mathematical logic) and the notions to be used through the book. The rest of the book is divided into four parts: • Part I: Propositional logic, Chaps. 2–4 • Part II: First-order logic, Chaps. 5–7 • Part III: Logic in Programming, Chaps. 8–10 • Part IV: Logic of Computability, Chaps. 11 and 12 The topics of this book were chosen from the field of logic with a focus on the algorithmic aspect of logic. We have selected only most effective algorithms from the field. We did not list all the important references to these topics as they are rarely needed for the beginners and can be found easily on the internet. We thank all the original contributors of these contents, including research papers and software tools, and hope they will forgive us for not listing them all. v

vi Preface This book also contains some original materials: • In Chap. 5, we show that the set definition by a first-order formula is an interesting application of first-order logic, where the defined set is a special model of the formula. If the set is a new entity (type or sort), the set itself is the extensional definition of the entity and the formula is its intentional definition. • A new presentation of an almost-linear time unification algorithm in Chap. 6. • In Chap. 8, we introduce the notions of first-termination and last termination of Prolog programs. • An interpretation of Gödel’s incompleteness theorems in terms of Turing machines is given in Chap. 11. • Also in Chap. 11, a new concept of “computably countable” is shown to be equivalent to computable or recursively enumerable, and is the result of adding computability to countability. • In Chap. 12, we pointed out that Deepak Kapur’s ground congruence algorithm can be simplified by using only “splitting,” that is, “flattening” is optional. Without the help from many friends, colleagues, and our families, there would be no printing of this book. The authors thank everyone who helped one way or the other. This book grew out of notes from a course titled “Logic in Computer Science” at the University of Iowa. The first author taught this course many times. Students in his course used these notes as textbooks and provided good feedback. We apologize for not listing their names here. We thank Cesare Tinelli for introducing this course to Iowa, Zubair Shafiq for using an early version of this book in teaching this course, and Alberto Segre for the support when the first author expressed the idea of converting the notes into a textbook. We also thank Clark Barrett, Pascal Fontaine, and Cesare Tinelli for permitting us to use a figure of SMT-LIB in this book. We wish to thank the teachers and colleagues who enriched the authors’ knowledge on the topics of the book. The first author thanks Jean-Luc Rémy, Pierre Lescanne, Jean-Pierre Jouannoud, Hélène Kirchner, Claude Kirchner, and Michael Rusinowitch for making the oversea life enjoyable for a new graduate student to study rewrite systems. The first author is grateful to his thesis advisor, Deepak Kapur, for supporting and directing his research on automated induction and ordered resolution within rewrite systems. The second author is grateful to his thesis advisors, Yunmei Dong and C.S. Tang, from whom he learned about formal specifications, rewrite systems, and temporal logic. We also thank the colleagues who worked with us on many topics of the book. They are Peter Baumgartner, Frank Bennett, Maria Paola Bonaciana, Jieh Hsiang, Emmanual Kounalis, William McCune, Mark Stickel, to name a few. Many people read different versions of the draft, and provided us with useful comments and suggestions. We are grateful to all of them, including Shaowei Cai, Wenjian Chai, Yuhang Dong, Rui Han, Jiangang Huang, Fuqi Jia, Changwen Li, Tian Liu, Yongmei Liu, Kunhang Lv, Zongyan Qiu, Yidong Shen, Langchen Shi, Yuefei Sui, Sicheng Tan, Bohua Zhan, Wenhui Zhang, Yu Zhang, Chunlai Zhou, and Xueyang Zhu. Special thanks go to Tian Liu, who provided a very good technique

Preface vii for proving a language is unrecognizable and whose comments lead to the concept of “computably countable” in Chap. 11. It has been a pleasure to work with the folks at Springer Nature in creating the final product. We mention Celine Lanlan Chang, Sudha Ramachandran, and Kamesh Senthilkumar because we have had the most contact with them, but we know that many others have been involved, too. We would also like to thank the National Science Foundation of China (NSFC) for its continuous support. Finally, we would like to thank deeply our families for their patience, inspiration, and love. The first author is grateful in particular to his son, Roy, and daughter, Felice, for comments and proofreading of the book, and his wife, Ling Rao, for logistic of writing the book. This book is dedicated to Ling. Iowa City, IA, USA Hantao Zhang Beijing, China Jian Zhang August 2024

Contents 1 Introduction to Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1 Logic Is Everywhere . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.1.1 Statement or Proposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.1.2 A Brief History of Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.1.3 Thinking or Writing Logically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2 Logical Fallacies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.2.1 Formal Fallacies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.2.2 Informal Fallacies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.3 A Glance of Mathematical Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.3.1 Set Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.3.2 Computability Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.3.3 Model Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 1.3.4 Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Part I Propositional Logic 2 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.1.1 Logical Operators. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.1.2 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2.2.1 Interpretations. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2.2.2 Models, Satisfiability, and Validity . . . . . . . . . . . . . . . . . . . . . . . . 41 2.2.3 Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 2.2.4 Entailment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 2.2.5 Theorem Proving and the SAT Problem . . . . . . . . . . . . . . . . . . . 47 2.3 Normal Forms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 2.3.1 Negation Normal Form (NNF) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 2.3.2 Conjunctive Normal Form (CNF) . . . . . . . . . . . . . . . . . . . . . . . . . 51 ix

x Contents 2.3.3 Disjunctive Normal Form (DNF) . . . . . . . . . . . . . . . . . . . . . . . . . . 53 2.3.4 Full DNF and Full CNF from Truth Table . . . . . . . . . . . . . . . . 54 2.3.5 Binary Decision Diagram (BDD) . . . . . . . . . . . . . . . . . . . . . . . . . . 55 2.4 Optimization Problems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 2.4.1 Minimum Set of Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 2.4.2 Logic Minimization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 2.4.3 Maximum Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 2.5 Using Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 2.5.1 Bitwise Operators. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 2.5.2 Decision Problems in Propositional Logic . . . . . . . . . . . . . . . . 68 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 3 Reasoning in Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 3.1 Proof Procedures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 3.1.1 Types and Styles of Proof Procedures . . . . . . . . . . . . . . . . . . . . . 80 3.1.2 Semantic Tableau . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 3.1.3 α-Rules and β-Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 3.2 Deductive Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 3.2.1 Inference Rules and Proofs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 3.2.2 Hilbert System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 3.2.3 Natural Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 3.2.4 Inference Graphs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 3.3 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 3.3.1 Resolution Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 3.3.2 Resolution Strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 3.3.3 Preserving Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 3.3.4 Completeness of Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 3.3.5 A Resolution-Based Decision Procedure . . . . . . . . . . . . . . . . . . 102 3.3.6 Simplification Strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 3.4 Boolean Constraint Propagation (BCP) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 3.4.1 BCP: A Simplification Procedure . . . . . . . . . . . . . . . . . . . . . . . . . . 106 3.4.2 A Decision Procedure for Horn Clauses. . . . . . . . . . . . . . . . . . . 108 3.4.3 Unit Resolution Versus Input Resolution . . . . . . . . . . . . . . . . . . 109 3.4.4 Head/Tail Literals for BCP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 4 Propositional Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 4.1 The DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 4.1.1 Recursive Version of DPLL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 4.1.2 All-SAT and Incremental SAT Solvers . . . . . . . . . . . . . . . . . . . . 123 4.1.3 BCPw: Use of Watch Literals in DPLL . . . . . . . . . . . . . . . . . . . . 124 4.1.4 Iterative Implementation of DPLL . . . . . . . . . . . . . . . . . . . . . . . . . 127 4.2 Conflict-Driven Clause Learning (CDCL) . . . . . . . . . . . . . . . . . . . . . . . . . . 128 4.2.1 Generating Clauses from Conflicting Clauses. . . . . . . . . . . . . 129

Contents xi 4.2.2 DPLL with CDCL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 4.2.3 Unsatisfiable Cores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 4.2.4 Random Restart . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 4.2.5 Branching Heuristics for DPLL. . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 4.3 Use of SAT Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 4.3.1 Specify SAT Instances in DIMACS Format . . . . . . . . . . . . . . . 138 4.3.2 Sudoku Puzzle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 4.3.3 Latin Square Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140 4.3.4 Graph Problems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141 4.4 Maximum Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143 4.4.1 2SAT Versus Max2SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143 4.4.2 Weighted and Hybrid MaxSAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 4.4.3 Local Search Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 4.4.4 The Branch-and-Bound Algorithm . . . . . . . . . . . . . . . . . . . . . . . . 149 4.4.5 Use of Hybrid MaxSAT Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . 154 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 Part II First-Order Logic 5 First-Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 5.1 Syntax of First-Order Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 5.1.1 Terms and Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162 5.1.2 Quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165 5.1.3 Unsorted and Many-Sorted Logic . . . . . . . . . . . . . . . . . . . . . . . . . 167 5.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 5.2.1 Interpretation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 5.2.2 Models, Satisfiability, and Validity . . . . . . . . . . . . . . . . . . . . . . . . 173 5.2.3 Equivalence and Entailment. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 5.2.4 Set Constructions and Many-Sorted Logic . . . . . . . . . . . . . . . . 179 5.2.5 First-Order Logic Versus Higher-Order Logic . . . . . . . . . . . . 182 5.3 Proof Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184 5.3.1 Semantic Tableau . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185 5.3.2 Natural Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 5.4 Conjunctive Normal Form (CNF) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188 5.4.1 Prenex Normal Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188 5.4.2 Skolemization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190 5.4.3 Clausal Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200 6 Unification and Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201 6.1 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201 6.1.1 Substitutions and Unifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202 6.1.2 Combining Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203 6.1.3 Rule-Based Unification. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204

xii Contents 6.1.4 Practically Linear Time Unification Algorithm . . . . . . . . . . . 207 6.2 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213 6.2.1 Formal Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213 6.2.2 Factoring . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215 6.2.3 A Refutational Proof Procedure. . . . . . . . . . . . . . . . . . . . . . . . . . . . 215 6.3 Simplification Orders and Ordered Resolution . . . . . . . . . . . . . . . . . . . . . 217 6.3.1 Well-Founded Partial Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217 6.3.2 Simplification Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219 6.3.3 Completeness of Ordered Resolution . . . . . . . . . . . . . . . . . . . . . . 224 6.4 Prover9: A Resolution Theorem Prover . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 6.4.1 Input Formulas to Prover9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 6.4.2 Inference Rules and Options . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229 6.4.3 Simplification Orders in Prover9. . . . . . . . . . . . . . . . . . . . . . . . . . . 231 6.4.4 The TPTP Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 235 7 First-Order Logic with Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 7.1 Equality of Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 7.1.1 Axioms of Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 238 7.1.2 Semantics of “=” . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 239 7.1.3 Theory of Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241 7.2 Rewrite Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243 7.2.1 Rewrite Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 244 7.2.2 Termination of Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246 7.2.3 Confluence of Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247 7.2.4 The Knuth-Bendix Completion Procedure . . . . . . . . . . . . . . . . 248 7.2.5 Special Rewrite Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255 7.3 Inductive Theorem Proving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259 7.3.1 Inductive Theorems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259 7.3.2 Structural Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 261 7.3.3 Induction on Two Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 263 7.3.4 Many-Sorted Algebraic Specification . . . . . . . . . . . . . . . . . . . . . 264 7.3.5 Recursion, Induction, and Self-Reference . . . . . . . . . . . . . . . . . 268 7.4 Resolution with Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 269 7.4.1 Paramodulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 270 7.4.2 Simplification Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271 7.4.3 Equality in Prover9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 273 7.5 Finite Model Finding in First-Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . 275 7.5.1 Mace4: A Finite Model Finding Tool. . . . . . . . . . . . . . . . . . . . . . 275 7.5.2 Finite Model Finding by SAT Solvers . . . . . . . . . . . . . . . . . . . . . 278 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 280 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 283

Contents xiii Part III Logic in Programming 8 Prolog: Programming in Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 287 8.1 Prolog’s Working Principle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 287 8.1.1 Horn Clauses in Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 288 8.1.2 Resolution Proof in Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289 8.1.3 A Goal-Reduction Procedure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 291 8.2 Prolog’s Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 295 8.2.1 Atoms, Numbers, and Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . 296 8.2.2 Compound Terms and Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 297 8.2.3 Popular Predicates over Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 298 8.2.4 Sorting Algorithms in Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 300 8.3 Recursion in Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 301 8.3.1 Program Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 302 8.3.2 Focused Recursion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 304 8.3.3 Tail Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 305 8.3.4 A Prolog Program for N -Queen Puzzle . . . . . . . . . . . . . . . . . . . 306 8.4 Beyond Clauses and Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 307 8.4.1 The Cut Operator “!” . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 307 8.4.2 Negation as Failure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 309 8.4.3 Beyond Clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 310 8.4.4 Variations and Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 312 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 313 9 Hoare Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 315 9.1 Formal Verification of Computer Systems . . . . . . . . . . . . . . . . . . . . . . . . . . 315 9.1.1 Verification of Imperative Programs . . . . . . . . . . . . . . . . . . . . . . . 316 9.1.2 Verification of Functional Programs . . . . . . . . . . . . . . . . . . . . . . . 317 9.2 Hoare Triples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 318 9.2.1 Hoare Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 320 9.2.2 Examples of Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . . . 325 9.2.3 Partial and Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 328 9.3 Automated Generation of Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 329 9.3.1 Verification Conditions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 330 9.3.2 Proof of Theorem 9.3.4. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 332 9.3.3 Implementing V C in Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 336 9.4 Obtaining Good Loop Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 340 9.4.1 Invariants from Generalizing Postconditions . . . . . . . . . . . . . . 341 9.4.2 Program Synthesis from Invariants . . . . . . . . . . . . . . . . . . . . . . . . 343 9.4.3 Choosing A Good Language for Assertions. . . . . . . . . . . . . . . 345 9.4.4 Verification Tools for Conventional Languages . . . . . . . . . . . 347 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 348 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 349

xiv Contents 10 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 351 10.1 An Approach from Modal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 352 10.1.1 Modal Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 352 10.1.2 Kripke Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 353 10.1.3 Restrictions and Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 357 10.2 Linear Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 358 10.2.1 Timeline as Interpretation Sequence . . . . . . . . . . . . . . . . . . . . . . . 359 10.2.2 Properties of LTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 362 10.2.3 Model Checking with Kripke Frames . . . . . . . . . . . . . . . . . . . . . 364 10.3 Semantic Tableaux for LTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 366 10.3.1 Rules for Modal Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 367 10.3.2 Deciding Satisfiability by Tableaux. . . . . . . . . . . . . . . . . . . . . . . . 370 10.4 Binary Temporal Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 377 10.4.1 The until and release Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . 377 10.4.2 The weak until and strong release Operators . . . . . . . . . . . . . . 380 10.4.3 Extension of Semantic Tableau . . . . . . . . . . . . . . . . . . . . . . . . . . . . 381 10.5 Verification of Concurrent Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 381 10.5.1 Model Checking with Finite State Machines . . . . . . . . . . . . . . 382 10.5.2 Properties of Concurrent Programs . . . . . . . . . . . . . . . . . . . . . . . . 384 10.5.3 The BAKERY(2) Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 384 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 389 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 392 Part IV Logic of Computability 11 Decidable and Undecidable Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 395 11.1 A Bit of History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 395 11.1.1 Gödel’s Incompleteness Theorems . . . . . . . . . . . . . . . . . . . . . . . . 395 11.1.2 Three Well-Known Computing Models . . . . . . . . . . . . . . . . . . . 397 11.1.3 Halting Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 398 11.2 Turing Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 398 11.2.1 Formal Definition of Turing Machines . . . . . . . . . . . . . . . . . . . . 400 11.2.2 High-Level Description of Turing Machines . . . . . . . . . . . . . . 404 11.2.3 Recognizable Versus Decidable. . . . . . . . . . . . . . . . . . . . . . . . . . . . 405 11.3 Decidability of Problems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 406 11.3.1 Encoding of Decision Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . 406 11.3.2 Decidable Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 408 11.3.3 Undecidable Problems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410 11.3.4 Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 412 11.3.5 Rice’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 416 11.4 Computability of Counting Bijections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 418 11.4.1 Properties of Counting Bijections . . . . . . . . . . . . . . . . . . . . . . . . . 419 11.4.2 Equivalence of Recognizable and Recursively Enumerable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 420

Contents xv 11.4.3 Equivalence of Recognizable and Computably Countable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 11.4.4 Identifying Unrecognizable Languages . . . . . . . . . . . . . . . . . . . 424 11.5 Turing Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 426 11.5.1 Turing Completeness of Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427 11.5.2 Turing Completeness of Rewrite Systems . . . . . . . . . . . . . . . . . 429 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 431 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 432 12 Decision Procedures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 433 12.1 DPLL(T ): Extend DPLL with Theories T . . . . . . . . . . . . . . . . . . . . . . . . . . 435 12.1.1 Propositional Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 435 12.1.2 Examples of DPLL(T ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 438 12.1.3 DPLLT(X): An Algorithm of DPLL(T ) . . . . . . . . . . . . . . . . . . 440 12.2 Equality with Uninterpreted Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 442 12.2.1 Uninterpreted Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 442 12.2.2 The Congruence Closure Problem . . . . . . . . . . . . . . . . . . . . . . . . . 443 12.2.3 The NOS Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 445 12.2.4 Ground Congruence by Completion . . . . . . . . . . . . . . . . . . . . . . . 448 12.3 Linear Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453 12.3.1 Simplex Method by Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 454 12.3.2 The Simplex Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 458 12.3.3 Linear Programming. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 460 12.3.4 Integer Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 461 12.3.5 Difference Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 463 12.4 Making DPLL(T ) Practical . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 465 12.4.1 Making DPLL(T ) Efficient . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 465 12.4.2 Combination of Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 468 12.4.3 SMT-LIB: A Library of SMT Problems . . . . . . . . . . . . . . . . . . . 471 12.4.4 SMT-COMP: Competition of SMT Solvers . . . . . . . . . . . . . . . 472 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 475 Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477

About the Authors Hantao Zhang is Professor of Computer Science with the University of Iowa, USA. His research interests include automated reasoning, constraint solving, and discrete mathematics. He is the recipient of numerous NSF awards, including the prestigious NSF Young Investigator Award. He has published more than 100 papers in these areas, including a book on automated mathematical induction and a book chapter for the Handbook of Satisfiability. He won the Skolem Award by CADE (International Conference on Automated Deduction) in 2015 as his paper on SATO has passed the test of time as one of the most influential papers in the field. Jian Zhang is a researcher with the Institute of Software, Chinese Academy of Sciences, and a professor with the University of Chinese Academy of Sciences. His research interests include automated reasoning, constraint solving, program analysis, and software testing. Jian Zhang serves on the editorial boards of several journals including IEEE Transactions on Reliability, Journal of Computer Science and Technology, Frontiers of Computer Science, Science China – Information Sciences, and Chinese Journal of Computers. He is the author of Deciding the Satisfiability of Logical Formulas—Methods, Tools and Applications (in Chinese, Science Press, 2000) and a co-author of Automatic Generation of Combinatorial Test Data (Springer, 2014). xvii

Chapter 1 Introduction to Logic Do you like to solve Sudoku puzzles? If so, how long will it take on average to solve a Sudoku puzzle appearing in a newspaper, minutes or hours? An easy exercise in Chap. 1 of this book asks you to write a small program in your favorite language that will solve a Sudoku puzzle, no matter the difficulty, in less than a second on your laptop. Did you ever play the Tower of Hanoi? This puzzle consists of three rods and a number of disks of different sizes, which can slide onto any rod. The puzzle starts with the disks stacked in ascending order of size on one rod, making a conical shape with the smallest at the top. The objective of the puzzle is to move the entire stack to another rod, following three rules: • Only one disk can be moved at a time. • Each move consists of taking the top disk from one of the stacks and placing it on top of another stack or on an empty rod. • No larger disk may be placed on top of a smaller disk. In the illustration figure, the three rods are named a, b, and c (Fig. 1.1). There are three disks initially on rod a, and each disk is named by its size. A solution of the puzzle of moving the disks from rod a to rod b is given as follows: Move disk 1 from a to b Move disk 2 from a to c Move disk 1 from b to c Move disk 3 from a to b Move disk 1 from c to a Move disk 2 from c to b Move disk 1 from a to b This solution was produced by a Prolog program of 3 lines and 168 characters (including commas and periods). The same program can produce solutions for various numbers of disks. Prolog is a programming language based on logic and is introduced in Chap. 8 of the book. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025 H. Zhang, J. Zhang, Logic in Computer Science, https://doi.org/10.1007/978-981-97-9816-2_1 1

2 1 Introduction to Logic Fig. 1.1 Illustration of the Tower of Hanoi The above two examples illustrate that logic is not only a theoretic foundation of computer science but also a problem-solving tool. The emphasis of this book is on how to make this tool efficient and practical. After a rigorous introduction to basic concepts, we will study various algorithms based on logic and introduce software tools which are implementations of these algorithms. To solve a problem using a logic-based tool, you need to think about the problem in logic and specify the problem in logic. This is a skill that needs to be learned like any other, and it does take some training and practice to master this skill. The same skill can be applied to abstract situations such as those encountered in formal proofs. Logic is innate to all of us—indeed, you probably use the laws of logic unconsciously in your everyday speech and in your own internal reasoning. Because logic is innate, the logic principles that we learn should make sense—if you find yourself having to memorize one of the principles in the book, without feeling a mental “click” or comprehending why that law should work, then you will probably not be able to use that principle correctly and effectively in practice. In 1953 Albert Einstein wrote the following in a letter to J. E. Switzer: The development of Western Science has been based on the two great achievements, the invention of the formal logical system (in Euclidean geometry) by the Greek philosophers, and the discovery of the possibility of finding out causal relationships by systematic experiment (at the Renaissance). This book demonstrates the application of these two great achievements of modern science in one setting: developing formal logical systems by systematic experiment. That is, our focus is to convert the algorithms of logical systems into logic tools, and both the algorithms and the tools need systematic experiments. 1.1 Logic Is Everywhere Logic has been called the calculus of computer science, because logic is fundamen- tal in computer science, similar to calculus in the physical and engineering sciences. Logic is used in almost every field of computer science: computer architecture (such as digital gates, hardware verification), software engineering (specification and verification), programming languages (semantics, type theory, abstract data types, object-oriented programming), databases (relational algebra), artificial intelligence

1.1 Logic Is Everywhere 3 (automated theorem proving, knowledge representation), algorithms and theory of computation (complexity, computability), etc. Logic also plays important roles in other fields, such as mathematics, psychology, and philosophy. In mathematics, logic includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics. The unifying themes in mathematical logic include the study of the expressive power of formal systems and the deductive power of formal proof systems. Mathematical logic is further divided into the fields of (a) set theory, (b) model theory, (c) proof theory, and (d) computability theory. These areas share basic results of logic. Symbolic logic in the late nineteenth century and mathematical logic in the twentieth are also called formal logic. Topics traditionally treated by logic but not part of formal logic are often labeled philosophical logic, which deals with arguments in the natural language. Example. Given the premises that (a) “all men are mortal” and (b) “Adam is a man,” we may draw the conclusion that (c) “Adam is mortal,” by the inference rule of modus ponens (Definition 5.3.1). Philosophical logic is the investigation, critical analysis, and intellectual reflection on issues arising in logic. It is the branch of studying questions about reference, predication, identity, truth, quantification, existence, entailment, modality, and necessity. Many of these topics are shared by mathematical logic and discussed in this book. Hence, studying this book will help us be logical in thinking, writing, or conversation. 1.1.1 Statement or Proposition Logic comes from natural languages as most sentences in natural languages are statements or propositions. A proposition is a sentence that expresses a judgment or opinion and has a truth value. We will use statement and assertion as synonyms of proposition. Here are some examples: • The color of the apple is green. • Today is either Monday or Tuesday. • He is a 20-year-old sophomore. Every statement can be either true or false. For instance, the first statement above can be true for one apple but false for another. True or false are called the truth values of a statement. Some sentences in natural languages are not statements, such as commands or exclamatory sentences. For example, “Run fast!” Coach shouts. The first part of the sentence, “Run fast!”, is not a statement; the second part, “Coach shouts,” is a statement. In fact, a sentence is a statement if and only if it has a truth value. In natural languages, we can combine or relate statements with words such as “not” (negation), “and” (conjunction), “or” (disjunction), “if-then” (implication),

4 1 Introduction to Logic etc. That is, a statement can be obtained from other statements by these words. In logic, these words are called logical operators, or equivalently, logical connectives. A statement is composed if it can be expressed as a composition of several simpler statements; otherwise, it is simple. In the above three examples of statements, the first statement is simple; the other two are composed. That is, “today is either Monday or Tuesday” is the composition of “today is Monday” and “today is Tuesday,” using the logical operator “or.” The second sentence, “He is a 20-year-old sophomore,” is the composition of “he is a 20-year-old” and “he is a sophomore,” using the implicit logical operator “and.” We often regard “the color of that apple is not green” as a composed statement: It is the negation of a simple statement. Logical operators are indispensable for expressing the relationship between statements. For example, the following statement is a composition of several simple statements. (∗) If either taxes are not raised or expenditures rise, then the debt ceiling is increased. To see this clearly, we need to introduce symbols, such as t, e, and d, to denote simple statements: 1. t : “taxes are raised” 2. e: “expenditures rise” 3. d: “the debt ceiling is increased” To express that the statement (∗) is composed, let us use these symbols for logical operators: ¬ for negation, ∨ for “either-or,” and → for the “if-then” relation (i.e., implication). Then (∗) becomes the following formula: ((¬t) ∨ e) → d Here each of the symbols t, e and d is called a propositional variable, which denotes a statement, either simple or composed. Naturally, these propositional variables, like statements, can take on only the truth values: true and false. Each propositional variable can be assigned an interpretation or meaning. For instance, the interpretation of t in the above example is “taxes are raised.” Propositional variables are also called Boolean variables after their inventor, the nineteenth century mathematician George Boole. Boolean logic includes any logic in which the considered truth values are true and false. This book studies exclusively Boolean logic. The study of propositional variables with logic operators is called propositional logic, which is the simplest one in the family of Boolean logic. This can be differentiated from probability logic, which is not a Boolean logic because probability values are used to represent various degrees of truth values. Statements which contain subjective adjectives, such as “that apple is delicious,” are better expressed in probability logic, as “delicious” is subjective. Questions regarding the degrees of truth of subjective statements are ignored in Boolean logic. For example, the statement, “that apple is delicious,” can be true in one’s view and false in the other’s. Despite this simplification, or indeed because of it, Boolean logic is

1.1 Logic Is Everywhere 5 scientifically successful. One does not even have to know exactly what the truth values true and false are. 1.1.2 A Brief History of Logic Sophisticated theories of logic were developed in many cultures, including Greece, India, China, and the Islamic world [1]. Greek methods, particularly Aristotelian logic (or term logic), found wide application and acceptance in Western science and mathematics for millennia. Aristotle (384–322 BC) was the first logician to attempt a systematic analysis of logical syntax, of nouns (or terms), and of verbs. He demonstrated the principles of reasoning by employing variables to show the underlying logical form of an argument. He sought relations of dependence which characterize necessary inference, and distinguished the validity of these relations, from the truth of the premises. He was the first to deal in a systematic way with the principles of contradiction, which states that a proposition cannot be both true and false, and excluded the middle, which states that for every proposition, either this proposition or its negation is true. Aristotle has had an enormous influence in Western thought. He developed the theory of syllogism, where three important principles are applied for the first time in history: the use of symbols, a purely formal treatment, and the use of an axiomatic system. Aristotle also developed the theory of fallacies, as a theory of non-formal logic. Another famous ancient Greek logician is Euclid (325–265 BC), who established the foundations of geometry that largely dominated the field until the early nineteenth century. Euclidean geometry is an axiomatic system, in which all theorems are derived from a small number of simple axioms. Euclid’s reasoning from assumptions to conclusions remains valid after the discovery of non-Euclidean geometry. Christian and Islamic philosophers such as Boethius (died 524), Ibn Sina (Avicenna, died 1037), and William of Ockham (died 1347) further developed Aristotle’s logic in the Middle Ages, reaching a high point in the mid-fourteenth century with Jean Buridan (1301–1358/62 AD). In the nineteenth century, attempts to treat the operations of formal logic in a symbolic or algebraic way had been made by philosophical mathematicians, including Leibniz and Lambert, but their works remained isolated and little known. In the beginning of the nineteenth century, logic was studied with rhetoric, through syllogism, and with philosophy. Mathematical logic emerged in the mid- nineteenth century as a field of mathematics independent of the traditional study of logic. The development of modern symbolic logic or mathematical logic during this period by the likes of Boole, Frege, Russell, and Peano is the most significant in the 2000-year history of logic and is arguably one of the most important and remarkable events in human intellectual history.