 where \(\ulcorner \cdot \urcorner\) is a Gödel numbering of the language of \(\varphi\) as described in  Section 1.3.  The second step of Turing and Church’s negative answer to the Entscheidungsproblem relied on their prior specification of similar decision problems for the models \(\mathbf{T}\), \(\mathbf{L}\), and \(\mathbf{GR}\). Together with Kleene (1936a), they showed the following: