Logic as a Tool: A Guide to Formal Logical ReasoningISBN: 9781118880005
380 pages
October 2016

Description
Written in a clear, precise and userfriendly style, Logic as a Tool: A Guide to Formal Logical Reasoning is intended for undergraduates in both mathematics and computer science, and will guide them to learn, understand and master the use of classical logic as a tool for doing correct reasoning. It offers a systematic and precise exposition of classical logic with many examples and exercises, and only the necessary minimum of theory.
The book explains the grammar, semantics and use of classical logical languages and teaches the reader how grasp the meaning and translate them to and from natural language. It illustrates with extensive examples the use of the most popular deductive systems  axiomatic systems, semantic tableaux, natural deduction, and resolution  for formalising and automating logical reasoning both on propositional and on firstorder level, and provides the reader with technical skills needed for practical derivations in them. Systematic guidelines are offered on how to perform logically correct and wellstructured reasoning using these deductive systems and the reasoning techniques that they employ.
•Concise and systematic exposition, with semiformal but rigorous treatment of the minimum necessary theory, amply illustrated with examples
•Emphasis both on conceptual understanding and on developing practical skills
•Solid and balanced coverage of syntactic, semantic, and deductive aspects of logic
•Includes extensive sets of exercises, many of them provided with solutions or answers
•Supplemented by a website including detailed slides, additional exercises and solutions
For more information browse the book's website at: https://logicasatool.wordpress.com
Table of Contents
Preface xi
Acknowledgements xv
Introduction xvii
An Appetizer: Logical Paradoxes and SelfReference xxi
1 Understanding Propositional Logic 1
1.1 Propositions and logical connectives: truth tables and tautologies 1
1.1.1 Propositions 1
1.1.2 Propositional logical connectives 2
1.1.3 Truth tables 3
1.1.4 The meaning of the connectives in natural language and in logic 4
1.1.5 Computing truth values of propositions 5
1.1.6 Propositional formulae and their truth tables 6
1.1.7 Tautologies 11
1.2 Propositional logical consequence: logically correct inferences 18
1.2.1 Propositional logical consequence 18
1.2.2 Logically sound rules of propositional inference and logically correct propositional arguments 21
1.2.3 Fallacies of the implication 23
1.3 Logical equivalence: negation normal form of propositional formulae 28
1.3.1 Logically equivalent propositional formulae 28
1.3.2 Basic properties of logical equivalence 29
1.3.3 Some important logical equivalences 29
1.4 Supplementary: Inductive definitions and structural induction and recursion 34
1.4.1 Inductive definitions 34
1.4.2 Induction principles and proofs by induction 36
1.4.3 Basics of the general theory of inductive definitions and principles 37
1.4.4 Inductive definitions and proofs in wellfounded sets 39
1.4.5 Recursive definitions on inductively definable sets 40
2 Deductive Reasoning in Propositional Logic 47
2.1 Deductive systems: an overview 47
2.1.1 The concept and purpose of deductive systems 47
2.1.2 Brief historical remarks on deductive systems 48
2.1.3 Soundness, completeness and adequacy of deductive systems 50
2.2 Axiomatic systems for propositional logic 52
2.2.1 Description 52
2.2.2 Derivations in the axiomatic system H 54
2.3 Semantic Tableaux 58
2.3.1 Description of the deductive system ST of Semantic Tableaux 59
2.3.2 Some derivations in ST 61
2.3.3 Unsigned version of the system of Semantic Tableaux 64
2.4 Natural Deduction 68
2.4.1 Description 69
2.4.2 Examples of derivations in Natural Deduction 71
2.5 Normal forms and Propositional Resolution 77
2.5.1 Conjunctive and disjunctive normal forms of propositional formulae 77
2.5.2 Clausal Resolution 79
2.5.3 Resolutionbased derivations 80
2.5.4 Optimizing the method of resolution 82
2.6 Supplementary: The Boolean satisfiability problem and NPcompleteness 86
2.7 Supplementary: Completeness of the propositional deductive systems 88
3 Understanding Firstorder Logic 96
3.1 Firstorder structures and languages: terms and formulae of firstorder logic 97
3.1.1 Firstorder structures 97
3.1.2 Firstorder languages 99
3.1.3 Terms and formulae 100
3.2 Semantics of firstorder logic 108
3.2.1 The semantics of firstorder logic: an informal outline 108
3.2.2 Interpretations of firstorder languages 111
3.2.3 Variable assignment and evaluation of terms 112
3.2.4 Truth of firstorder formulae 112
3.2.5 Evaluation games 114
3.2.6 Translating firstorder formulae to natural language 117
3.3 Basic grammar and use of firstorder languages 123
3.3.1 Translation from natural language to firstorder languages: warmup 123
3.3.2 Restricted quantification 124
3.3.3 Free and bound variables, and scope of a quantifier 125
3.3.4 Renaming of a bound variable in a formula and clean formulae 127
3.3.5 Substitution of a term for a variable in a formula, and capture of a variable 128
3.3.6 A note on renamings and substitutions in a formula 130
3.4 Logical validity, consequence, and equivalence in firstorder logic 135
3.4.1 More on truth of sentences in structures: models and countermodels 135
3.4.2 Satisfiability and validity of firstorder formulae 136
3.4.3 Logical consequence in firstorder logic 137
3.4.4 Using equality in firstorder logic 140
3.4.5 Logical equivalence in firstorder logic 142
3.4.6 Logical equivalences involving quantifiers 143
3.4.7 Negating firstorder formulae: negation normal form 144
3.5 Syllogisms 151
4 Deductive Reasoning in Firstorder Logic 159
4.1 Axiomatic system for firstorder logic 160
4.1.1 Axioms and rules for the quantifiers 160
4.1.2 Derivations from a set of assumptions 160
4.1.3 Extension of the axiomatic system H with equality 161
4.2 Semantic Tableaux for firstorder logic 167
4.2.1 Some derivations in Semantic Tableaux 168
4.2.2 Semantic Tableaux for firstorder logic with equality 171
4.2.3 Discussion on the quantifier rules and on termination 173
4.3 Natural Deduction for firstorder logic 180
4.3.1 Natural Deduction rules for the quantifiers 180
4.3.2 Derivations in firstorder Natural Deduction 181
4.3.3 Natural Deduction for firstorder logic with equality 183
4.4 Prenex and clausal normal forms 187
4.4.1 Prenex normal forms 187
4.4.2 Skolemization 189
4.4.3 Clausal forms 190
4.5 Resolution for firstorder logic 194
4.5.1 Propositional Resolution rule in firstorder logic 194
4.5.2 Substitutions of terms for variables revisited 195
4.5.3 Unification of terms 196
4.5.4 Resolution with unification in firstorder logic 197
4.5.5 Examples of resolutionbased derivations 199
4.5.6 Resolution for firstorder logic with equality 201
4.5.7 Optimizations and strategies for the method of Resolution 202
4.6 Supplementary: Soundness and completeness of the deductive systems for firstorder logic 210
4.6.1 Firstorder theories 211
4.6.2 Soundness 212
4.6.3 Herbrand structures and interpretations 212
4.6.4 Henkin theories and Henkin extensions 214
4.6.5 Completeness theorem 217
4.6.6 Semantic compactness of firstorder logic 217
5 Applications: Mathematical Proofs and Automated Reasoning 222
5.1 Logical reasoning and mathematical proofs 223
5.1.1 Proof strategies: direct and indirect proofs 223
5.1.2 Tactics for logical reasoning 227
5.2 Logical reasoning on sets, functions, and relations 231
5.2.1 Zermelo–Fraenkel axiomatic theory of sets 231
5.2.2 Basic operations on sets and their properties 234
5.2.3 Functions 236
5.2.4 Binary relations and operations on them 237
5.2.5 Special binary relations 239
5.2.6 Ordered sets 240
5.3 Mathematical Induction and Peano Arithmetic 246
5.3.1 Mathematical Induction 247
5.3.2 Peano Arithmetic 250
5.4 Applications: automated reasoning and logic programming 254
5.4.1 Automated reasoning and automated theorem proving 254
5.4.2 Logic programming and Prolog 255
6 Answers and Solutions to Selected Exercises 263
Answers and solutions: Section 1.1 263
Answers and solutions: Section 1.2 266
Answers and solutions: Section 1.3 268
Answers and solutions: Section 1.4 270
Answers and solutions: Section 2.2 270
Answers and solutions: Section 2.3 272
Answers and solutions: Section 2.4 281
Answers and solutions: Section 2.5 287
Answers and solutions: Section 3.1 293
Answers and solutions: Section 3.2 296
Answers and solutions: Section 3.3 297
Answers and solutions: Section 3.4 299
Answers and solutions: Section 3.5 305
Answers and solutions: Section 4.1 306
Answers and solutions: Section 4.2 308
Answers and solutions: Section 4.3 325
Answers and solutions: Section 4.4 328
Answers and solutions: Section 4.5 329
Answers and solutions: Section 4.6 338
Answers and solutions: Section 5.1 339
Answers and solutions: Section 5.2 339
Answers and solutions: Section 5.3 344
Answers and solutions: Section 5.4 347
References 348
Index 351