 In 1936, J. Barkley Rosser made an important improvement that allows one to get rid of the somewhat clumsy assumption of \(\omega\)-consistency in the proof of Gödel’s first theorem. For this purpose, Rosser introduced a new, somewhat artificial “provability predicate” \(\Prov^*(x)\) which was constructed, informally, as follows: