 He proved formally that no Turing machine can tell, of each formula of the predicate calculus, whether or not the formula is a theorem of the calculus (provided the machine is limited to a finite number of steps when testing a formula for theoremhood). So, given his thesis that if an effective method exists then it can be carried out by one of his machines, it follows that there is no such method. 