A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity

Contents......Page 4
What is logic?......Page 8
Time complexity......Page 9
Sets and structures......Page 11
Functions......Page 13
1.1 What is propositional logic?......Page 16
1.2 Validity, satisfiability, and contradiction......Page 22
1.3 Consequence and equivalence......Page 24
1.4 Formal proofs......Page 27
1.5 Proof by induction......Page 37
1.5.1 Mathematical induction......Page 38
1.5.2 Induction on formula complexity......Page 40
1.6 Normal forms......Page 42
CNF algorithm......Page 45
1.7 Horn formulas......Page 47
Horn algorithm......Page 48
1.8.1 Clauses......Page 52
1.8.2 Resolvents......Page 53
1.8.3 Completeness of resolution......Page 55
1.9 Completeness and compactness......Page 59
Exercises......Page 63
2.1 The language of first-order logic......Page 68
2.2 The syntax of first-order logic......Page 69
2.3 Semantics and structures......Page 72
2.4.1 Graphs......Page 81
2.4.2 Relational databases......Page 84
2.4.3 Linear orders......Page 85
2.4.4 Number systems......Page 87
2.5 The size of a structure......Page 88
2.6 Relations between structures......Page 94
2.6.1 Embeddings......Page 95
2.6.2 Substructures......Page 98
2.6.3 Diagrams......Page 101
2.7 Theories and models......Page 104
Exercises......Page 106
3. Proof theory......Page 114
3.1 Formal proofs......Page 115
3.2.1 Conjunctive prenex normal form......Page 124
3.2.2 Skolem normal form......Page 126
3.3.1 Herbrand structures......Page 128
3.3.2 Dealing with equality......Page 131
3.3.3 The Herbrand method......Page 133
3.4 Resolution for first-order logic......Page 135
3.4.1 Unification......Page 136
The unification algorithm......Page 137
3.4.2 Resolution......Page 139
3.5 SLD resolution......Page 143
3.6 Prolog......Page 152
Exercises......Page 157
4.1 The countable case......Page 162
4.2 Cardinal knowledge......Page 167
4.2.1 Ordinal numbers......Page 168
4.2.2 Cardinal arithmetic......Page 171
4.2.3 Continuum hypotheses......Page 176
4.3 Four theorems of first-order logic......Page 178
4.4 Amalgamation of structures......Page 185
4.5 Preservation of formulas......Page 189
4.5.1 Supermodels and submodels......Page 190
4.5.2 Unions of chains......Page 194
4.6 Amalgamation of vocabularies......Page 198
4.7 The expressive power of first-order logic......Page 204
Exercises......Page 208
5. First-order theories......Page 213
5.1 Completeness and decidability......Page 214
5.2 Categoricity......Page 220
5.3.1 Dense linear orders......Page 226
5.3.2 Ryll-Nardzewski et al.......Page 229
5.4 The random graph and 0-1 laws......Page 231
5.5 Quantifier elimination......Page 236
5.5.1 Finite relational vocabularies......Page 237
5.5.2 The general case......Page 243
5.6 Model-completeness......Page 248
5.7 Minimal theories......Page 254
5.8 Fields and vector spaces......Page 262
5.9 Some algebraic geometry......Page 272
Exercises......Page 274
6.1 Types......Page 282
6.2 Isolated types......Page 286
6.3 Small models of small theories......Page 290
6.3.1 Atomic models......Page 291
6.3.2 Homegeneity......Page 292
6.3.3 Prime models......Page 294
6.4 Big models of small theories......Page 295
6.4.1 Countable saturated models......Page 296
6.4.2 Monster models......Page 300
6.5 Theories with many types......Page 301
6.6 The number of nonisomorphic models......Page 304
6.7 A touch of stability......Page 305
Hierachy of first-order theories......Page 308
Exercises......Page 310
7. Computability and complexity......Page 314
7.1 Computable functions and Church\'s thesis......Page 316
7.1.1 Primitive recursive functions......Page 317
7.1.2 The Ackermann function......Page 322
7.1.3 Recursive functions......Page 324
7.2 Computable sets and relations......Page 327
7.3 Computing machines......Page 331
7.4 Codes......Page 335
7.5 Semi-decidable decision problems......Page 342
7.6.1 Nonrecursive sets......Page 347
7.6.2 The arithmetic hierarchy......Page 350
7.7 Decidable decision problems......Page 352
The even problem (EVENS)......Page 353
The composites problem (COMP)......Page 354
The graph problem (GRAPH)......Page 356
The connectivity problem (CON)......Page 357
The satisfiability problem for propositional logic (PSAT) etc......Page 358
7.7.2 Time and space......Page 359
7.7.3 Nondetermenistic polynomial-time......Page 362
7.8 NP-completeness......Page 363
Minesweeper......Page 365
Exercises......Page 367
8. The incompleteness theorem......Page 372
8.1 Axioms for first-order number theory......Page 373
8.2 The expressive power of first-order number theory......Page 377
8.3 Godel\'s First Incompleteness Theorem......Page 385
8.4 Godel codes......Page 389
8.5 Godel\'s Second Incompleteness Theorem......Page 395
8.6 Goodstein sequences......Page 398
Exercises......Page 401
9.1 Second-order logic......Page 403
9.2 Infinitary logics......Page 407
9.3 Fixed-point logics......Page 410
Inflationary fixed-point logic (IFP)......Page 411
Partial fixed-point logic (PFP)......Page 413
Least fixed-point logic (LFP)......Page 414
9.4 Lindstrom\'s theorem......Page 415
Exercises......Page 419
10.1 Finite-variable logics......Page 423
10.2 Classical failures......Page 427
10.3 Descriptive complexity......Page 432
10.4 Logic and the P=NP problem......Page 438
Exercises......Page 439
Bibliography......Page 441
Index......Page 443