Surely Church must also have discovered the universal machine? Church's major result was the undecidability of the halting problem, and to set up the diagonaliz

Surely Church must also have discovered the universal machine? Church's major result was the undecidability of the halting problem, and to set up the diagonalization proof you need a notion of interpreting a program. Looking at his paper[0], he has THEOREM XII. It is possible to associate simultaneously with every well-formed formula an enumeration of the formulas obtainable from it by conversion, in such a way that the function of two variables, whose value, when taken of a well-formed formula A and a positive integer n, is the n-th formula in the enumeration of the formulas obtainable from A by conversion, is recursive. THEOREM XVI. Every recursive function of positive integers is λ-definable. So approximately, Theorem XII gives an algorithm for evaluating a program A n steps, and theorem XVI says that this algorithm can be compiled in the a λ-calculus program. Church cites a paper by Kleene for this construction[1]. It's true that the Kleene doesn't prove this using a general recursion combinator like the Y combinator; instead he first shows how to λ-encode primitive recursive functions, and gives a combinator for the μ operator [2]. When you talk about Church "not following up" the notion of universality, I'm not sure what more you would want him to do. Of course he did not prove that λ-calculus was equivalent to Turing machines, because those had not been invented yet. But he and Kleene did prove that the λ-definable functions coincide with the μ-recursive functions, which was the best known model of universal computation. And he argues ([0] section 7) that this captures the intuitive notions of "a function for which there exists an algorithm" and "a function which can be proven to have a given value". [0] https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/church.pdf https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/c... [1] https://projecteuclid.org/download/pdf_1/euclid.dmj/1077489488 https://projecteuclid.org/download/pdf_1/euclid.dmj/10774894... [2] https://en.wikipedia.org/wiki/%CE%9C-recursive_function https://en.wikipedia.org/wiki/%CE%9C-recursive_function