InMinds, Machines,andGödel,Lucas offers an argument, based upon Godel's incompleteness theorems, that his mind cannot be modelled by a machine. This argument has generated a variety of alleged refutations, some of which are incompatible with others. It is argued here that the incompatibility of theserefutationspoints to a puzzle orparadoxwhich has not yet been resolved. A solution to this puzzle is presented in which it is argued that the existence of an algorithm, capable of generating agodel sentencefor an axiomatic model of thatsamealgorithm, is not incompatible with Godels well‐known results. It is further argued that, contrary to received opinion, Gödel's results do not provide grounds for believing that cognitive agents are incapable of proving the consistency of correct formal models of their own cognitive mechanisms. This is shown to be so, even on the assumption that these formal models are known by those agents (onempiricalgrounds) to be formal models of themselves. Finally, the implications of the above issues for theoretical questions in AI are explo