Movatterモバイル変換

1. Moses Schönfinkel had a chance to publish just one paper on CL(see Schönfinkel (1924)). CL was soon rediscovered and greatlyexpanded in its scope by Haskell B. Curry, who was joined by severalother logicians in an effort to develop CL and the closely related\(\lambda\)-calculuses invented by Alonzo Church.

2. This sentence may be seen to formalize a well-known metatheorem aboutwell-behaved sequent and consecution calculuses—withoutexplicating some of the technical details.

3. Theformal notions of algorithms, computable functions andalike had not yet been formulated at the time when Schönfinkelpublished his paper. \(\lambda\)-calculuses, Turing machines andPost’s calculuses appeared a decade or more later, and othernotions such as Markov algorithms, register machines, 0-type grammarsand abstract state machines are even newer. See Kleene (1967, Ch. V)concerning the early history of some of these concepts.

4. ‘\(\textsf{C}Gyx\)’ could be thought to be read as“\(y\) is less than \(x\),” and ‘\(Lyx\)’could stand for this binary predicate in a more mnemonic presentationof FOL. However, given \(G\), ‘\(\textsf{C}Gyx\)’ and‘\(Lyx\)’ express the same meaning.

5. The possibility of this move follows from, and therefore, illustratesthecombinatorial completeness theorem. Although this lastpotential transformation is not important for the success ofSchönfinkel’s procedure, combinatorial completeness is.

6. This may be the reason why Schönfinkel gave second-orderexamples toward the end of his paper, despite the fact that heunequivocally stated at the beginning of his paper that he isconcerned with FOL. (Incidentally, the misleading examples were notcaught by the German editor, who, on the other hand, appended someparagraphs to the paper that contain mistaken claims.) The unfortunatechoice of examples might have contributed to the misinterpretation ofSchönfinkel’s aims along the line that he attempted toprovide a typefree framework for all of mathematics.

7. The importance of this idea can hardly be overstated. Viewing afunction of several arguments as a function of one argument is oftencalled “currying” (with the other direction termed“uncurrying”). The same idea reappears in other areas ofmathematics, for example, in algebra as (abstract) residuation and incategory theory (in the unary case) as adjoint functors.

8. One might contend that the understanding of (closed) formulas notonly as meaningful sentences but also as sequences of symbols on paperis as crucial to Schönfinkel’s procedure as it is toGödel’s first incompleteness theorem.

9. We follow Curry’s meta-theoretical distinctions in calling theentities that CL deals with ‘objects’ rather than usingthe neutral expression ‘expressions’. (Curry uses‘obs’ as a technical term.)

10. We do not follow Curry’s terminology completely, according towhich the combinator that is denoted here by \(\textsf{M}\) is only acombinator with “duplicative effect,” because we do notutilize the distinction between regular and nonregular combinators.The interested reader should consult Curry and Feys (1958) concerninga slightly different use of the terms “cancellator,”“duplicator,” “permutator,” etc.