Abstract

Lucas and Penrose have contended that, by displaying how any characterisation of arithmetical proof programmable into a machine allows of diagonalisation, generating a humanly recognisable proof which eludes that characterisation, Gödel's incompleteness theorem rules out any purely mechanical model of the human intellect. The main criticisms of this argument have been that the proof generated by diagonalisation will not be humanly recognisable unless humans can grasp the specification of the object-system ; and counts as a proof only on the hypothesis that the object system is consistent. The present paper argues that criticism may be met head-on by an intuitionistic proponent of the anti-mechanist argument; and that criticism is simply mistaken. However the paper concludes by questioning the sufficiency of the situation for an interesting anti-mechanist conclusion.