Author(s): [edited by] Haskell B. Curry, J. Roger Hindley, Jonathan P. Seldin.
Series: Studies in logic and the foundations of mathematics 65
Edition: English
Publisher: North-Holland Pub. Co
Year: 1972.
Language: English
Pages: 520 p
City: Amsterdam ; London
Contents......Page 12
Preface......Page 8
Explanation of Notations......Page 14
A. Preliminaries......Page 16
1. Formal systems......Page 17
2. Philosophy of combinatory logic......Page 23
3. Constructions......Page 30
4. Components and replacement......Page 32
5. Monotone relations......Page 34
B. The weak theory of combinators......Page 37
1. Formulation......Page 38
2. General properties of weak reduction......Page 43
3. The standardization theorem......Page 47
4. Order of combinations......Page 49
5. Canonical reductions......Page 51
6. Some special techniques......Page 54
C. Bracket abstraction......Page 57
1. Fundamental properties......Page 58
2. Structure of [x]Y......Page 62
3. Structure of the m-variable bracket abstract......Page 66
4. Reduction of a bracket abstract......Page 71
D. The synthetic theory of combinators......Page 82
1. Preliminaries......Page 83
2. Properties of bracket abstraction......Page 86
3. Transformation of the reduction rules......Page 90
4. Zeta-validity......Page 94
5. The rule (η)......Page 96
E. Strong reduction......Page 101
1. Basic properties of strong reduction......Page 102
2. Linearization of strong reduction......Page 108
3. Normal reductions......Page 111
4. Combinations in normal form......Page 121
5. The normal form theorem......Page 126
6. The converse normal form theorem......Page 130
7. Axiomatization of strong reduction......Page 131
8. Standardization......Page 134
1. Basic properties of C-systems......Page 145
2. Strong C-systems; the H-transformation......Page 152
3. C-reduction......Page 157
4. Extenstional types of C-reduction......Page 163
5. Combinatory epifunctions......Page 166
6. Special λI-transformation......Page 168
7. Fixed-point combinators......Page 169
8. Theorem of Böhm......Page 171
A. Illative systems in general......Page 178
2. Some impossible extensions......Page 179
3. Z-systems......Page 180
4. Generalized axiom schemes......Page 186
1. The system F_0......Page 190
2. Illative primatives......Page 192
3. The generalized Russell paradox......Page 195
4. Canonicalness restrictions......Page 197
5. Modifications of Rule Eq......Page 200
C. Inferential systems for L......Page 201
2. An L-formulation......Page 202
3. Alternative formulations......Page 210
4. The elimination theorem......Page 211
5. Relations between the systems......Page 218
D. CL-systems......Page 222
1. Formulation and definitions......Page 223
2. General theory of CL-systems......Page 225
A. Foundations......Page 226
1. Combinatory natural numbers......Page 227
2. Arithmetical combinators......Page 231
3. Interdefinability of arithmetical combinators......Page 237
4. Recursive numerical functions......Page 246
5. The case of λI-conversion......Page 252
B. Gödelian epitheory......Page 260
1. Gödel numeration......Page 261
2. The undecidability theorem......Page 266
3. Inverse Gödel numeration......Page 269
C. Combinatory syntax......Page 273
1. Dyads and numerals......Page 274
2. Polyads......Page 277
3. Selection operations......Page 280
4. Discriminations and length......Page 285
5. Generators......Page 288
D. Typed combinatory arithmetic......Page 290
1. Arithmetical basic functionality......Page 291
2. Functional character of ordered pairs......Page 292
3. F-schemes for R......Page 294
4. Prorecursive functions and combinators......Page 300
5. Functionals of finite type......Page 301
6. Consistency questions......Page 305
1. Fundamental conventions......Page 307
2. Canonical restrictions......Page 309
3. The F-sequence......Page 310
1. Fundamental definitions......Page 311
2. The subject-conversion theorems......Page 312
3. Monoschematic basic functionality......Page 314
C. Deductive theory of F_1......Page 319
1. Role of Rule Eq'......Page 320
2. The stratification theorem for A-deductions......Page 321
3. A T-formulation......Page 322
1. Fundamental conventions......Page 323
2. The subject-construction theorem......Page 325
3. The subject-reduction theorem......Page 328
4. The subject-expansion theorem......Page 330
5. A-deductions......Page 331
1. Fomulation......Page 332
2. The elimination theorem......Page 333
3. Equivalence of the systems......Page 335
4. The normal form theorem......Page 340
5. Standardization......Page 345
6 Modifications for F-deductions......Page 348
F. The system F_12......Page 350
2. Deductive theory of F_12......Page 351
15. The Theory of Restricted Generality......Page 354
1. Informal discussion......Page 355
2. The Ξ-sequence......Page 358
3. Bound variables......Page 361
4. Implication......Page 362
5. Universal quantification......Page 364
7. Relation to F_1......Page 366
8. The G-sequence......Page 368
B. Deductive theory of F_2......Page 371
1. The deduction theorem......Page 372
2. A T-formulation......Page 379
3. Canonicalness restrictions......Page 381
4. An L-formulation......Page 385
5. V-formulation......Page 387
6. Equality and related extensions......Page 394
C. Finite formulations......Page 396
1. The deduction theorem......Page 398
2. A T-formulation......Page 406
3. Formulation of equality......Page 413
4. An L-formulation......Page 417
5. Relative canonicalness......Page 419
6. Modifications and extensions......Page 425
7. V-formulations......Page 427
D. The predicate calculus......Page 429
1. Predicate calculus in F_21......Page 431
2. Predicate calculus in F*_21......Page 437
16. The Theory of Universal Generality......Page 442
1. The P- and Π-sequences......Page 443
2. Bound variables......Page 445
4. Relation to F_20......Page 446
1. The deduction theorems......Page 447
2. Inferential formulations......Page 451
3. Comparison with F_21......Page 452
C. Deductive theory of F_32......Page 453
1. The deduction theorem......Page 454
2. The extended system without the deduction theorem......Page 455
3. The extended system with a deduction theorem......Page 457
4. General relations between F_2 and F_3......Page 459
1. The system F*_31......Page 460
2. The system F*_32......Page 465
3. Relative canonicalness......Page 466
A. Formulations......Page 467
1. The underlying F-system......Page 468
2. Formulation of T......Page 470
3. Alternative formulations......Page 472
1. Partial and total valuations......Page 476
2. The elimination theorem......Page 479
3. General models......Page 485
C. Kinds of type theory......Page 493
1. Basic type theory......Page 494
2. Transfinite type theory......Page 505
3. Extended type theory......Page 513
Bibliography......Page 514
Index......Page 520
