Mathematical Logic with Special Reference to the Natural Numbers

Title ......Page 1
Copyright ......Page 2
Dedication ......Page 3
Contents ......Page 5
Preface ......Page 13
Introduction ......Page 15
1.2 The signs and symbols ......Page 24
1.3 The formulae ......Page 26
1.5 Rules of formation ......Page 27
1.6 Parentheses ......Page 30
1.8 The rules of consequence ......Page 32
1.9 Corresponding and related occurrences ......Page 35
1.10 The lambda-rules ......Page 36
1.11 Definitions and abbreviations ......Page 37
1.12 Omission of parentheses ......Page 38
1.13 Formal systems ......Page 41
1.14 Extensions of formal systems ......Page 42
1.16 Negation ......Page 43
Historical remarks to Chapter 1 ......Page 44
Examples 1 ......Page 46
2.1 Definition of a propositional calculus ......Page 48
2.2 Equivalence of propositional calculi ......Page 49
2.4 Models of propositional calculi ......Page 50
2.5 Deductions ......Page 53
2.6 The classical propositional calculus ......Page 56
2.7 Some properties of the remodelling and building schemes ......Page 57
2.8 Deduction theorem ......Page 62
2.9 Modus Ponens ......Page 63
2.10 Regularity ......Page 65
2.11 Duality ......Page 66
2.12 Independence of symbols, axioms and rules ......Page 67
2.13 Consistency and completeness of Pc ......Page 69
2.14 Decidability ......Page 71
2.15 Truth-tables ......Page 72
2.16 Boolean Algebra ......Page 75
2.17 Normal forms ......Page 78
Historical remarks to Chapter 2 ......Page 79
Examples 2 ......Page 82
3.1 Definition of a predicate calculus ......Page 86
3.2 Models ......Page 90
3.3 Predicative and impredicative predicate calculi ......Page 91
3.4 The classical predicate calculus of the first order ......Page 92
3.5 Properties of the system Fc ......Page 93
3.6 Modus Ponens ......Page 98
3.7 Regularity ......Page 102
3.8 The system Fc ......Page 104
3.9 Prenex normal form ......Page 105
3.10 H-disjunctions ......Page 113
3.11 Validity and satisfaction ......Page 122
3.12 Independence ......Page 125
3.14 Fc with functors ......Page 127
3.15 Theories ......Page 128
3.16 Many-sorted predicate calculi ......Page 129
3.17 Equality ......Page 133
3.18 Predicate calculus with equality and functors ......Page 137
3.19 Elimination of axiom schemes ......Page 140
3.20 Special cases of the decision problem ......Page 144
3.21 The reduction problem ......Page 150
3.22 Method of semantic tableaux ......Page 163
3.23 An application of the method of semantic tableaux ......Page 168
3.24 Resolved Fc ......Page 174
3.25 The system BFc ......Page 180
3.26 Set theory ......Page 185
3.27 Ordinals ......Page 189
3.28 Transfinite induction ......Page 192
3.29 Cardinals ......Page 194
3.30 Elimination of the e-symbol ......Page 198
3.31 Complete Boolean Algebras ......Page 206
3.32 Truth-definitions for set theory ......Page 207
3.33 Predicative and impredicative properties ......Page 212
3.34 Topology ......Page 213
Historical remarks to Chapter 3 ......Page 215
Examples 3 ......Page 219
4.2 The A00-rules of formation ......Page 227
4.3 The A00-rules of consequence ......Page 229
4.4 Definition of A00-truth ......Page 232
4.6 Exclusiveness of A0Q-truth and A00-falsity ......Page 233
4.7 Consistency of A00 with respect to A00-truth ......Page 238
4.8 Completeness and decidability of A00 with respect to A00-truth ......Page 239
4.9 Negation in the system A00 ......Page 241
4.10 The system B00 (the anti-A00-system) ......Page 242
Historical remarks to Chapter 4 ......Page 243
Examples 4 ......Page 244
5.1 Calculable functions ......Page 246
5.2 Primitive recursive functions ......Page 247
5.3 Definitions of particular primitive recursive functions ......Page 249
5.4 Characteristic functions ......Page 257
5.5 Other schemes for generating calculable functions ......Page 260
5.7 Simultaneous recursion ......Page 261
5.8 Recursion with substitution in parameter ......Page 262
5.9 Double recursion ......Page 264
5.10 Simple nested recursion ......Page 266
5.11 Alternative definitions of primitive recursive functions ......Page 268
5.12 Existence of a calculable function which fails to be primitive recursive ......Page 272
5.13 Enumeration of primitive recursive functions ......Page 274
5.14 Definition of the proof-predicate for A00 ......Page 279
5.15 The function Val ......Page 284
Historical remarks to Chapter 5 ......Page 287
Examples 5 ......Page 289
6.1 The system A0 ......Page 292
6.2 A0-truth ......Page 293
6.3 Undefinability of A0-falsity in A0 p- ......Page 297
6.4 Enumeration of A0-theorems ......Page 298
Examples 6 ......Page 300
7.1 Turing machines and Church's Thesis ......Page 302
7.2 Some simple tables ......Page 314
7.3 Equivalence of partially calculable and partially recursive functions ......Page 318
7.4 The S-O-O' proposition ......Page 327
7.5 The undecidability of the classical predicate calculus Fc ......Page 328
7.6 Various undecidability results ......Page 330
7.7 Lattice points ......Page 332
7.9 Simple sets ......Page 337
7.10 Hypersimple sets ......Page 338
7.11 Creative sets ......Page 341
7.12 Productive sets ......Page 344
7.13 Isomorphism of creative sets ......Page 346
7.14 Fixed point proposition ......Page 348
7.15 Completely productive sets ......Page 349
7.16 Oracles ......Page 350
7.17 Degrees of unsolvability ......Page 357
7.18 Structure of the upper semi-lattice of degrees of unsolvability ......Page 360
7.19 Example of the priority method. Solution of Post's problem ......Page 366
7.20 Complete degrees ......Page 370
7.21 Sequences of degrees ......Page 375
7.22 Non-recursively separable recursively enumerable sets ......Page 378
7.23 Cohesive sets ......Page 379
7.24 Maximal sets ......Page 380
7.25 Minimal degrees ......Page 382
7.26 Degrees of theories ......Page 386
7.27 Chains of degrees ......Page 388
7.28 Recursive real numbers ......Page 389
Historical remarks to Chapter 7 ......Page 392
Examples 7 ......Page 396
8.1 The system A ......Page 401
8.2 Definition of A-truth ......Page 402
8.3 Incompleteness and undecidability of the system A ......Page 404
8.4 Various properties of the system A ......Page 405
8.5 Modus Ponens ......Page 410
8.6 Consistency ......Page 412
8.7 Truth-definitions ......Page 415
8.8 Axiomatizable sets of statements ......Page 417
Historical remarks to Chapter 8 ......Page 421
Examples 8 ......Page 422
9.1 The hierarchy of A-definable sets of lattice points ......Page 423
9.2 Dkp-sets ......Page 427
9.3 Sets undefinable in A ......Page 430
9.4 f-definable sets of lattice points ......Page 431
9.5 Computing degrees of unsolvability ......Page 433
Examples 9 ......Page 435
10.1 Limitations of the system A ......Page 437
10.2 Possible ways of extending the system A0 ......Page 439
10.3 The system E ......Page 444
10.4 The system AI ......Page 452
10.5 Definition of an Arproof p ......Page 454
10.6 Theorem induction ......Page 459
10.7 The AI-proof-predicate ......Page 462
10.8 An example of an AI-proof ......Page 465
10.9 Relations between A0-theorems and E-correctness ......Page 469
10.10 Properties of the system AI ......Page 473
10.11 Reversibility of rules ......Page 477
10.12 Deduction theorem ......Page 483
10.13 Cuts with an A00 cut formula ......Page 484
10.14 Cut removal with a weaker form of R3 ......Page 498
10.15 Cut removal in general ......Page 501
10.16 Further properties of the system AI ......Page 511
10.17 The consistency of AI ......Page 514
Historical remarks to Chapter 10 ......Page 521
Examples 10 ......Page 523
11.1 The system A' ......Page 525
11.2 Remarks ......Page 530
11.4 Properties of the systems A(v) ......Page 532
11.5 The systems A(v)* ......Page 533
11.6 The definition of A-truth in A'* ......Page 535
11.7 Consistency of AI ......Page 544
11.8 Definition of A(k)-truth ......Page 549
11.9 Scheme for an A(k)-truth-definition ......Page 552
11.10 Truth-definitions in impredicative systems ......Page 554
11.11 Further extensions of the systems A(k) ......Page 555
11.12 Incompleteness of extended systems ......Page 557
11.13 Real numbers ......Page 558
11.14 The analytical hierarchy ......Page 567
11.15 On the length of proofs ......Page 572
Historical remarks to Chapter 11 ......Page 573
Examples 11 ......Page 574
12.1 Models and truth-definitions ......Page 577
12.2 Models for A00 ......Page 579
12.3 Models for A0 ......Page 580
12.5 General models ......Page 581
12.6 Satisfaction ......Page 582
12.7 Examples ......Page 584
12.8 Non-standard models ......Page 585
12.9 A non-standard model for AI ......Page 589
12.10 Induction ......Page 591
12.11 S-models ......Page 594
12.12 Ultraproducts ......Page 595
12.13 S-models ......Page 599
12.14 Satisfaction by D2-predicates ......Page 604
12.15 HE-models ......Page 607
12.16 Completeness of higher order Predicate Calculi ......Page 608
12.17 Independence proofs ......Page 613
Historical remarks to Chapter 12 ......Page 620
Examples 12 ......Page 621
Epilogue ......Page 623
Glossary of special symbols ......Page 625
Note on references ......Page 633
References ......Page 635
Index ......Page 645