The origin of functionals in logic
McCarthy's "A Basis for a Mathematical Theory of Computation" introduces recursive function definitions, mutually recursive definitions and computable functionals in a way that is closed to today's programming practice.
He shows that partial recursive functions are a subset of this formalism.
I'm interested in the relation between logical languages and this formalism. I traced the origins of recursive definitions in logic to Skolem's "The foundations of elementary arithmetic" through a footnote in a book.
What is the origin of functionals (functions that take other function as parameters) in logic?
Solution 1:
The origin of functionals in logic (I prefer to call them higher-order functions, to avoid confusion with other notions of functional in other domains of mathematics) coincides with the origin of modern logic. The pioneering work by Gottlob Frege about foundations of logic and mathematics, such as Funktion und Begriff (1891) and especially Grundgesetze der Arithmetik (1893), clearly presents the concept of functional. Quoting from Funktion und Begriff (actually quoting from here):
Like things and functions are different, so are functions, whose arguments are functions radically different from functions whose arguments must be things. I call the latter functions of first order, the former functions of second order.
I am not an expert in Frege's work, so I cannot say how important functionals are in his attempt to provide foundations to logic and mathematics. In my opinion, the first systematic studies of functionals in logic date back to the 20's and 30's, with the introduction of combinatory logic and $\lambda$-calculus.
Combinatory logic (CL) was introduced by Moses Schönfinkel in 1920 and first published in his 1924 paper On the Building Blocks of Mathematical Logic, and in the late 20's and in the 30's rediscovered and systematically studied by Haskell Curry (his first published paper on that, Grundlagen der kombinatorischen Logik, dates back to 1930). The $\lambda$-calculus ($\lambda$) was introduced Alonzo Church in 1928 and first published in his 1932 paper A set of postulates for the foundation of logic.
Quoting from Cardone and Hindley's History of Lambda-calculus and Combinatory Logic (2006):
[...] the situation in logic and the foundations of mathematics was much more fluid in the early 1900s than it is today; Russell’s paradox was relatively recent, Gödel's theorems were not yet known, and a significant strand of work in logic was the building of systems intended to be consistent foundations for the whole of mathematical analysis. Some of these were based on a concept of set, others on one of function, and there was no general consensus as to which basis was better. In this context λ and CL were originally developed, not as autonomous systems but as parts of more elaborate foundational systems based on a concept of function.
Roughly speaking, both $\lambda$ and CL share the idea that everything is a function, and so one of the core aspects of these frameworks is the possibility to apply a function to another function. Even though $\lambda$ and CL have failed in their original purpose to provide foundations to whole mathematics, nowadays $\lambda$ and CL are used extensively in higher-order logic and computing (see for instance Curry-Howard correspondence), and they have inspired (or represent the kernel of) several important logical systems and programming languages.