Page 151 - Textos de Matemática Vol. 40

A note on the history of functional self-application 139
combinatory logic [Cur30, CF58, CHS72]. It was Curry who first advocated explicitely self-application as a meaningful concept, cf. [Cur30, p. 515f].
Today, combinatory logic is a well-established branch of mathematical logic, together with its twin theory, the λ-calculus, which was invented by Alonzo Church (1903–1995).22 Furthermore, it provides the foundations for functional programming in computer science. And, type-free functional pro- gramming languages, like lisp and scheme, allow self-application as a specific programming feature.23
But also the celebrated computer model due to John (Ja´nos, Johann) von Neumann (1903–1957), in which code and data are represented on the same level, contains—at least implicitly—the possibility of functional self-appli- cation.
Finally, we would like to mention the applicative theories, discussed in this work, as an elaborated theory with self-application. Here, self-application is meaningful at the expense of partiality of the underlying logic.24 As we know, self-application is in this context a special case of diagonalization.
Nowadays functional self-application is a well-studied, well-understood and unsuspicious concept in mathematical logic. However, it usually requires an un- typed setting as well as a concept of partiality, both uncommon from a traditional mathematical point of view. It it worth noting that in the standard mathemat- ical framework of Zermelo-Fraenkel set theory, ZF, functional self-application is excluded only by the axiom of foundation. This axiom, due to von Neu- mann, was added to the canon of ZF axioms comparatively late, in 1925/1930 [vN25, vN29, Zer30] (see [Acz88, p. 106f]).25 However, the possibility of func- tional self-application based on non-well-founded sets seems to have never been considered, neither in the rudimentary versions of ZF without foundation, nor in the explicit non-well-founded set theories of Dmitry Mirimanoff (1861–1945) [Mir17a, Mir17b] and Paul Finsler (1894–1970) [Fin26, Fin75].26
Now, we will turn to the use of functional self-application by Hilbert, 15 years before its appearance in the talk of Sch¨onfinkel. Therefore, we have to look
22However, both, combinatory logic and λ-calculus, originally also aimed to provide a foun- dation for logic and mathematics in general, an aim which failed due to the occurrence of inconsistencies, cf. [KR35, Cur42] and [Ros84, Section 2]. For a full account to the history of combinatory logic and λ-calculus we can refer to [CH0x] and [Sel0x].
23“John McCarthy worked several ideas of the LC [λ-calculus] into lisp. He clearly recog- nized procedures as functions of one argument. In the LC, such functions can be applied to each other and give such functions when applied. In lisp, it is possible to apply one procedure to another, and on occasion get another procedure.” [Ros84, p. 339].
24Here, we will not consider the total versions of applicative theories.
25Zermelo considered in a draft of his axiomatization of set theory around 1905 the axiom “I. Eine wohldefinirte Menge entha¨lt niemals sich selbst als Element. M ̸∈ M.” (I. A well- defined set never contains itself as an element. M ̸∈ M.) But this axiom did not find its way into the published axiomatization of 1908 [Zer08], cf. [Pec90, p. 95] with reference to [Moo82, p. 155f].
26In [vR80] the author uses non-well-founded set theory to construct a model of the λ- calculus.