David Lewis (1969).

Lucas Arithmetic

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 ability. Lewis dubbed this form of reasoning the Lucas arithmetic.

Lewis defines this arithmetic is the ordinary Peano arithmetic with the addition of an infinitary rule of inference. Peano arithmetic is a formalisation of the arithmetic developed by Giuseppe Peano in the late 19th century. The system uses a set of five axioms to deduce all the truths of ordinary arithmetic.

In ordinary Peno 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 ensure the consistency of the 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 systems of arithmetic each of which contains the Gödel sentences for 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.