 This passage illustrates another sense in which the question of the decidability of logical derivability is connected to the concerns which had initiated Hilbert’s study of metamathematics. For note that if \(\Gamma\) is a finite set of axioms \(\{\gamma_1,\ldots,\gamma_k\}\), then the question of whether \(\psi\) is a logical consequence of \(\Gamma\) is equivalent to whether the sentence \(\varphi=_{\textrm{df}} (\gamma_1 \wedge \ldots \wedge \gamma_k) \rightarrow \psi\) is logically valid. By  Gödel’s Completeness Theorem (see the entry on Gödel)  for first-order logic, this is equivalent to the derivability of \(\varphi\) from Hilbert &amp; Ackermann’s axiomatization of first-order logic. A positive answer to the Entscheidungsproblem could thus be interpreted as showing that it is possible to mechanize the search for proofs in mathematics in the sense of allowing us to algorithmically determine if a formula expressing an open question (e.g. the Riemann Hypothesis) is a logical consequence of a suitably powerful finitely axiomatized theory (e.g., Gödel-Bernays set theory).