We now understand the Entscheidungsproblem to have been answered in the negative by Church (1936a) and Turing (1937). The solution they provided can be reconstructed as follows: 1) a mathematical definition of a model of computation \(\mathfrak{M}\) was presented; 2) an informal argument was given to show that \(\mathfrak{M}\) contains representatives of all effective procedures; 3) a formal argument was then given to show that no machine \(M \in \mathfrak{M}\) decides \(\sc{FO}\text{-}\sc{VALID}\). Church (1936b) took \(\mathfrak{M}\) to be the class of terms \(\Lambda\) in the untyped lambda calculus, while Turing took \(\mathfrak{M}\) to correspond the class of \(\mathfrak{T}\) of Turing machines. Church also showed the class \(\mathcal{F}_{\Lambda}\) of lambda-definable functions is extensionally coincident with the class \(\mathcal{F}_{\mathfrak{R}}\) of general recursive functions (as defined by Gödel 1986b and Kleene 1936). Turing then showed that the class \(\mathcal{F}_{\mathfrak{T}}\) of functions computable by a Turing machine was extensionally coincident with \(\mathcal{F}_{\Lambda}\).