Combinatory logic. Vol. 1.

Preface......Page 3
Explanation of Notations......Page 6
A. The analysis of substitution......Page 10
B. The Russell paradox......Page 13
C. Plan of the work......Page 14
D. Historical sketch......Page 17
1. Axiomatic systems......Page 21
3. Example of a formal system......Page 22
B. Definition of a formal system......Page 23
1. Fundamental definitions......Page 24
2. Definiteness restrictions......Page 26
C. Philosophy of formal systems......Page 28
2. Representation......Page 29
3. Interpretation......Page 30
4. Acceptability......Page 31
1. Languages......Page 32
2. Grammatics......Page 33
4. The A-language......Page 34
5. Syntactical systems......Page 35
1. Relational systems......Page 37
2. Logistic systems......Page 38
3. Applicative systems......Page 39
4. Reduction to a single atom......Page 40
5. Complete formalization......Page 41
1. Historical and bibliographical comment......Page 42
2. Metasystems......Page 44
3. Formal systems and nominalism......Page 46
1. Examples of epistatements......Page 49
2. Constructiveness......Page 50
3. Truth criteria......Page 51
4. Definitions......Page 52
1. Constructions......Page 53
3. Deductions......Page 56
4. Proofs by induction......Page 57
5. Notation......Page 58
1. Preliminary definitions......Page 61
2. Substitution......Page 62
3. Formal variables......Page 63
4. Free variables......Page 64
5. Extensions......Page 65
2. Definition of replacement......Page 66
3. The replacement theorem......Page 67
5. Monotone quasi-ordering generated by a given relation......Page 68
7. Replaceability......Page 70
1. Definitional extensions......Page 71
2. Complete definitions......Page 75
3. Generated equivalence......Page 76
4. Relative definitions......Page 78
5. Primitive recursive definitions......Page 82
6. Monotone character of primitive recursive operations......Page 83
1. Historical comment......Page 85
2. Other directions of epitheory......Page 86
1. Elementary examples......Page 89
2. Need for a functional notation......Page 90
3. The λ-notation......Page 91
2. Functions of several arguments......Page 92
3. λ-applicative systems......Page 93
4. Relation to bound variables in general......Page 94
1. Preliminary......Page 96
3. Auxiliary conventions......Page 97
2. Rules of β-conversion......Page 98
3. Generalization......Page 100
5. Redexes......Page 101
6. δ-conversion......Page 102
1. The basic definition......Page 103
2. Statement of the theorems......Page 104
3. Preliminary lemmas......Page 105
4. Proof of Theorem 1......Page 106
5. Proof of Theorem 2......Page 108
6. Proof of (a)......Page 109
8. Proof of Theorem 3......Page 112
S. Supplementary topics......Page 113
2. Notation......Page 114
3. Motivation of the restricted system......Page 115
4. The δ_1-system......Page 116
A. General formulation......Page 117
1. The property (χ) and its corollaries......Page 118
2. Property (B)......Page 119
3. Stepwise generated quasi-orderings......Page 120
4. Residuals......Page 122
5. Outline of proof of Theorem 1......Page 123
1. The theory of β-conversion......Page 124
2. The full λ-calculus......Page 126
3. The strong form of (D)......Page 128
4. Generalization......Page 131
1. Property (H)......Page 132
2. Outline of the proof of (E)......Page 134
3. Minimal sequences of redexes......Page 135
4. Minimalization of a relative reduction......Page 136
6. Concluding remarks......Page 139
1. Pure η-conversion......Page 140
2. Postponement of η-contractions......Page 141
3. Advancement of η-contractions......Page 144
4. Property (χ) for the βη-calculus......Page 145
5. Extension to the full λ-calculus......Page 146
1. Standardization theorem......Page 148
3. Extensions to λK-conversion......Page 151
1. Definition of order......Page 153
2. Preliminary theorems......Page 154
3. Order and β-conversion......Page 155
1. Historical statement......Page 158
5. Intuitive Theory of Combinators......Page 160
1. The combinators B, C, I, W......Page 161
3. The combinators S, Φ, Ψ......Page 162
4. Examples......Page 163
1. Definitions in terms of B, C, W......Page 164
2. Definitions involving K......Page 166
3. Rosser's primitive combinators......Page 168
1. Kinds of obs......Page 169
4. Kinds of regular combinators......Page 170
6. Terminology for combinations......Page 171
1. Composite product......Page 172
2. Powers......Page 173
3. Deferred combinators......Page 174
5. Inverse combinators......Page 176
E. Combinators related to S......Page 177
1. The sequences Φ_n and S_n......Page 178
2. The sequence X_[n]......Page 179
3. The sequence X^[m]......Page 180
4. Iterative sequences......Page 182
5. Iterators......Page 183
1. General theorems......Page 184
2. Theorems on regular combinators......Page 185
G. Paradoxical combinators......Page 186
1. Conditions on the proper combinators entering a combination......Page 188
2. Bases for sets of combinators......Page 191
3. Independence and interdefinability among the combinators S, K, C, B, W, I......Page 192
1. Historical statement......Page 193
2. Other sets of primitive combinators......Page 194
1. Preliminary......Page 195
2. Definition of functional abstraction......Page 197
3. Alternative definitions......Page 199
1. Redundance of the rule (ν)......Page 203
2. Incorporation of the intuitive theory......Page 204
4. Conclusion......Page 205
C. The combinatory axioms......Page 206
1. The rule (ξ)......Page 207
2. The rules (η) and (η')......Page 208
3. Consequences of (ζ')......Page 210
4. The systems H_η and H_β......Page 212
D. Theory of the substitution prefix......Page 214
1. Preliminaries......Page 218
2. Properites of J and M......Page 221
3. The J-M isomorphism......Page 224
4. Relations between H and L......Page 225
5. Concluding remarks......Page 226
F. Theory of strong reduction......Page 227
1. Preliminaries......Page 228
2. Strict formulation......Page 231
3. Normal reductions......Page 235
4. The normal form theorem......Page 237
1. Historical comment......Page 245
2. Normal representation of a combination......Page 246
3. Combinatory semigroups......Page 247
1. General specifications for the basic system......Page 248
2. E-rules......Page 249
1. Properties of relations......Page 250
2. Interrelations of the properties......Page 252
3. Properties of [⊢]......Page 253
1. Preliminary theorems......Page 254
2. Properties in terms of strong deducibility......Page 255
3. Formulation of L_0......Page 256
D. The systems K......Page 257
1. Formulation......Page 258
1. The systems [H]......Page 259
2. Modification of Rule K_2......Page 260
3. Transition to a logistic system......Page 261
4. Change from H to a logistic system L'......Page 262
5. Notes on the systems K......Page 263
1. Historical comment......Page 264
8. Introduction to Illative Combinatory Logic......Page 266
A. The Russell paradox......Page 267
B. Alternative explanations of the paradox......Page 269
C. The notion of functionality......Page 271
D. Relations to other illative concepts......Page 275
1. Symbolic conventions......Page 277
3. Equality......Page 278
4. Reductions......Page 280
5. Conventions in regard to statements and inferences......Page 281
1. Historical and bibliographical comment......Page 282
2. Grammatical interpretation of functionality......Page 283
3. Comments on consistency......Page 284
1. Nature of the theory of functionality......Page 286
2. Morphological conventions......Page 287
3. Formulation of the theory proper......Page 288
4. F-deductions......Page 289
5. The F-sequence......Page 290
B. The subject-construction theorem......Page 291
1. Statement and proof of the theorem......Page 292
2. Deductions from (FK) and (FS)......Page 293
3. Further examples......Page 297
4. Stratification......Page 298
C. The subject-conversion theorems......Page 302
1. Role of Rule Eq'......Page 303
2. The subject-reduction theorem for F_1(S, K)......Page 304
3. The subject-expansion theorem for F_1(S, K)......Page 306
4. Other choices of primitive combinators......Page 308
5. Termination questions......Page 310
6. Strong reduction......Page 311
1. The stratification theorem......Page 313
3. The substitution theorem......Page 315
5. Necessity of stratification......Page 317
6. The λ-formulation of F^b_1......Page 318
E. Analogies with propositional algebra......Page 321
1. The F-P transformation......Page 322
2. Converse transformation......Page 323
1. A T-rule formulation......Page 324
2. Preliminary L-formulation......Page 329
3. Refinement of the L-formulation......Page 331
4. The elimination theorem......Page 335
5. Relations between the systems......Page 341
6. Standardization......Page 348
1. Quine's notion of statification......Page 353
A. Preliminaries......Page 354
1. Fundamental conventions......Page 355
2. Equality......Page 356
3. Inconsistency of the full free theory......Page 358
4. Consistency of F^f_1(I)......Page 360
1. F-substitution......Page 362
2. Reducing F-substitution......Page 363
3. FQ-standardization......Page 365
4. Consequences of the standardization theorem......Page 368
1. The normalization theorem......Page 369
2. The subject-reduction theorem......Page 370
3. The standardization theorem for the free partial system......Page 372
4. Strengthened standardization......Page 373
1. Formulation......Page 374
2. Standardization theorem for F^r_1......Page 375
3. Extension to F^s_1......Page 376
E. Finite formulation......Page 377
1. Methods of expressing generality......Page 378
2. Properties of Ξ'......Page 379
3. Properties of Ξ''......Page 380
4. Finite formulation in terms of L......Page 381
5. Consistency questions......Page 382
Appendix A. List of Basic Constants......Page 385
Appendix B. List of Properties of Relations......Page 388
Bibliography......Page 390
Index......Page 402