Talk:Entscheidungsproblem

From Wikipedia, the free encyclopedia

Socrates
Philosophy Portal
This article is within the scope of the WikiProject Philosophy, which collaborates on articles related to philosophy. To participate, you can edit this article or visit the project page for more details.
B This article has been rated as B-Class on the quality scale.
Mid This article has been rated as mid-importance on the importance scale.

Contents

[edit] Talk page cleaned up

I deleted the rambling that was here. Wikipedia is not a place to publish new ideas. CMummert · talk 14:31, 12 January 2007 (UTC)


[edit] Holding place, taken from history on Turing machine page

[edit] Origin of the Entscheidungsproblem:

The origin of the Entscheidungsproblem goes back to Gottfried Leibniz. In the late 1600's, after having constructed a successful mechanical calculating machine, Leibniz dreamed of building a machine that could manipulate symbols in order to determine the truth values of mathematical statements (Davis 2000:3-20). He realized that the first step would have to be a clean formal language, or what he called a lingua characterica. Much of his subsequent work was directed towards that goal but had no lasting influence. In fact, George Boole, without knowledge of Leibniz' work (cf Gratten-Guiness and Bornet 1997:xliii), devised a "calculus" of logic (ironically not accepting the possibility of the logical OR X+X = X discovered by Leibniz (Davis 2000:18) and yet proposing X*X = X; Stanley Jevons subsequently argued with Boole for the acceptability of the logical OR (Gratten-Guiness and Bornet 1997:xiv)).

Then in 1879, Frege presented his " Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought". About this Frege states:

"In fact, what I wanted to create was not a mere calculus ratiocinator but a lingua characterica in Leibniz's sense." (van Heijenoort 1967:2).

Bertrand Russell and Alfred North Whitehead subsequently reworked Frege’s peculiar symbolism into a more "user friendly" format that would appear in 1914 as Principia Mathematica. This, together with Guiseppe Peano’s axioms of arithmetic (1899) would, through the efforts of many mathematicians over the next 30 years, evolve into the langua characterica that Leibniz had sought.

[edit] 1901: Russell’s Paradox:

In 1901 Bertrand Russell sent a letter to Frege, pointing out a problem with Frege's logic by creating a simple paradox, now called Russell's paradox. It represented a problem that simply refused to go away and would, 30 years later, bring down David Hilbert's "program" to reduce all of mathematics to symbol-manipulation.

[edit] 1905: Richard's Paradox:

