EL LEGADO DE ALAN TURING / THE LEGACY OF ALAN TURING

ON TURING’S LEGACY IN MATHEMATICAL LOGIC AND THE FOUNDATIONS OF MATHEMATICS

Joan Bagaria

ICREA (Institució Catalana De Recerca I Estudis Avançats) and Departament de Lògica, Història i Filosofia de la Ciència, Universitat de Barcelona.

joan.bagaria@icrea.cat

EL LEGADO DE TURING EN LA LÓGICA MATEMÁTICA Y LOS FUNDAMENTOS DE LAS MATEMÁTICAS

CONTENTS

*This is the written version of the talk with the same title delivered at the “International Symposium: The Legacy of Alan Turing”, held at the Fundación Ramón Areces, Madrid, on 23-24 October 2012.

1. PREAMBLE: THE FOUNDATIONS OF MATHEMATICS IN THE 1930'S Top

David Hilbert (1862-1943), one of the most prominent mathematicians of his time, developed in the 1920's an ambitious programme for laying the foundations of mathematics[1]. New firm foundations were much needed in the wake of the discovery of several paradoxes involving some of the most basic mathematical notions, such as those of infinite sets, or definability. At the beginning of his famous address on The Foundations of Mathematics, delivered at the Hamburg Mathematical Seminar in July 1927, he said (Hilbert, 1928Hilbert, D. (1928). "Die Grundlagen der Mathematik". Abhandlungen aus den mathematischen Seminar der Hamburgischen Universität 6. English translation in J. van Heijenoort (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, 1967.):


I pursue a significant goal, for I should like to eliminate once and for all the questions regarding the foundations of mathematics [...] by turning every mathematical proposition into a formula that can be concretely exhibited and strictly derived. (Hilbert, 1927)


The need for formalization and strict derivation of mathematical statements according to explicitly stated logical rules was the only way, according to Hilbert, to be able to reason about ideal elements, such as actual infinite sets, while avoiding the paradoxes. To attain this goal, Hilbert proposed a foundation for mathematics that he called proof theory, whose goal was to build a formal system consisting of


• A formal language, in which every mathematical statement can be expressed by a formula.

• 
An effectively given list T of formulas, called axioms. These include logical axioms, axioms of equality, and mathematical axioms (including axioms of number, i.e., arithmetical axioms, as well as explicit definitions, and finite and transfinite recursion axioms).


• A finite set of rules of inference for deriving new formulas φ from T, written T ⊢ φ, and read “T proves φ”. In Hilbert's system [Hilbert, 1928Hilbert, D. (1928). "Die Grundlagen der Mathematik". Abhandlungen aus den mathematischen Seminar der Hamburgischen Universität 6. English translation in J. van Heijenoort (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, 1967.] the only rule of inference is the Modus Ponens).


