Logics for Computer Science : Classical and Non-Classical

Providing an in-depth introduction to fundamental classical and non-classical logics, this textbook offers a comprehensive survey of logics for computer scientists. Logics for Computer Science contains intuitive introductory chapters explaining the need for logical investigations, motivations for different types of logics and some of their history. They are followed by strict formal approach chapters. All chapters contain many detailed examples explaining each of the introduced notions and definitions, well chosen sets of exercises with carefully written solutions, and sets of homework. While many logic books are available, they were written by logicians for logicians, not for computer scientists. They usually choose one particular way of presenting the material and use a specialized language. Logics for Computer Science discusses Gentzen as well as Hilbert formalizations, first order theories, the Hilbert Program, Godel's first and second incompleteness theorems and their proofs. It also introduces and discusses some many valued logics, modal logics and introduces algebraic models for classical, intuitionistic, and modal S4 and S5 logics. The theory of computation is based on concepts defined by logicians and mathematicians. Logic plays a fundamental role in computer science, and this book explains the basic theorems, as well as different techniques of proving them in classical and some non-classical logics. Important applications derived from concepts of logic for computer technology include Artificial Intelligence and Software Engineering. In addition to Computer Science, this book may also find an audience in mathematics and philosophy courses, and some of the chapters are also useful for a course in Artificial Intelligence. Contents 6 1 Introduction: Paradoxes and Puzzels 10 1.1 Mathematical Paradoxes 10 1.2 Computer Science Puzzles 16 1.2.1 Reasoning About Knowledge in Distributed Systems 17 1.2.2 Reasoning in Artificial Intelligence 18 1.3 Homework Problems 21 2 Introduction to Classical Logic 23 2.1 Propositional Language: Motivation and Description 24 2.2 Propositional Semantics: Motivation and Description 29 2.3 Examples of Propositional Tautologies 38 2.4 Predicate Language Description and Application to ArtificialIntelligence 45 2.5 Predicate Semantics: Description and Laws of Quantifiers 57 2.6 Homework Problems 66 3 Propositional Semantics: Classical and Many Valued 72 3.1 Formal Propositional Languages 72 3.2 Extensional Semantics M 82 3.3 Classical Semantics 87 3.3.1 Tautologies: Decidability and Verification Methods 96 3.3.2 Sets of Formulas: Consistency and Independence 105 3.4 Classical Tautologies and Equivalence of Languages 108 3.5 Many Valued Semantics: Łukasiewicz, Heyting, Kleene,Bohvar 116 3.6 M Tautologies, M Consistency, and M Equivalenceof Languages 133 3.7 Homework Problems 144 4 General Proof Systems: Syntax and Semantics 151 4.1 Syntax 153 4.1.1 Consequence Operation 164 4.1.2 Syntactic Consistency 169 4.2 Semantics 170 4.3 Exercises and Examples 177 4.4 Homework Problems 182 5 Hilbert Proof Systems Completeness of ClassicalPropositional Logic 184 5.1 Deduction Theorem 185 5.1.1 Formal Proofs 197 5.2 Completeness Theorem: Proof One 205 5.2.1 Examples 211 5.3 Completeness Theorem: Proof Two 216 5.4 Some Other Axiomatizations 227 5.5 Exercises 230 5.6 Homework Problems 234 6 Automated Proof Systems Completeness of Classical Propositional Logic 238 6.1 Gentzen Style Proof System RS 238 6.2 Search for Proofs and Decomposition Trees 246 6.3 Strong Soundness and Completeness 257 6.4 Proof Systems RS1 and RS2 261 6.5 Gentzen Sequent Systems GL, G, LK 268 6.5.1 Gentzen Sequent Systems GL and G 269 6.6 GL Soundness and Completeness 282 6.7 Original Gentzen Systems LK, LI Completeness and Hauptzatz Theorems 288 6.8 Homework Problems 307 7 Introduction to Intuitionistic and Modal Logics 310 7.1 Introduction to Intuitionistic Logic 310 7.1.1 Philosophical Motivation 311 7.1.2 Algebraic Intuitionistic Semantics andCompleteness Theorem 313 7.1.3 Algebraic Semantics and Completeness Theorem 314 7.1.4 Connection Between Classical and IntuitionisticTautologies 320 7.2 Gentzen Sequent System LI 322 7.2.1 Decomposition Trees in LI 325 7.2.2 Proof Search Examples 328 7.2.3 Proof Search Heuristic Method 337 7.3 Introduction to Modal S4 and S5 Logics 340 7.3.1 Algebraic Semantics for S4 and S5 344 7.3.2 S4 and Intuitionistic Logic, S5 and Classical Logic 349 7.4 Homework Problems 351 8 Classical Predicate Semantics and Proof Systems 354 8.1 Formal Predicate Languages 354 8.2 Classical Semantics 369 8.3 Predicate Tautologies 385 8.3.1 Equational Laws of Quantifiers 389 8.4 Hilbert Proof Systems Soundness and Completeness 397 8.5 Homework Problems 402 9 Hilbert Proof Systems Completeness of ClassicalPredicate Logic 406 9.1 Reduction Predicate Logic to Propositional Logic 407 9.1.1 Henkin Method 413 9.2 Proof of Completeness Theorem 424 9.3 Deduction Theorem 435 9.4 Some Other Axiomatizations 440 9.5 Homework Problems 445 10 Predicate Automated Proof Systems Completeness ofClassical Predicate Logic 446 10.1 QRS Proof System 447 10.2 QRS Decomposition Trees 452 10.2.1 Examples of Decomposition Trees 454 10.3 Proof of QRS Completeness 461 10.4 Skolemization and Clauses 471 10.4.1 Prenex Normal Forms and Skolemization 474 10.4.2 Clausal Form of Formulas 486 10.5 Homework Problems 490 11 Formal Theories and Gödel Theorems 493 11.1 Formal Theories: Definition and Examples 494 11.2 PA: Formal Theory of Natural Numbers 504 11.3 Consistency, Completeness,Gödel Theorems 519 11.3.1 Hilbert's Conservation and Consistency Programs 523 11.3.2 Gödel Incompleteness Theorems 525 11.4 Proof of the Incompleteness Theorems 530 11.4.1 The Formalized Completeness Theorem 535 11.5 Homework Problems 538 The theory of computation is based on concepts defined by logicians and mathematicians. Logic plays a fundamental role in computer science, and this book explains the basic theorems, as well as different techniques of proving them in classical and some non-classical logics. Important applications derived from concepts of logic for computer technology include Artificial Intelligence and Software Engineering. Providing an in-depth introduction to fundamental classical and non-classical logics, this textbook offers a comprehensive survey of logics for computer scientists. Logics for Computer Science contains intuitive introductory chapters explaining the need for logical investigations, motivations for different types of logics and some of their history. They are followed by strict formal approach chapters. All chapters contain many detailed examples explaining each of the introduced notions and definitions, well chosen sets of exercises with carefully written solutions, and sets of homework. Includes links to the author's companion lecture slides for each chapter: several hundred presentations which summarize the ideas presented in the chapters for ease of comprehension Front Matter ....Pages I-X Introduction: Paradoxes and Puzzels (Anita Wasilewska)....Pages 1-13 Introduction to Classical Logic (Anita Wasilewska)....Pages 15-63 Propositional Semantics: Classical and Many Valued (Anita Wasilewska)....Pages 65-143 General Proof Systems: Syntax and Semantics (Anita Wasilewska)....Pages 145-177 Hilbert Proof Systems Completeness of Classical Propositional Logic (Anita Wasilewska)....Pages 179-232 Automated Proof Systems Completeness of Classical Propositional Logic (Anita Wasilewska)....Pages 233-304 Introduction to Intuitionistic and Modal Logics (Anita Wasilewska)....Pages 305-348 Classical Predicate Semantics and Proof Systems (Anita Wasilewska)....Pages 349-400 Hilbert Proof Systems Completeness of Classical Predicate Logic (Anita Wasilewska)....Pages 401-440 Predicate Automated Proof Systems Completeness of Classical Predicate Logic (Anita Wasilewska)....Pages 441-487 Formal Theories and Gödel Theorems (Anita Wasilewska)....Pages 489-535