Table of Contents

Acknowledgments vii

A history of logic 1

A Patterns of reasoning 2

A.1 Reductio ad absurdum 2

A.2 Aristotle 3

A.3 Other patterns and later developments 8

B A language and its meaning 9

B.1 Early semantic observations and problems 10

B.2 The Scholastic theory of supposition 11

B.3 Intension vs. extension 11

B.4 Modalities 12

C A symbolic language 14

C.1 The "universally characteristic language" 15

C.2 Calculus of reason 15

D 1850-1950 - mathematical logic 17

D.1 George Boole 18

D.2 Gottlob Frege 22

D.3 Set theory 25

D.4 20th century logic 27

E Modern symbolic logic 29

E.1 Formal logical systems: Syntax 30

E.2 Formal semantics 34

E.3 computability and decidability 37

F Summary 41

The Greek alphabet 42

Part I Elements of set theory 43

1 Sets, functions, relations 45

1.1 Sets and functions 45

1.2 Relations 52

1.3 Ordering relations 54

1.4 Infinities 56

Exercises 63

2 Induction 65

2.1 Well-founded orderings 65

2.1.1 Inductive proofs 68

2.2 Inductive definitions 73

2.2.1 "1-1" Definitions 77

2.2.2 Recursive programming [optional] 79

2.2.3 Proofs by structural induction 82

2.3 Transfinite induction [optional] 88

Exercises 90

Part II Turing machines 93

3 Computability and decidability 95

3.1 Alphabets and languages 95

3.2 Turing machines 97

3.2.1 Composing Turing machines [optional] 103

3.3 Universal Turing machine 105

3.4 Undecidability 108

Exercises 112

Part III Propositional logic 115

4 Syntax and proof systems 117

4.1 Axiomatic systems 117

4.2 Propositional syntax 123

4.3 Hilbert's axiomatic system H 124

4.4 The axiomatic system N 127

4.5 H vs. N 129

4.6 Provable equivalence 130

4.7 Consistency 132

4.8 Gentzen's axiomatic system G 133

4.8.1 Decidability of PL 134

4.8.2 Rules for abbreviated connectives 136

4.9 Some proof techniques 136

Exercises 137

5 Semantics of PL 139

5.1 The Boolean semantics 139

5.1.1 Syntactic abbreviations 146

5.2 Semantic properties 147

5.2.1 Some propositional laws 148

5.3 Set-based semantics 149

5.3.1 Sets and propositions 150

5.3.2 Boolean algebras [optional] 153

Exercises 155

6 Soundness and completeness 159

6.1 Expressive completeness 159

6.2 Disjunctive and Conjunctive normal form 162

6.2.1 CNF, clauses and satisfiability [optional] 163

6.3 Soundness 166

6.4 Completeness 170

6.5 Some applications 174

Exercises 175

Part IV First order logic 181

7 Syntax and proof systems of FOL 183

7.1 Syntax of FOL 185

7.2 Scope of quantifiers 188

7.2.1 Some examples 190

7.2.2 Substitution 193

7.3 The axiomatic system N 195

7.3.1 Deduction Theorem in FOL 197

7.4 Gentzen's system for FOL 199

Exercises 201

8 Semantics op FOL 205

8.1 The basic definitions 205

8.2 Semantic properties 212

8.3 Open vs. closed formulae 213

8.3.1 Deduction Theorem in G and H 216

Exercises 218

9 More semantics 221

9.1 Prenex normal form 221

9.1.1 Levy hierarchy 225

9.2 Substructures: An example of model theory 226

9.3 "Syntactic" semantics 229

9.3.1 Reachable and term structures 230

9.3.2 Herbrand's theorem 235

9.3.3 Horn clauses 236

9.3.4 Herbrand models of Horn theories 238

9.3.5 Computing with Horn clauses 239

9.3.6 Computational completeness 241

Exercises 243

10 Soundness and completeness 245

10.1 Soundness of N 245

10.2 Completeness of N 246

10.3 Completeness of Gentzen's system [optional] 252

10.4 Some applications 254

Exercises 258

Why is first order logic "first order"? 261

Index 265