The formal system is not arbitrary, for it is intended to model mathematics in the following sense (Hilbert, 1928Hilbert, D. (1928). "Die Grundlagen der Mathematik". Abhandlungen aus den mathematischen Seminar der Hamburgischen Universität 6. English translation in J. van Heijenoort (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, 1967.):


The axioms and provable propositions, that is the formulas that result from this procedure, are images (Abbildung) of the thoughts constituting customary mathematics as it has developed until now. (Hilbert, 1928Hilbert, D. (1928). "Die Grundlagen der Mathematik". Abhandlungen aus den mathematischen Seminar der Hamburgischen Universität 6. English translation in J. van Heijenoort (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, 1967.)

In a famous passage from his 1925 address On the Infinite, Hilbert expressed the conviction of the solvability of all mathematical problems[2] (Hilbert, 1925Hilbert, D. (1925). "On the Infinite". English translation in J. van Heijenoort (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931. Harvard University Press, 1967.):


... every mathematical problem can be solved. We are all convinced of that. After all, one of the things that attract us most when we apply ourselves to a mathematical problem is precisely that within us we always hear the call: here is the problem, search for the solution; you can find it by pure thoughts, for in mathematics there is no ignorabimus. (Hilbert, 1925Hilbert, D. (1925). "On the Infinite". In van Heijenoort, J. (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931: Harvard University Press, 1967, English translation in J. van Heijenoort.)

Thus, it appears that Hilbert was convinced that his proposed system for the foundation of mathematics, or perhaps some extension of it, could be


Complete: Given a formula φ, either T ⊢ φ or T ⊢ ¬φ.

Further, as an essential requirement for the legitimacy of any formal system strong enough for the foundation of mathematics (hence involving ideal elements), Hilbert wanted a proof of consistency, a proof that should be obtained by purely finitary means (i.e., not involving ideal elements), for he believed that only finitary statements are firmly grounded. Thus, the system should be provably


Consistent: For no formula φ we have
 T ⊢ φ and T ⊢ ¬φ.

And the proof should be finitistic (hence arithmetical).


As Hilbert (1925Hilbert, D. (1925). "On the Infinite". In van Heijenoort, J. (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931: Harvard University Press, 1967, English translation in J. van Heijenoort.) acknowledged,


... my proof theory cannot specify a general method for solving every mathematical problem; that does not exist. (Hilbert, 1925Hilbert, D. (1925). "On the Infinite". In van Heijenoort, J. (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931: Harvard University Press, 1967, English translation in J. van Heijenoort.)


He, however, does not give any argument of why this is so. Yet he seemed to believe that, in addition to being complete and consistent, some formal system based on first-order logic and strong enough to encompass all ordinary mathematics could be


Decidable: There is a definite method, or mechanical process, by which, given any formula φ, it can be determined whether or not φ is provable in the system.


The existence of such an effective method (for any given formal system) is known as the Entscheidungsproblem (the Decision Problem). The Problem had already been posed for different formal systems by Schröder (1895) and Löwenheim (1915). The formulation above was stated in the context of first-order logic by Hilbert and Ackermann in 1928Hilbert, D. and Ackermann, W. (1928). Grundzügen der theoretischen Logik. Springer-Verlag.. Let us observe that completeness implies a positive solution to the Entscheidungsproblem (assuming the axioms are given effectively).


1.1. Incompleteness


In the autumn of 1930, in his retirement address to the Society of German Scientists and Physicians, in Königsberg, and in response to the Latin maxim: Ignoramus et ignorabimus (We do not know, and will not know), Hilbert famously asserted:


Wir müssen wissen. Wir werden wissen. (We must know. We will know.)


Thus, Hilbert was still holding onto the belief that every mathematical problem could be solved, presumably by deriving it from a complete formal system. Ironically, just the day before, during the Conference on Epistemology held jointly with the Society meetings, Kurt Gödel had informally announced his incompleteness result, which represented a fatal blow to Hilbert’s program, at least in the form outlined above. Gödel’s First Incompleteness Theorem asserts that


Theorem 1. Every consistent formal system that contains a small amount of arithmetic is incomplete, i.e., there are formulas φ such that neither T ⊢ φ nor T ⊢ ¬φ.


The amount of arithmetic needed is indeed a very small fragment of Peano’s Arithmetic. For instance, Robinson’s finitely-axiomatizable theory Q suffices.


The second incompleteness theorem is even more dramatic.


Theorem 2. No consistent formal system that contains a moderate amount of arithmetic can prove its own consistency. I.e., the arithmetical statement

CON(T)


that expresses the consistency of the system is not provable in the system itself. Formally,


In this case, the finitely-axiomatizable fragment of Peano’s Arithmetic known as Σ1-Induction suffices. Thus, no reasonable formal system for mathematics (not even for a basic fragment of arithmetic) can be both consistent and complete.


But how about the Entscheidungsproblem? To answer this, one needs to make precise the notion of mechanical process, which leads naturally to the notion of computable function on the natural numbers: Given a formal system, one needs a computable function f such that for any given formula φ, f(φ) = 1 if φ is provable in the system, and f(φ) = 0, otherwise. Since formulas in the relevant formal systems are finite sequences of symbols in a countable alphabet, by coding them by natural numbers, we may assume that f : ℕ → {0, 1}. The question is thus to define precisely the notion of computable function on the natural numbers.


1.2. Princeton


In the 1930’s, Princeton University was the centre of mathematical logic in the United States. The Institute for Advanced Studies (IAS), created in 1930 and housed in the same building as the Department of Mathematics, the old Fine Hall, attracted first-rate mathematicians such as Oswald Veblen and John von Neumann, as well as Albert Einstein. Kurt Gödel visited the IAS on several occasions, giving a series of lectures in 1934 on his incompleteness results, and becoming a permanent member in 1940. In Princeton, Alonzo Church (1903-1995) was the leading figure in Logic. Together with his bright students John Barkley Rosser and Stephen Kleene, Church developed the λ-calculus, a formal system designed to formalize the intuitive notion of effectively calculable function. Church and Kleene introduced a class of effectively calculable functions, called λ-definable, and Church formulated the so-called


Church’s Thesis (First unpublished version, 1934): A function on the natural numbers is effectively calculable if and only if it is λ-definable.

In the meantime, Gödel had introduced his class of computable functions, known as the Gödel-Herbrand general recursive functions, and he had presented them during his 1934 visit to Princeton. Shortly afterwards, Kleene showed that the class of λ-definable functions coincides with the class of Herbrand-Gödel recursive functions, and also with the class of Kleene’s recursive functions, now known simply as recursive. Thus, the first published version of Church’s Thesis reads:


Church’s Thesis (1936): A function on the natural numbers is effectively calculable if and only if it is recursive.


There is a notion of normal form for formulas of the λ-calculus, and in 1935, Church had proved the following:


Theorem 3 (Church, 1936aChurch, A. (1936a). "An unsolvable problem of elementary number theory". Amer. J. of Math, 58 (2), pp. 345-363.). There is no recursive function on the formulas of the λ-calculus such that on any formula C the value is 2 or 1 according as C has a normal form or not.


As a consequence, Church obtains the following:


Corollary 4 (Church, 1936bChurch, A. (1936b). "A Note on the Entscheidungsproblem". The Journal of Symbolic logic, 1 (1), pp. 40-41.). The answer to the Entscheidungsproblem is negative, even for first-order logic
.

That is, there is no effectively computable function on formulas C of first-order logic[3] whose value is 1 or 0 according as C is valid or not (equivalently, by Gödel’s Completeness Theorem, provable or not in the first-order logic calculus).


But is this really a solution to the Entscheidunsproblem? Church’s solution relies on Church’s Thesis, which identifies computable and recursive (as well as λ-definable) functions. Gödel was not convinced. The problem is why should every computable function be recursive?


2. ALAN TURING ENTERS THE SCENE
 Top

Alan Matthison Turing (1912-1954)[4], aged 22, was elected Fellow at King’s College in Cambridge on the basis of a dissertation on the Gaussian Error Function, in which he proved the Central Limit Theorem (which he didn’t know had already been proved in 1922 by J. W. Lindeberg). In the Spring of 1935 Turing took a course by Max Newman on the Foundations of Mathematics, including Gödel’s incompleteness theorems and the Entscheidungsproblem. He immediately started working on the problem, producing in April of 1936 a manuscript entitled On Computable Numbers, with an Application to the Entscheidungsproblem. The paper consists of:


• The analysis of an (idealized) human computer, in the process of computing a computable function on the natural numbers.


• The description of a machine analogue of the human computer: the automatic machines, or a-machines, now known as Turing Machines.


As is well-known, a Turing Machine (TM) is a device consisting of a tape (unbounded at both ends) divided into squares, a head that scans (reads), writes, and erases a symbol (0 or 1) on a given square of the tape, and a finite list of configurations. The TM performs two basic operations: (A) a possible change of symbol in the square being scanned, together with a possible change of configuration, and (B) a possible change of scanned square, together with a possible change of configuration. The operation being performed at any given time is determined by the current configuration and the observed symbol in the scanned square. A TM can thus be described completely by a finite table, detailing the operations, and therefore the table, hence the TM, can be coded by a natural number.


When set in motion starting from a blank tape, a TM produces a sequence of binary numbers. If the sequence is infinite, the machine is called circle-free. Turing calls an infinite sequence of natural numbers computable if it can be computed by a circle-free TM.

• 
A proof of the existence of a Universal Turing Machine.


A Universal Turing Machine (UTM) is a TM that can be used to compute any computable sequence. That is, if the UTM U is set in motion with the code of a TM M written on the tape, then U will produce the same sequence as M. Turing’s UTM has been regarded as the first description of the stored-program computer.


• A proof of the non-computability of the Halting Problem.


The Halting Problem is the problem of determining whether an arbitrary TM is circle-free or not. Turing proves that there is no circle-free TM that will compute the sequence of all codes of circle-free TM’s. Should such a TM exist, there would be a TM M computing the sequence 1-f_n(n), where f_n is the sequence computed by the n-th circle-free TM. If m is the code of M, then f_m(m) = 1-f_m(m), which is impossible.


Turing also proves that there is no TM that, given the code of a TM M, will determine whether the sequence computed by M contains a 0 or not. And the same for 1. In fact, he shows that the computability of the Halting Problem is equivalent to the existence of such TM’s.


• A “proof” that the computable functions (i.e., those computable by a Turing machine) are indeed those that “would naturally be regarded as computable”.


Of course, a real (i.e., mathematical) proof of this assertion is not possible, and so the arguments given by Turing are of three kinds:


(a) A direct appeal to intuition.

(b) 
A proof of the equivalence between computable (i.e., computable by a TM) and effectively calculable (or recursive).


(c) Giving examples of a large class of functions which are computable.

• 
A negative solution to the Entscheidungsproblem
.

For each TM M, he writes a first-order formula Un(M) which says: the symbol 0 appears in the sequence computed by M. Then he proves that (1) if 0 appears on the sequence computed by M, then Un(M) is provable, and that (2) if Un(M) is provable, then 0 appears in the sequence computed by M. In this way a negative solution to the Entscheidungsproblem for first-order logic follows from the non-computability of the Halting Problem.


It is hard to overestimate the importance of Turing’s paper, both for the foundations of mathematics and the theory of computation. With regards to foundations, it is worth noticing Gödel’s enthusiastic reaction (see Gödel, 1964Gödel, K. (1964). "Postscriptum". In Davis, M. (ed.), The Undecidable. New York: Raven, 1965.).


Due to A. M. Turing’s work, a precise and unquestionably adequate definition of the general concept of formal system can now be given ... Turing’s work gives an analysis of the concept of ‘mechanical procedure’ (alias ‘algorithm’ or ‘computation procedure’ or ‘finite combinatorial procedure’). ... A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas. (Gödel, 1964Gödel, K. (1964). "Postscriptum". In Davis, M. (ed.), The Undecidable. New York: Raven, 1965.)


Thus, while Turing (and Chuch, independently) had given a negative solution to the Hilbert-Ackermann version of the Entscheidungsproblem, hence yet a further blow to Hilbert’s Program, he had given for the first time, according to Gödel, a precise definition of the concept of formal system, thus opening the door to a possible revision of the Program.


3. TURING’S DOCTORAL DISSERTATION Top

On the recommendation of Max Newman, Turing got accepted as a graduate student at Princeton. In a letter to Church, Newman writes:


I should mention that Turing’s work is entirely independent; he has been working without any supervision or criticism from anyone. That makes it all the more important that he should come into contact as soon as possible with the leading workers on this line, so that he should not develop into a confirmed solitary.


Turing completed his doctoral dissertation in two years. His thesis, presented in 1938, was entitled Systems of logic based on ordinals. The motivation, clearly stated on the first paragraph, was to avoid as far as possible the effects of Gödel’s incompleteness through the construction of sequences of formal systems of increasing degree of completeness (Turing, 1939Turing, A. (1939). "Systems of Logic based on ordinals". Proc. London Math. Soc., (2), pp. 161-228.):


The well-known theorem of Gödel [...] shows that every system of logic is in a certain sense incomplete, but at the same time it indicates means whereby from a system L of logic a more complete system L’ may be obtained. By repeating the process we get a sequence L, L1 = L’, L2 = L’1 , ... each more complete than the preceding. A logic L_ω may then be constructed in which the provable theorems are the totality of theorems provable with the help of the logics L, L1, L2, ... [...] Proceeding in this way we can associate a system of logic with any constructive ordinal. It may be asked whether a sequence of logics of this kind is complete in the sense that to any problem A there corresponds an ordinal α such that A is solvable by means of the logic L_α. (Turing, 1939Turing, A. (1939). "Systems of Logic based on ordinals". Proc. London Math. Soc., (2), pp. 161-228.)


The following is an example of the formal systems (ordinal logics) studied in his thesis. Let T₀ be the set of axioms of Peano’s Arithmetic (PA). Given T_k, let T_k+1 := T_k + CON(T_k). Then let T_ω := U_k<ω T_k. One can continue into the transfinite by letting T_ω+1 := T_ω + CON(T_ω), and so on. By Gödel’s Second Incompleteness Theorem, T_α+1 is strictly stronger than T_α, whenever T_α is effectively given. But for T_α to be effectively given, the ordinal α must be computable. This leads to the notion of ordinal notations, i.e., a computable way to assign countable ordinals to natural numbers. Let us denote by |a| the ordinal assigned to the natural number a.


The Church-Kleene system O of ordinal notations: The number 1 is a notation for the ordinal 0, 2^a is a notation for the successor of |a| and 3 ⋅ 5^e is a notation for the supremum of the sequence |a_n|, whenever the sequence is strictly increasing and e is the code of a computable function ê such that ê(n) = a_n, for each n.


Observe that the set O of ordinal notations, with the order given by a <_O b if and only if |a| < |b|, forms a tree that splits only at limit levels, and whenever a branch on the tree splits it does it infinitely.


The system T* := 〈T_a〉_aєo is an example of an Ordinal Logic. One might hope that every arithmetical statement φ could be decided by some T_a. That is, either T_a ⊢ φ or T_a ⊢ ¬φ. Since the statement CON(T) is ∏₁⁰, that is, of the form ∀xR(x), where R is some computable relation[5], a natural question is whether every ∏₁⁰ statement could be decided by some T_a. Turing proves the following completeness theorem for ∏₁⁰ statements:


Theorem 5. For every true ∏₁⁰ sentence φ, there exists a Є O with |a| = ω + 1 such that T_a ⊢ φ
.

The proof of the Theorem is quite ingenious (see Feferman, 2012Feferman, S. (2012). "Turing's Thesis". In Alan Turing's Systems of Logic. The Princeton Thesis. Edited by Andrew W. Appel. Princeton University Press.), but as Turing himself recognized, it is disappointing because it is uninformative. Given a ∏₁⁰ sentence φ, he does find an a such that, if φ is true, then a Є O with |a| = ω + 1 and T_a ⊢ φ. But this just shifts the question about the truth of φ to the question about the number a belonging to O, a question that is actually more complex than any arithmetical statement.


3.1. Oracles 


In section 3 of the Thesis, Turing goes on to consider what he calls number-theoretic statements (i.e., ∏₂⁰), namely, those of the form ∀x∃yR(x, y), where R is a computable relation. However, he does not succeed in proving a similar completeness theorem for ∏₂⁰ statements; not surprisingly, for S. Feferman showed in 1962 that this is impossible (Feferman, 1962Feferman, S. (1962). "Transfinite recursive progressions of transfinite theories". J. Symbolic Logic, 27, pp. 259-316.). Then in section 4, and in order to produce concrete examples of problems that are more complex than ∏₂⁰, Turing introduces the notion of computation relative to an oracle
.

Let us suppose that we are supplied with some unspecified means of solving number-theoretic [i.e., ∏₂⁰] problems; a kind of oracle as it were. [...] With the help of the oracle we could form a new kind of machine (call them o-machines), having as one of its fundamental processes that of solving a given number-theoretic problem. (Turing, 1939Turing, A. (1939). "Systems of Logic based on ordinals". Proc. London Math. Soc., (2), pp. 161-228.)


Turing then defines precisely the notion of o-machine (for a fixed oracle o) and formulates the Halting Problem for o-machines, showing that it is not computable by any o-machine, with an argument entirely analogous to the non-computability of the Halting Problem. Since every ∏₂⁰ statement is easily seen to be equivalent to one of the form “M is a circle-free TM”, if o is an oracle that decides every ∏₂⁰ formula, then it follows that the Halting Problem for o-machines is not ∏₂⁰.


Although the notion of o-machine is not pursued any further in Turing’s Thesis, with hindsight it is perhaps the most important notion introduced in that work, for it is the starting point of the study of relative computability.


3.2. Relative computability 


The theory of computability relative to an oracle, was developed by Emil Post (1897-1984) and Kleene into the theory of degrees of unsolvability, also known as Turing Degrees.


A set of natural numbers A is Turing reducible to a set of natural numbers B if A is computable with oracle B. Written A ≤_T B.


Two sets of natural numbers A and B are Turing equivalent, written A ≡_T B, if and only if A ≤_T B and B ≤_T A
.

A Turing Degree is an ≡_T-equivalence class. Let D denote the set of Turing Degrees with the order induced by ≤_T
.

The analysis of the structure of D has produced many fascinating new ideas and techniques, such as the priority method, and is still one of the central areas of modern computability theory. Much is known about D. For example: each degree is countable; there are 2^ℵ0-many degrees; each degree has only countably-many predecessors; D is not dense; for every degree a there is a degree b incomparable with a; there are 2^ℵ0-many incomparable degrees; every two degrees have a least upper bound, but they need not have a greatest lower bound; etc.


The structure of D is indeed very complex. For one thing, every countable partial ordering can be embedded in D. Moreover, the first-order theory of D and the set of theorems of second-order arithmetic are recursively isomorphic (S. Simpson, 1977). Perhaps the most outstanding still open problem about D is whether it is rigid, that is, whether D has a non-trivial automorphism.


3.3. On intuition and ingenuity


In section 11 of the Thesis, entitled “The purpose of ordinal logics”, Turing singles out two faculties of mathematical reasoning he calls intuition and ingenuity
.

The activity of the intuition consists in making spontaneous judgements which are not the result of conscious trains of reasoning. (Turing, 1939Turing, A. (1939). "Systems of Logic based on ordinals". Proc. London Math. Soc., (2), pp. 161-228.)


Whereas


The exercise of ingenuity in mathematics consists in aiding the intuition through suitable arrangements of propositions, and perhaps geometrical figures or drawings. It is intended that when these are really well arranged validity of the intuitive steps which are required cannot seriously be doubted. (Turing, 1939Turing, A. (1939). "Systems of Logic based on ordinals". Proc. London Math. Soc., (2), pp. 161-228.)


By the introduction of formal logic, the need for intuition is


... greatly reduced by setting down formal rules for carrying out inferences which are always intuitively valid. (Turing, 1939Turing, A. (1939). "Systems of Logic based on ordinals". Proc. London Math. Soc., (2), pp. 161-228.)


But since it is not possible to find a formal logic that would eliminate the use of intuition completely, because of Gödel’s incompleteness, one is naturally forced to consider “non-constructive” systems of logic, such as ordinal logics. With an ordinal logic we are in a position to prove theorems by the intuitive steps of recognizing a number as a notation for an ordinal, and the mechanical (yet requiring ingenuity) steps of applying the logical rules.


Further study of ordinal logics, rechristened as transfinite recursive progressions of transfinite theories was carried out in the 1960’s by Feferman (1962Feferman, S. (1962). "Transfinite recursive progressions of transfinite theories". J. Symbolic Logic, 27, pp. 259-316.).


ACKNOWLEDGMENTS
Top

The work was partially supported by the Spanish Ministry of Science and Innovation under grant MTM2011-25229, and by the Generalitat de Catalunya (Catalan Government) under grant 2009 SGR 187.

NOTES Top

REFERENCESTop