On the use of the constructive omega-rule within automated deduction

For many decades, the proponents of `artificial intelligence' have maintained that computers will soon be able to do everything that a human can do. In his bestselling work of popular science, Sir Roger Penrose takes us on a fascinating tour through the basic principles of physics, cosmology, mathematics, and philosophy to show that human thinking can never be emulated by a machine. Oxford Landmark Science books are 'must-read' classics of modern science writing which have crystallized big ideas, and shaped the way we think.

The theories considered here are based on the classical functional calculus (possibly of higher order) together with a set A of non-logical axioms; they are also assumed to contain classical first-order number theory. In foundational investigations it is customary to further restrict attention to the case that A is recursive, or at least recursively enumerable (an equivalent restriction, by [1]). For such axiomatic theories we have the well-known incompleteness phenomena discovered by Godei [6]. Quite far removed from such theories are those based on non-constructive sets of axioms, for example the set of all true sentences of first-order number theory. According to Tarski's theorem, there is not even an arithmetically definable set of axioms A which will give the same result (cf. [18] for exposition).