  Gödel’s Completeness theorem was not sufficient, however, to give a positive solution to the entscheidungsproblem. Given a formula, \(\varphi\), if \(\varphi\) is valid then the above procedure would eventually list it out and thus could answer, “Yes, \(\varphi\) is valid.” However, if \(\varphi\) were not valid then we might never find this fact out. What was missing was a procedure to list out all the non-valid formulas, or equivalently to list out all satisfiable formulas.