Argument from Gödel's theorem is dialectical
A mechanist presents Lucas with a machine model of Lucas's mind. Lucas shows that he can recognise the truth of the machine's Gödel sentence—whereas the machine can't. In this way, Lucas can defeat any mechanist attempts to reduce him to a machine.
The Lucas argument involves a hypothetical game played between Lucas and mechanist.
David Lewis (1969) proposed that the real issue in the Lucas argument is the form of arithmetic that Lucas uses in discussing his own mathematical activity. Lucas dubbed this form of reasoning the Lucas arithmetic.
Lewis defines this arithematic as the ordinary Peano arithematic with the addition of an inflationary rule of inference. Peano arithmetic is a formalization of arithematic developed by Guissepe Peano in the late 19th century. The system uses a set of 5 axioms to deduce all the truths of ordinary arithmetic.
In ordinary Peano arithmetic, the consistency of the system cannot be proven within the system; this would violate Gödel's second theorem. The addition of an infinitary rule, however, allows us to infer the consistency of a formal system from within that system without violating Gödel's second theorem.
When fully worked out, the Lucas arithmetic includes all of the Gödel sentences of all systems powerful enough to produce arithmetic. As such, it includes an entire hierarchy of of systems of arithmetic, each of which contains Gödel sentences for all the lower-level systems in the hierarchy.
Note: The method of adding an infinitary inference rule to Peano arithmetic was developed by Gerhard Gentzen, in 1936.