[Unlike the Russell paradox which involves "sets", but like the Barry paradox, this is a paradox of language, and the use of language. Very simple to state. Careful examination makes the reader Rather uncomfortable because of hidden assumptions and little errors in its original form (a letter). Makes use of Cantor's diagonal argument. Problem of language addressed only cursorily by Finsler (1926) but in great depth (i.e. central argument) by Gödel (1931). "Both Godel's and Finsler's arguments, with their similarities and differences, skirt the Richard paradox without falling into it; both exploit Richard's argument to obtain new and valid conclusions" (van heijenoort 1967:439).

[edit] 1900: The Entscheidungsproblem (the "decision problem") expressed in Hilbert's tenth question

In 1900 the famous mathematician David Hilbert posed a set of problems -- now known as Hilbert's problems – his beacon illuminating the way for mathematicians of the twentieth century. The 2nd problem asked for a proof that “arithmetic” is “consistent”. Kurt Gödel would prove in 1931 that, within what he called “P” (nowadays called Peano Arithmetic), “there exist undecidable sentences [propositions]” (Gödel in Davis 1965:6, in van Heijenoort 1967:596). Because of this, “the consistency of P is unprovable in P, provided P is consistent”(Gödel’s theorem IX, Davis 1965:36). While Gödel’s proof would display the tools necessary to resolve the Entscheidungsproblem, he himself would not answer it for reasons described below.

It is within the 10th problem where the question of an "Entscheidungsproblem" actually appears, but the question would float about for almost 30 years before it was framed precisely. (The 10th problem itself was resolved in the negative in 1970; its resolution in turn required the tools developed to answer the Entsheidungsproblem). Hilbert's original description of #10 is as follows:

"10. Determination of the solvability of a Diophantine equation. Given a Diophantine equation with any number of unknown quantities and with rational integral coefficients: To devise a process according to which it can be determined in a finite number of operations whether the equation is solvable in rational integers.
"The Entscheidungsproblem [decision problem for first-order logic] is solved when we know a procedure that allows for any given logical expression to decide by finitely many operations its validity or satisfiability . . . The Entscheidungsproblem must be considered the main problem of mathematical logic. . .. The solution of the Entscheidungsproblem is of fundamental significance for the theory of all domains whose propositions could be developed on the basis of a finite number of axioms" (this translation, and the original text in German, appears in Dershowitz and Gurevich 2007:1-2).

By 1922, the specific question of an "Entscheidungsproblem" applied to Diophantine equations had developed into the more general question about a “decision method” for any mathematical formula, and H. Behmann stated that

". . . most general form of the Entscheidungsproblem [is] as follows:
"A quite definite generally applicable prescription is required which will allow one to decide in a finite number of steps the truth or falsity of a given purely logical assertion. . ." (Gandy 1994:57 quoting Behmann)
"Behmann remarks that . . . the general problem is equivalent to the problem of deciding which mathematical propositions are true." (Gandy 1994:57)

Martin Davis explains it this way: Suppose we are given a "calculational procedure" that consists of (1) a set of axioms and (2) a logical conclusion written in first order logic, that is -- written in what Davis calls "Frege's rules of deduction" (or the modern equivalent of Boolean logic). Gödel's doctoral dissertation (1930) proved that Frege's rules were complete "...in the sense that every valid formula is provable" (van Heijenoort, p. 582). Given that encouraging fact, could there be a generalized "calculational procedure" that would tell us whether a conclusion can be derived from its premises? Davis calls such calculational procedures "algorithms". The Entscheidungsproblem would be an algorithm as well. "In principle, an algorithm for [the] Entscheidungsproblem would have reduced all human deductive reasoning to brute calculation" (Davis 2000:146).

In other words: Is there a “decisional algorithm” that can tell us if any algorithm is "true" (i.e. an algorithm that always correctly yields a judgment "truth" or "falsehood"?)

” . . . it seemed clear to Hilbert that with the solution of this problem, the Entscheidungsproblem, that it should be possible in principle to settle all mathematical questions in a purely mechanical manner. Hence, given unsolvable problems at all, if Hilbert was correct, then the Entscheidungsproblem itself should be unsolvable" (Davis 1967:108).

Indeed: What about our Entscheidungsproblem algorithm itself? Can it determine, in a finite number of steps, whether it, itself, is “successful” and "truthful" (that is, it does not get hung up in an endless “circle” or “loop”, and it correctly yields a judgment "truth" or "falsehood" about its own behavior and results)? Within this question Russell's paradox (and Cantor’s diagonal argument) is reasserting itself with a vengeance.

[edit] 1926: Finsler's (arguable) first demonstration of an undecidable proposition

[Requires understanding of the Richard paradox (1905). Finsler rightly shows the undecidability of a provable statement (known to be false outside the system) rather the undecidability of a true or a false statement. [insert Godel quote here from his 1970]. Godel trashes Finsler's argument in an unpublished letter (1970). [insert nasty Godel 1970 here to make point that the matter involves a "system system"].others (Hilbert and Bernays 19xx) were (somewhat) accepting, goobut when Finsler attempted to claim priority Godel brushed him off [insert quote here from Breger 1992: "Finsler strives for truth in mathematics, not just for formal derivability" (p. 255) "According to Hilbert and Bernays (1939...; compare also Bernays 1935...) the central idea of Finsler's paper is remarkable and should be given due respect, but his contention is merely analogous to Godel's theorem, and his reasoning cannot be put to use by proof theory" (p. 257)], his proof lapsing into oblivion. van Heijenoort 1967 and more recent commentators yield conflicting/confusing opinions. ]

[edit] 1928: Hilbert further defines the Entscheidungsproblem

By the 1928 international congress of mathematicians, Hilbert "made his questions quite precise. First, was mathematics complete . . . Second, was mathematics consistent. Third . . . was mathematics decidable?" (Hodges p. 91, Hawking p. 1121).

Hodges describes it this way: "By the 1928 international congress of mathematicians, Hilbert "made his questions quite precise. First, was mathematics complete in the technical sense that every statement . . . could be proved, or disproved. Second, was mathematics consistent, in the sense that the [false] statement ‘2 + 2 = 5’ could never be arrived at by a sequence of valid steps of proof. And thirdly, was mathematics decidable?" By this he meant, did there exist a definite method which could, in principle, be applied to any assertion, and which was guaranteed to produce a correct decision as to whether that assertion was true.” (Hodges 1983:91).

[edit] 1931: True ≠ Provable: Gödel's undecidability theorem VI (the so-called "first incompleteness theorem")

The "first incompleteness theorem" appears as "Theorem VI" in his 1931 paper On Formally Undecidable Propositions in Principia Mathematica and Related Systems I. In Gödel's original notation, it states:

"The general result about the existence of undecidable propositions reads as follows:
"Theorem VI. For every ω-consistent recursive class κ of FORMULAS there are recursive CLASS SIGNS r, such that neither v Gen r nor Neg(v Gen r) belongs to Flg(κ) (where v is the FREE VARIABLE of r).2 (van Heijenoort translation and typsetting 1967:607. "Flg" is from "Folgerungsmenge = set of consequences" and "Gen" is from "Generalisation = generalization" (cf Meltzer and Braithwaite 1962, 1992 edition:33-34) )

In 1930-1 Kurt Gödel, by the proof of his undecidability theorem IV and the consequences thereof (in particular Theorem XI, the second so-called "incompleteness theorem"), answered the first two questions NO. But in order to do this he had to first demonstrate an undecidable assertion (sentence, proposition).

The approach that Gödel took is simular to that taken by Finsler (1926). First, like Finsler, he does not employ the assertion "x is [or is not] true" but rather, he employs "x is [is not] provable". Second, like Finsler he employs Cantor's diagonal method (although his usage is subtle whereas Finsler's is obvious).

"Some form of diagonalization argument lies at the basis of most proofs, or perhaps of every proof, of the undecidability theorm and of the first incompleteness theorem..."(Franzen 2005:70)

Indeed, in this context the diagonal argument is used by Gödel (1931), Church (1934), Turing (1936-7), and Kleene (1952).

Third, unlike Finsler, Gödel expresses his assertions "x is [is not] PROVABLE" within a tightly-defined system of arithmetic, i.e. a tiny collection of symbols, axioms and formation rules that define "the numbers" and the total functions of common arithmetic (e.g. "add", "multiply", "raise to a power", "divide" etc). So just what does PROVABLE mean?

"A formula is provable if a proof of it exists" (Godel 1934:p.41)

Gödel's notion of "a proof" is not what the student learns in geometry. In his "proof" the last axiom or "formula" must follow "immediately from" (as an "immediate consequence" of, ) the preceding axiom(s) and/or formula(s):

"A finite sequence of formulas shall be a proof (specifically, a proof of the last formula of the sequence) if each formula of the sequence is either an axiom, or an immediate consequence of one or more of the preceding formulas" (Godel 1934:p.41).

This definition is difficult. It contains many hidden (tacit) assumptions/definitions such as "sequence", "last", "immediate consequence", "preceding". But unlike Finsler, Gödel attempts to clear these issues up in his "rigorous execution of the proof" (Gödel 1934 as the quote appears in Davis 1965:9), or as translated by van Heijenoort "with full precision" (p.599).

For Gödel a "formula" is a sequence of axioms or a sequence of formulas or a combined sequence of axioms and formulas. So as shown in the example below for "CLEAR x" (x is a register, CLEAR means "empty" or "make equivalent to zero"), the "formula" is actually a sequence of axioms with numbers substituted for the variables. Similar formulas can be written for any arithmetic or logic formula such as "ADD_TO_A B", "LOAD_A_WITH C", "STORE_A_IN B", "AND_TO_A B" etc. But even Godel's axiomatic treatment has "tacit" axioms:

"In other words, the know-how of a human being is necessary -- a know-how which is not formalized in the axioms...It seems to me that Hilbert...was also aware of this fundamental problem of an axiomatic approach.... Evidentally the know-how which is necessary to understand a certain piece of written formal logic is usually hidden" ((cf Berger Tacit Knowledge and Mathematica knowledge 2000:227-228).

Godel's formulas and the scheme he used to convert them to numbers is complex. A simpler example might be useful. Perhaps from it we can to see what Godel was up to, and to see if, and if so where, any other tacit assumptions are hiding.

A very simple, but very powerful, computational "system" is the Turing-equivalent counter machine, an abstract computational model that we call "M". This M should behave like primitive recursion, that is, work from a tiny set of 5 "number-theoretic formulas/formation-schemata (word used by Godel 1931:12 in U, also Kleene 1952:219). The following is Kleene's list (1952:219) and a similar list was used by Godel:

The Kleene list:

  • (I) successor function
  • (II) constant function
  • (III) identity or "projection" function
  • (IV) definition by substitution
  • (V) definition by primitive recursion (2 types, the first one similar to Godel's that starts from 0th case and is over one variable)

The Godel list: ≡≠⇒⋀⊗ℵ↑∆←⊆∉∈∸→⊂∀∃ℕ∩∪ǎăℬ⇔

  • (I) Peano axioms: 0 exists and has no successor, IF x' = y' THEN x = y, primitive recursion starting from the 0th case and is over one variable).
  • (III) The 4 base axioms of Principia Mathematica
  • (III) Substitution
  • (V) identity or projection function: (∃u)(∀v (u(v)≡ a)). A function u exists, such that for all formulas v used in formula u, the formula v ≡ a can be plucked out of the bunch of them. Here a is a formula that does not contain u free, and I am using modern symbols ∃ and ∀ and modern usage.
"This axiom represents the axiom of reducibility (comprehension axiom of set theory)" (ibid p. 13) [what is this axiom ??]
  • (VI) Type-elevation: x1 ∀ (x2(x1) ≡ y2(x1) --> x2 = y2
"This axiom asserts that a class is completely determined by itself" (ibid p. 13)
  • "c is an immediate consequence of" a and b (of a) if a is the formula (~b)V(c), where c is the formula ∀v(a) <= ??

Our machine will be the Melzak model (holes in the ground), but simplified to the Lambek model (the abacus model, cf B-B-J 2002:45ff), and further modified into the Peano axioms (see Minsky 1967:201, also Shepherdson-Sturgis ??): A line of holes (aka "registers") begins with a hole (of potentially unbounded size) labelled 1, an unlimited source S of pebbles to be put into the holes, and a mechanism that is capable of following a set of instructions in a TABLE with respect to the holes and pebbles. The holes in the ground are the "variables" and will be of only type I. The numbers are the collections of pebbles in the ground. The set of instructions that the mechanism follows will be:

(1) Constant function: CLR_A [should I use the indirection method? CLRi]: : clear a hole called "1" of pebbles (aka hole "A") (2) Successor function: INC_A [should I use the indirection method? INC_A]: add a single pebble to the hole labelled "1" (3) Identity function: ldAi, MOVrAi, CPYrAi[here I have to use the indirection method]: From the entire sequence of holes, find the hole, the number of which, is the quantity of pebbles in hole "2" (aka P) Use this procedure. remove all the pebbles from the hole labelled "2" (aka "P" for "pointer"). Start with hole 1 and put the pebbles in one-to-one correspondence with the holes until the pebbles run out: the hole where this happens is the hole of interest. (4) Substitution function: stAi In a manner similar to ldAi, find the hole of interest. Then remove all the holes from pointer-hole #2 (aka P) [either throw them into the pointed-to hole, or count out a similar number from the source S and throw those into P; replace the counters into hole A (aka #1). CPYAri ?? (5) Recursion function and mu-operator combined (see Minsky 1967: After each instruction the following will occur. Also, there is a specific IF-THEN operation JZ as follows: Test hole #1 to see whether or not said hole is empty of pebbles. If empty go to the instruction marked "[A]=Z" else go to the "[A]≠Z". OR: two holes J1 and J2... no, still must either go to next instruction

The Universal program: The TABLE of instructions for U must know the exact construction of the program-instruction set, where its dedicated registers reside, and where the starting program-instruction will be. Note that the program-instruction set need not be the same as the TABLE-instruction set; in fact, in our example it will not be.

Godel's second restriction, a rather onerous one, is as follows. Because diagonalization arguments (and Godel's argument) operate only on "functions of a single variable" (Godel 1934:Undecidable p.46), the model must be modified so we can create only single-variable formulas. This, as we see below, forces us into defining sequences of recursive formulas. Gödel commented on why this is possible in a "Remark: Variables for functions (relations) of two or more arguments are superfluous as primitive symbols since one can define relations [functions] as classes of ordered pairs [etc]..."(Davis translation 1965:10).

Another outcome of this second restriction will be the following: "Formulas" (that is, sequences of axioms or other formulas) must have one entry-point "at the top", and one exit-point "at the bottom." Godel's (very important) "immediate consequence" formula #43 Fl(x, y, z) ("Fl" from "Fogle" i.e. "consequence" (cf Meltzer-Braithwaite 1962:33) makes use of a similar notion. To say that a formula "x is an immediate consequence of formulas y and z" means that EITHER (1) y=z implies x OR (2) there exists some bound-variable "v" and x = v for function y "generalized over variable v". [THIS ISN'T QUITE RIGHT BUT ITS CLOSE]. The term (1) takes care of axioms and term (2) takes care of some preceding formula y. But the point is that either y=z --> x or y&z --> x ( (z & z-->y) & (y & y-->x) => x ).

The Cantor diagonalization method requires that all the axioms for all their possible parameters (i.e. CLEAR 1, CLEAR 2, ... CLEAR N, INCREMENT 1, INCREMENT 2, ... INCREMENT N, etc) and all the possible "formulas" such as ADD_TO_A B", "LOAD_B_FROM C", "MULTIPLY_A_BY M", "STORE_A_IN P" etc must be "enumerable" -- convertable to numbers and countable, to boot.

Given that Godel was able to display “undecidable sentences [propositions]” Gandy can now answer the question posed above about what happens when we submit our Entscheidungsproblem algorithm to itself for testing:

”For any such system Σ Gödel constructs a formula φ which is satisfiable, but for which this fact cannot be proved in Σ. As a consequence, given any proposed algorithm α for the Entscheidungsproblem and any system Σ, either it cannot be proved in Σ that α always gives an answer, or it cannot be proved in Σ that its answer is always correct.” (Gandy 1994:63)

So why didn’t Gödel just go ahead and prove the undecidability of the Entscheidungsproblem? Gandy supposes that first “one needed to reflect long and hard on the idea of calculability” (Gandy 1994:64). The ever-cautious Gödel was unconvinced that either Church’s λ-definability or even his own forms of "recursion" (primitive recursion in Gödel 1931, eventually augmented into “Herbrand-Gödel” recursion by the mid-1930's) was adequate to the task. Besides, the question requires finite means, and Gödel was more interested in “nonfinist concepts and methods” (Gandy 1994:64). So, the third question — the Entscheidungsproblem — would have to wait until the mid-1930's.

[edit] 1931-1935: Effective calculability: λ-calculus? Recursion? Machine computation?

The problem was: An answer to the Entscheidungsproblem first required a precise characterization – a definition, an hypothesis/conjecture, or better yet, an axiomization -- of the notion of "definite general applicable prescription" or what Alonzo Church would come to call "effective calculability (cf part "7. The notion of effective calculability" in Church 1936:100 in The Undecidable). Even the form of the characterization – should it be a definition, or a hypothesis, or an axiomization? – would come under debate.

In 1928 no such characterization existed. But over the next 6–7 years Princeton professor Church and his two students Stephen Kleene and J. B. Rosser would propose a "definition" by use of Church's λ-calculus and Herbrand-Gödel’s recursion theory -- i.e. Gödel's primitive recursion modified by a suggestion of Jacques Herbrand. Then Emil Post would propose his so-called “working hypothesis” (of a worker moving from room to room writing and erasing marks per a list of instructions) (Post 1936), and lastly a few months later (1936-7) Alan Turing would follow up with his proposed "a- (automatic) machine" (closer to an axiomization but still not considered by some to be fully axiomatized, cf Gandy 1980, Sieg 1998, Moschovakis 2001, Dershowitz and Gurevich 2007).

[edit] 1935: Church’s proof

Indeed, Church's paper (presented to the American Mathematical Society 19 April 1935, published 15 April 1936) showed that an undecidable problem did exist. Church states the purpose of his paper this way:

”The purpose of the present paper is to propose a definition of effective calculability2 which is thought to correspond satisfactorily to the somewhat vague intuition notion . . . and show, by means of an example, that not every problem of this class is solvable.”

In footnote 2, Church states that “definition of effective calculability can be stated in either of two equivalent forms, (1) . . . if it is λ-definable, (2) . . . it is recursive in the sense of [Herbrand-Godel modified by Kleene]" (U. p. 90). Furthermore in this definition he uses the criterion “the algorithm has terminated becomes effectively known” (U p. 100).

An explanation of Church’s example is beyond the reach of this article. Gandy explains (cf Gandy 1994:81-2) that within all the undecidability proofs (Church’s, Kleene’s and Turing’s) the method involves (1) Enumeration -- An algorithmic-like method to list all possible well-formed functions F of a single variable m, assign a number to m, convert each parametrized-function “F of m” Fm to a Gödel number G(Fm), and put the G(Fm) in numerical order; (2) A successful demonstration that each parameterized-function Fm (and as a consequence its Gödelization G(Fm)) is a total function, i.e. to match the Gödelized G(Fm) to the correct Gödelized answer G(n), (3) Use of Cantor’s diagonal method to derive a contradiction when the function F is the decision procedure D acting on its own number i.e. G(D(D)) =? G(“True”? or “False”?).

Within the year Church would go on to strengthen his result, and in a paper titled A Note on the Entscheidungsproblem (April 1936) he would show that:

“The general case of the Entscheidungsproblem 7 of the [logical] system L is unsolvable.”
”7. The Entscheidungsproblem of a system of symbolic logic is here understood [in the sense of what is called the "deducibility problem" below, that is, as] the problem to find an effective method by which, given any expression Q in the notation of the system, it can be determined whether or not Q is provable in the system. Hilbert and Ackerman (loc. cit) understand the Entscheidungsproblem of the engere Funktionenkalkül [first order functional calculus] in a slightly different sense. But the two senses are equivalent in view of the proof by Kurt Gödel and the completeness of the engere Funktionenkalkül . . . .” (brackets in the original, Church 1936 :’’The Undecidable’’ p. 113)

Church sees two forms of the question: (i) “a constructive proof of the unsolvability of what we may call the “deducibility problem” of the engere Funktionenkalkül, that is the problem to find an effective procedure which is capable of determining, about any given expression in the notation of the engere Funktionenkalkül, whether it is decidable in that system; (ii) “ . . . a procedure for determining universal validity, [that] depends upon the non-constructively proved theorem of Gödel that every universally valid expression is deducible in the engere Funktionenkalkül, as well as on the assumption of the converse of this, that every deducible expression is universally valid.”

Church wondered : Had he proven case (ii) beyond a doubt? His proof relies upon Gödel’s completeness theorem (i.e. his PhD thesis, not his so-called incompleteness theorems), and Church noted (and Davis reiterates on 1965:108-109, and in 2000:114-5) that this is a “non-constructive” proof i.e. it relies on the use of reductio ad absurdum and consequently, the Law of Excluded Middle, an anathema to mathematicians with an intuitionistic outlook.

[edit] 1931-1937: A flurry of activity

Church beat Alan Turing to the punch by almost a year (Turing's paper received 28 May 1936, published January 1937).

Without knowledge that Church-Kleene-Rosser at Princeton had been working on the same problem, Turing, a Master's student at King's College, Cambridge UK, was approaching his characterization of "effective calculability" from a much different angle. And, the appearance of Church’s proof spurred Emil Post to publish; he too had been working in obscurity for a number of years, and he quickly submitted a brief paper in the fall of 1936 that offered as his "working hypothesis" of "effective calculability" a “process” (a man moving through a sequence of boxes marking and erasing per a list of instructions) very similar to Turing's a-machine. Moreover in a footnote he took a poke at Church's notion of a "definition" for effective calculability: Church’s definition would “mask this identification under a definition [and hide] the fact that a fundamental discovery in the limitations of the mathematicizing power of Homo Sapiens has been made and blinds us to the need of its continual verification.” (Footnote 8, Post 1936:291 in The Undecidable). Although Turing’s submission of his paper (received 28 May 1936) gave him a few months' priority over Post, Post's paper published first and Church had to certify that Post's work was independent of Turing's. Church and Paul Bernays refereed Turing's paper from spring 1936 through the fall; Bernays found errors in Turing's last proof and Turing had to modify it. But this gave Turing time to study Church's paper and add, in August 1936, an Appendix where he sketched a proof that Church's λ-calculus and his a-machines would compute the same functions.

Church would in turn defend himself against Post’s criticism by suggesting that “to define effectiveness as computability by an arbitrary machine subject to the restrictions of finiteness would seem to be an adequate representation of the ordinary notion, and if this is done the need for [Post’s] working hypothesis would disappear.” (cf Church 1937 in Gandy 1994:79).

"But what Church had done was something rather different, and in a certain sense weaker . . . the Turing construction was more direct, and provided an argument from first principles, closing the gap in Church's demonstration." (Hodges p. 112).

[edit] 1936-7 Turing’s Proof

Most of Turing's paper describes "effective calculability" in terms of "computable numbers are those whose decimals are calculable by finite means" (p. 117), in other words, his a-machines. He sets up an enumeration to be done by his universal machine U; it provides a “circle-deciding machine D” with numbers to test for “circularity”, starting with “1” and continuing in numerical sequence, (i.e. in modern terms, each number represents a programs to be tested for “unending loops”). He then proves, first, that his universal enumerator/circle-deciding program H = U+D cannot decide whether H (i.e. itself) will or will not end in "a circle" (a never-ending loop). (By assumption: it must never loop, but rather it must go on testing forever. But when it tests itself, its actions are to start with 1 and proceed, number by number, to test each one – by definition this is a circle and violates the premise.) By use of this result, Turing then proves that no universal deciding program E can tell if any machine M "ever prints a given symbol (0 say)." Armed with this second proof he goes on to prove that:

”The Hilbert Entscheidungsproblem can have no solution . . . there can be no general process for determining whether a given formula U of the functional calculus K is provable, i.e. that there can be no machine which, supplied with any one U of these formulae, will eventually say whether U is provable.” (U. p. 145)

Explanation of this proof is beyond the scope of this article. It involves Gödelizations of “complete configurations” of a-machines and subsequent attempts to match them to Gödelized “answers”, with failure as the ultimate outcome.

[edit] 1936-1965: Post’s "working hypothesis"

In his 1936 paper Post only proposed his "working hypothesis" of “a process” and criticized Church's "definition", but had proved nothing. rather, Post maintained a more philosophic stance. He hoped to publish a series of "wider and wider formulations . . . The success of the program would for us, change this hypothesis not so much to a definition or to an axiom but to a natural law" (Post 1936:291 in The Undecidable)

In later years Post remained skeptical of Church’s definition of effective calculability (Kleene’s “Thesis I” of 1943, named “Church’s Thesis” by Kleene in 1952) and Turing’s a-machines (named “Turing’s Thesis” by Kleene in 1952). In a paper Post submitted in 1941 and had rejected (subsequently published in 1965 by Davis in The Undecidable) he ponders the notion of, and the nature of, undecidability:

“1. The phrase “absolutely unsolvable” is due to Church . . . [but} this true only with respect to a given logic. A fundamental problem is the question of the existence of absolutely undecidable propositions, that is, propositions which in some a priori fashion can be said to have a determined truth-value [that is, either “true” or “false” but not both simultaneously], and yet cannot be proved or disproved in any valid logic" (Post in Davis 1965:340)

He seems to make a distinction between "number theory problems" of "Church" and what he called "combinatory mathematics" (cf Post 1965:338). Indeed, Post is emphatic about “the fundamental importance to mathematics of the existence of absolutely unsolvable combinatory problems . . . .“ He suggests that by use/adoption of “recursiveness” as a criterion of solvability, “the unsolvability in question as in the case of the famous problems of antiquity, becomes merely unsolvability by a given set of instruments. . . . The fundamental new thing is that for the combinatory problems the given set of instruments is in effect the only humanly possible set.” (Post 1965:340)


Post was seeking not just a “formulation which includes an equivalent for every possible ‘finite process’ but rather a “description that will cover every possible method for setting up finite processes”; he described this in his part “7. Generated sets of sequences” (Post 1965:402). He acknowledges that the “Turing simplifications” may work for “analysis of process” but doubts that they will work for “analysis of proof” (cf footnote 6:343) and he wonders if “Turing’s finite numbers of mental states hypothesis” will hold up under scrutiny and whether or not “an equally persuasive analysis be found for all humanly possible modes of symbolization” (footnote 9:344). Post hoped for a “reversal of the entire axiomatic trend of the late nineteenth and early twentieth centuries, with a return to meaning and truth. Postulational thinking will then remain as but one phase of mathematical thinking” (Post 1965:345).

[edit] 1965-present: Later developments

About Post’s “fundamental problem . . . the existence of absolutely undecidable propositions” mentioned above in Post’s footnote 1, Gandy remarks that:

”This was the problem he hoped one day to solve. It is a problem which most people today have stopped (alas?) thinking about.” (Gandy 1994:90)

[add something here about Gandy, Sieg, Moschovakis, Gurevich et. al. all trying to "characterize" (axiomatize) the generalized notion of "computation" by man or machine, and in all forms]

--- end ---

  • Robin Gandy 1994, “The Confluence of Ideas in 1936”, pages 51-102 in Rolf Herken (ed) 1994-1995, The Universal Turing Machine: A Half-Century Survey, Second Edition, Springer-Verlag/Wien New York, ISBN 3-211-82637-8.


Another major rewrite. wvbaileyWvbailey 18:18, 7 August 2007 (UTC)

There is something wrong with the section "The Entscheidungsproblem of 1928:". Mathematics is generally believed to be consistent, and although the proof systems for first order logic are complete, the axioms of mathematics are incomplete in a different sense. I have not looked at the sources to see how they present it, but as it is stated that para needs some help. — Carl (CBM · talk) 23:17, 6 August 2007 (UTC)
I agree. I had a bad time with the one sentence about Godel. Have I struck out the offender?
In 1930 Kurt Gödel answered the first two questions: YES the first order logic was complete (Gödel’s doctoral thesis proved his completeness theorem), but NO: the notion of primitive recursion (i.e. the arithmetic of Peano axioms and first order logic) was inconsistent (it could be used to “pose” a question about itself that could be answered in both the negative and the affirmative).
Tonight I found a good quote in Gandy 1994 that perhaps I will substitute after reading up a bit more on this. Thanks for your look-over. wvbaileyWvbailey 04:11, 7 August 2007 (UTC)
Yes, striking out that part is a large improvement. Here is the current version.

By the 1928 international congress of mathematicians, Hilbert "made his questions quite precise. First, was mathematics complete . . . Second, was mathematics consistent. Third . . . was mathematics decidable?" (Hodges p. 91, Hawking p. 1121). As mentioned above, in 1930-1 Kurt Gödel answered the first two questions: YES the first order logic was complete (Gödel’s doctoral thesis proved his completeness theorem), but NO: arithmetic’s consistency could not be answered within arithmetic (Peano Arithmetic) itself.

My concern is that the question "is mathematics complete" could mean "are the axioms we have chosen for mathematics strong enough to prove all mathematical truths?". This is a very different question than "is first order logic complete". It follows from both Godel's theorems and Tarski's undefinability-of-truth theorem that there is no effective (or even arithmetically definable) axiom system strong enough to completely capture the theory of the natural numbers. If you have Hodges' book, could you clarify what he means? Otherwise, I'll try to get to it, but I am busy this week. — Carl (CBM · talk) 17:58, 8 August 2007 (UTC)
I will study this very carefully (I've researched this a bit since your note and agree that what I wrote is misleading). I will propose new wording. Thanks, wvbaileyWvbailey 22:25, 8 August 2007 (UTC)
The following is the whole quote from Hodges. I've added some quotes from Godel 1931 and my interpretation of what is going on:
"By the 1928 international congress of mathematicians, Hilbert "made his questions quite precise. First, was mathematics complete in the technical sense that every statement . . . could be proved, or disproved. Second, was mathematics consistent, in the sense that the [false] statement ‘2 + 2 = 5’ could never be arrived at by a sequence of valid steps of proof. And thirdly, was mathematics decidable?" By this he meant, did there exist a definite method which could, in principle, be applied to any assertion, and which was guaranteed to produce a correct decision as to whether that assertion was true.” (Hodges 1983:91). In 1930-1 Kurt Gödel, by proof of his undecidability theorem IV and the consequences thereof, answered the first two questions NO. while it might be true that the first order logic might be complete (Gödel’s doctoral thesis proved his completeness theorem), With regards to “completeness”: Godel demonstrates that Peano arithmetic P is powerful enough to express, in P itself (he shows how to do this in footnote 360), the metamathematical statement “Arithmetic P is consistent". But as a consequence of his "undecidability Theorem" IV, “the SENTENCE which asserts that x [an arbitrary recursive consistent class] is consistent is not x-provable; in particular the consistency of P is unprovable in P, provided P is consistent (in the contrary of course, every statement is provable)”(Gödel’s theorem XI, Godel 1931:36 in The Undecidable). Thus in Peano arithmetic P there exists at least one statement that cannot be proven “consistent” or “inconsistent”; this fact makes P incomplete. But worse, just as the theorem states, the statement P is consistent cannot be proved within P itself. So in effect, Gödel got “two for one”.
I need to read up on this more, compare translations, etc. But this is a stab at it. wvbaileyWvbailey 03:05, 10 August 2007 (UTC)

[edit] Importance

I've changed the importance of this page from "low" to "mid". Actually, I think it rates a "high", but philosophers who are not mathematicians may think differently. The subject of the page is the impossibility of deciding every question that can be posed. Rick Norwood 19:39, 7 September 2007 (UTC)

I'm neither mathematican nor a philospher and I think it could be mid-to-high, at least from a (mathematics) foundational and historical perspective. In particular it has application to the philosophy of mind (that's the secret reason for my interest). Some writers fault the philosphers for not understanding the issues at gut-deep level but nevertheless concocting dubious pronouncements and arguments (e.g. not understanding quantum mechanics re philosophy of mind; also all the examples in Torkel Franzen 2005 Godel's Theorem: An Incomplete Guide to this Use and Abuse, A K Peters, Ltd. Wellesley MA). Another reason is: all three proofs of the 1930's that were so significant -- Church 1936, Turing 1936-7, Kleene 1943 -- all revolve the unsolvable "decision problem", and they all use similar techniques to arrive at their proofs (conversion of proofs to numbers, their subsequent enumeration (listing) and Cantor's diagonal argument). Godel 1931 (his theorem VI, the so-called first incompleteness theorem) is also a proof of undecidability and follows a similar tack. Is any of this of use to philosphers constructing arguments? I dunno, but I would hope so. wvbaileyWvbailey 21:52, 7 September 2007 (UTC)