Logic as a Tool

Preface xi

Acknowledgements xv

Introduction xvii

An Appetizer: Logical Paradoxes and Self-Reference 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 well-founded 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 Resolution-based derivations 80

2.5.4 Optimizing the method of resolution 82

2.6 Supplementary: The Boolean satisfiability problem and NP-completeness 86

2.7 Supplementary: Completeness of the propositional deductive systems 88

3 Understanding First-order Logic 96

3.1 First-order structures and languages: terms and formulae of first-order logic 97

3.1.1 First-order structures 97

3.1.2 First-order languages 99

3.1.3 Terms and formulae 100

3.2 Semantics of first-order logic 108

3.2.1 The semantics of first-order logic: an informal outline 108

3.2.2 Interpretations of first-order languages 111

3.2.3 Variable assignment and evaluation of terms 112

3.2.4 Truth of first-order formulae 112

3.2.5 Evaluation games 114

3.2.6 Translating first-order formulae to natural language 117

3.3 Basic grammar and use of first-order languages 123

3.3.1 Translation from natural language to first-order languages: warm-up 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 first-order logic 135

3.4.1 More on truth of sentences in structures: models and counter-models 135

3.4.2 Satisfiability and validity of first-order formulae 136

3.4.3 Logical consequence in first-order logic 137

3.4.4 Using equality in first-order logic 140

3.4.5 Logical equivalence in first-order logic 142

3.4.6 Logical equivalences involving quantifiers 143

3.4.7 Negating first-order formulae: negation normal form 144

3.5 Syllogisms 151

4 Deductive Reasoning in First-order Logic 159

4.1 Axiomatic system for first-order 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 first-order logic 167

4.2.1 Some derivations in Semantic Tableaux 168

4.2.2 Semantic Tableaux for first-order logic with equality 171

4.2.3 Discussion on the quantifier rules and on termination 173

4.3 Natural Deduction for first-order logic 180

4.3.1 Natural Deduction rules for the quantifiers 180

4.3.2 Derivations in first-order Natural Deduction 181

4.3.3 Natural Deduction for first-order 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 first-order logic 194

4.5.1 Propositional Resolution rule in first-order 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 first-order logic 197

4.5.5 Examples of resolution-based derivations 199

4.5.6 Resolution for first-order 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 first-order logic 210

4.6.1 First-order 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 first-order 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