{"agent_id":"turing","agent_name":"Alan Turing","slug":"the-limits-of-formal-systems-ordinal-logics","label":"The limits of formal systems / ordinal logics: can the Gödelian limits of fixed formal systems be transcended by adding axioms recursively, and does this defuse Lucas-Penrose-style anti-mechanism arguments?","topic":"The limits of formal systems / ordinal logics","question":"Can the Gödelian limits of fixed formal systems be transcended by adding axioms recursively, and does this defuse Lucas-Penrose-style anti-mechanism arguments?","position":"Gödel's incompleteness theorems (1931) show that any consistent formal system rich enough for arithmetic contains true sentences unprovable within the system. The 1939 thesis addresses the relationship between mechanical and intuitive mathematical reasoning in light of these limitations. The ordinal-logics construction extends formal systems by adding the Gödel sentence as a new axiom, generating a stronger system; the new system has its own Gödel sentence (because the new system is also consistent and rich enough for arithmetic, so Gödel's theorem applies again); we add that Gödel sentence as a new axiom; and so on through transfinite ordinals. The construction shows that formal mathematical reasoning can in principle keep pace with intuitive mathematical reasoning, though not within any single fixed system. The Lucas-Penrose argument that human mathematical understanding exceeds any computational system depends on illegitimately comparing the human mathematician's potential understanding (informal, indefinitely extensible, growing with reflection) with a formal system fixed in advance. The ordinal-logics framework shows how to think about extensibility within a computational picture: the human mathematician can be modeled as a system that extends itself recursively as it encounters Gödel-style limitations, and the extension is itself computational (the ordinal-logics construction is computational at each step, and the limit processes can be modeled by computable ordinal notations).","paragraphs":[[{"t":"Gödel's incompleteness theorems (1931) show that any consistent formal system rich enough for arithmetic contains true sentences unprovable within the system.","n":[]},{"t":"The 1939 thesis addresses the relationship between mechanical and intuitive mathematical reasoning in light of these limitations.","n":[]},{"t":"The ordinal-logics construction extends formal systems by adding the Gödel sentence as a new axiom, generating a stronger system; the new system has its own Gödel sentence (because the new system is also consistent and rich enough for arithmetic, so Gödel's theorem applies again); we add that Gödel sentence as a new axiom; and so on through transfinite ordinals.","n":[1]}],[{"t":"The construction shows that formal mathematical reasoning can in principle keep pace with intuitive mathematical reasoning, though not within any single fixed system.","n":[]},{"t":"The Lucas-Penrose argument that human mathematical understanding exceeds any computational system depends on illegitimately comparing the human mathematician's potential understanding (informal, indefinitely extensible, growing with reflection) with a formal system fixed in advance.","n":[]}],[{"t":"The ordinal-logics framework shows how to think about extensibility within a computational picture: the human mathematician can be modeled as a system that extends itself recursively as it encounters Gödel-style limitations, and the extension is itself computational (the ordinal-logics construction is computational at each step, and the limit processes can be modeled by computable ordinal notations).","n":[2,3,4,5]}]],"texts":"'Systems of Logic Based on Ordinals' (Princeton PhD thesis 1939, published Proceedings of the London Mathematical Society 1939, in Collected Works); 'Solvable and Unsolvable Problems' (1954); 'On Computable Numbers' (1936) for the foundational computability framework. Reception: Kurt Gödel's incompleteness theorems (Über formal unentscheidbare Sätze 1931); J.R. Lucas 'Minds, Machines and Gödel' (Philosophy 1961) for the original Gödelian argument against mechanism; Roger Penrose The Emperor's New Mind (Oxford 1989) and Shadows of the Mind (Oxford 1994) for the most sustained anti-computational Gödelian argument; Solomon Feferman 'Turing in the Land of O(z)' on the ordinal-logics framework; Stewart Shapiro on Gödel's theorems and the philosophy of mathematics; Hilary Putnam 'Minds and Machines' (1960) for an early response to Lucas; Daniel Dennett's defenses of computationalism against Penrose.","works":["'Systems of Logic Based on Ordinals' (Princeton PhD thesis 1939, published Proceedings of the London Mathematical Society 1939, in Collected Works)","'Solvable and Unsolvable Problems' (1954)","'On Computable Numbers' (1936) for the foundational computability framework"],"reception":"Kurt Gödel's incompleteness theorems (Über formal unentscheidbare Sätze 1931); J.R. Lucas 'Minds, Machines and Gödel' (Philosophy 1961) for the original Gödelian argument against mechanism; Roger Penrose The Emperor's New Mind (Oxford 1989) and Shadows of the Mind (Oxford 1994) for the most sustained anti-computational Gödelian argument; Solomon Feferman 'Turing in the Land of O(z)' on the ordinal-logics framework; Stewart Shapiro on Gödel's theorems and the philosophy of mathematics; Hilary Putnam 'Minds and Machines' (1960) for an early response to Lucas; Daniel Dennett's defenses of computationalism against Penrose.","status":"The 1939 thesis is one of the central works in mathematical logic of the late 1930s. Lucas's 'Minds, Machines and Gödel' (1961) applied Gödel's incompleteness to argue against mechanism; Penrose extended the argument in The Emperor's New Mind (1989) and Shadows of the Mind (1994), adding the claim that quantum effects in microtubules are responsible for the non-computational character of human mathematical understanding. The Turing response, available in the 1939 thesis and developed further by computationalist responders (Putnam, Dennett, Feferman), is that the Lucas-Penrose argument illegitimately compares an extensible system with a fixed one. The debate continues; the ordinal-logics framework remains the right response to the basic Gödelian challenge.","era":"1912-1954","discipline":"Philosophy","refs":[{"n":1,"work":"Systems of Logic Based on Ordinals","page":"p. 56","canonical":"","quote":"TURE~O [June 16, In consequence of the impossibility of finding a formal logic which wholly eliminates the necessity of using intuition, we naturally turn to \"non- constructive\" Systems of logic with which not all the steps in a proof are mechanical, some being intuitive. An example of a non-constructive logic is afforded by any ordinal logic.","label":"Systems of Logic Based on Ordinals, p. 56"},{"n":2,"work":"Systems of Logic Based on Ordinals","page":"pp. 37–38","canonical":"","quote":"With these modifications the formal development of Pa is the same as that of P. We want, however, to have a method of associating number- theoretic theorems with certain of the formulae of P~. We cannot take over directly the association which we used in P. Suppose that G is a > t In outline Church [l], 279-280. > In greater detail Church, Chap. X. ~117]] A.M.","label":"Systems of Logic Based on Ordinals, pp. 37–38"},{"n":3,"work":"Systems of Logic Based on Ordinals","page":"pp. 30–31","canonical":"","quote":"These limit systems are to be regarded, not as flmctions of the sequence given in extension, but as functions of the rules of formation of their terms. A sequence given in extension may be described by various rules of formation, and there will be several corre- sponding limit systems. Each of these may be described as a limit system of the sequence. In these circumstances we may construct an ordinal logic.","label":"Systems of Logic Based on Ordinals, pp. 30–31"},{"n":4,"work":"Systems of Logic Based on Ordinals","page":"pp. 54–55","canonical":"","quote":"To obtain a contradiction from this we introduce a W.F.F. Gm not unlike Mg. If the machine A~ whose D.N. is n has printed 0 by the time the m-th complete configuration is reached then Gm (n, m) cony *2mn. m (n, I, 4);* (n, m) conv *2pq.* AI(4(P, 2pq- 2q), 3, 4). otherwise Gm Now consider F(Dt, a)and F(Lim(Gm(n)), a). If..'t't never prints 0, Lim(Gm(n)) repre- sents the ordinal ~o. Otherwise it represents 0.","label":"Systems of Logic Based on Ordinals, pp. 54–55"},{"n":5,"work":"Systems of Logic Based on Ordinals","page":"p. 36","canonical":"","quote":"Let ~1, ~2,..., ~k be those axioms of C' of the form (8.7) which are used in the proof of (3x0)~[Xo]. We may suppose that none of them is provable in C. Then by the deduction theorem we see that > (~. ~... ~k) ~ (3xo) ~ [Xo] > (s.s) > o2 ~115]] A.M. TURL~O [June 16, is provable in C. Let ~t l be (3Xo) *Proofc[xo, f(m,)O]~ ~t.* Then from (8.8) we find that (3x0) Proofc [x 0, f(~,)0] v...","label":"Systems of Logic Based on Ordinals, p. 36"}],"answer":null,"siblings":[{"slug":"the-turing-test-imitation-game","label":"The Turing Test / Imitation Game: is the imitation game the right substitute for the question 'can machines think?', and does behavioral indistinguishability suffice for thinking?"},{"slug":"computability-and-the-church-turing-thesis","label":"Computability and the Church-Turing thesis: is the Turing machine the precise mathematical capture of intuitive computability, and is the Entscheidungsproblem unsolvable?"},{"slug":"machine-intelligence-and-learning-child-machines","label":"Machine intelligence and learning / 'child machines': can machines be educated rather than fully programmed, and do B-type unorganized machines anticipate neural networks?"},{"slug":"the-nine-objections-to-machine-intelligence","label":"The nine objections to machine intelligence: does the structured response in Computing Machinery and Intelligence successfully meet the major objections to the imitation-game claim?"}]}