From: Boudewijn Moonen Subject: Halting Problem and Goedel Incompleteness IV (was: Re: The halting Date: Tue, 29 Aug 2000 16:03:45 +0200 Newsgroups: sci.math To: davis_d@spcunb.spc.edu Summary: [missing] Unfortunately, that lousy netscape garbles mails, and, moreover, references to the literature were missing. So I repost this in a reformatted, completed version: "David K. Davis" wrote: > > Subject: The halting problem > Date: Mon, 31 Jul 2000 05:54:42 GMT > From: David K. Davis > Organization: St. Peter's College, US > Newsgroups: sci.math, sci.logic > > > Some programs applied to themselves as input halt. Others do not. Let P be > a program that when applied to programs whose self-application does not > halt, halts, and otherwise not. Does the application of P to itself halt? > > -Dave D. > Nice and to the point. Of course, P cannot exist, for its self-application would, by assumption, halt iff it would not halt. Turned the other way around, this says that "any program P that when applied to a program R halts implies (*) the self-application of R does not halt, does not halt on some program the self-application of which does nevertheless not halt". In other terms, every enumeration of programs-not-halting-upon-self-application is *incomplete* as there is at least one such program not being enumerated. In technical terms, the set NK of those programs is not recursively enumerable. Since the set of all (syntactically correct programs) is effectively enumerable (effectively enumerable = recursive = being enumerable in lexicographic order), it follows that the complement, the set K (name is historical) of programs- halting-upon-self-application, is a recursively enumerable set which is not effectively enumerable. Since the existence of a recursively enumerable set which is not effectively enumerable is known to be equivalent to Goedel's First Incompleteness Theorem, what your argument provides is not, at least not directly, a proof of the Unsolvability of the Halting Problem (UHP), but of the Goedel Incompleteness Theorem (GIT) in terms of computer programs (in fact, GIT is equivalent to UHP, I'll comment on this below). I'll present an outline of a direct argument in a moment. So for the time being let us call (*) "Goedel Incompleteness for Programs" (GIP). Some time ago I started three threads on this topic in sci.math, mainly asking for - Is there a form of GIT in terms of computer programs? - Is GIT equivalent to UHP? There were some interesting contributions, which did not settle these questions completely, but kept me thinking and searching, and since your post fits in nicely, I take the opportunity to comment on what I found out in the meantime and to ask some new questions in the course of this. A) The equivalence GIP <==> GIT =============================== In my former postings I used FPA as an abbreviation of Formal Peano Arithmetic, i.e. to designate any first order language needed to encode the Peano axioms; this is described in any reasonable book on Mathematical Logic (see e.g. [1]) or Computation Theory (see e.g. [2]). Formulas of FPA having no free occurrences of variables will be called *sentences*. I will use GIT to mean the following statement: (GIT) "There is a sentence G of FPA such that neither G nor its negation ~G is provable". The formulation of GIP above is just the version of Goedel's Incompleteness Theorem used by Roger Penrose in his "Shadows of the Mind" and has been certificated as clean by Solomon Feferman (http://psyche.cs.monash.edu.au/v2/psyche-2-07-feferman.html): "2.1 While Penrose's formulation of Gödel's theorem is by itself unexceptionable, ...[follows some polemics not of interest here] 2.2 Penrose's form of Gödel's incompleteness theorem is stated in terms of Turing machine computations as follows (pp. 74-75): Theorem 1: Suppose A is a Turing machine which is such that whenever A halts on an input (q,n) then C_q(n) does no halt. Then for some k, C_k(k) does not halt, yet A does not halt on (k,k). In other words, if the halting of A is a sufficient condition for the non-halting of Turing machines then it is not a necessary condition for that; still more briefly: soundness of A implies incompleteness of A." So why is this equivalent to GIT? The key point, which is responsible for the tight bonds bewteen Mathematical Logic and Computation Theory (and which makes Goedel's 1931 paper [3], in fact, the first substantial paper on that theory), is that computations correspond to logical deductions in the following manner. Let us introduce the following notations: If P is a program, and m, n are natural numbers, we write P : m --> n means P outputs n on input m P : m --> HALT means P halts on input m P : m --> INFTY means P does not halt on input m (here we switch freely between programs inputting numbers and programs inputting texts of programs by means of Goedel numbering). Then these properties are *expressible in FPA*. E.g. for the first property this means, there is a formula C(x,x',x'') having three free variables x, x', x'' such that P : m --> n iff C(g,m,n) is provable where g is the Goedel number of P. We simply write [P : x' --> x''] for this formula. Similarly for the other ones. (Of course, there is work to do here; this was one of Goedel's brilliant ideas). Another remark: GIP is concerned with a program which tests other programs on non-halting upon itself as input. This is equivalent to testing programs on non-halting on any given input, since any program with given input data can be rewritten as a program these input data are part of. Now to the equivalence of GIP with GIT. (i) How GIP implies GIT: ----------------------- Suppose GIP holds, but not GIT. Now, using the inference rules of FPA, one may write a program which systematically exploits all deductions from the peano axioms and so recursively enumerates all provable sentences of FPA. Call this program PA, the Peano Machine. Now write a program P as follows. On inputting a program Q, P runs PA and looks for the appearance of [Q : Q --> HALT] or ~[Q : Q --> HALT]. Then itdoes P : Q --> INFTY if Q : Q --> HALT , i.e. [Q : Q --> HALT] appears P : Q --> HALT if Q : Q --> INFTY , i.e. ~[Q : Q --> HALT] appears By assumption, one or the other happens in finite time. But then (+) P : Q --> HALT iff Q : Q --> INFTY contrary to GIP. (ii) How GIT implies GIP: ------------------------ Suppose GIT holds, but not GIP. Thus there is a program P with property (+). By the remark above, P may be thought of as testing programs on non-halting on given input data. We may assume that the FPA-language has only one quantifier, the "exists"-quantifier E. Any sentence S of FPA can be brought into an equivalent normal form (~)E x_1 ... (~)E x_k: F(x_1,...,x_k) where F(x_1,...,x_k) is a formula without bound variables. So we may assume S to be of this form. 1. S has no quantifiers. Then it encodes an arithmetical statement concerning finitely many concrete natural numbers, and one can write a program, E_0 say, deciding these statements. 2. Suppose S has exactly one quantifier. If it is of the form E x: F(x), write a program E_1, say, looping through the natural numbers n and testing F(n) with E_0 each time. At the same time, run P on E_1 whether to see it does not halt. Then either E_1 or P halts in finite time, thus proving S or ~S. 3. From this it is conceivable that one can write a program recursing on the quantifiers in a formula, which finally decides any given formula, contary to the assumption that GIT holds. (I owe this argument to Olaf Kummer, any imperfection in the too short presentation is due to me). B) A constructive Goedel formula ================================ Goedel proved a version of GIT being stronger insofar as he supplied in a constructive manner a specific sentence G such that neither G nor ~G was provable (under the somewhat stronger assumption of omega-consistency but let us disdain these technicalities here). Now in the proof of "GIP implies GIT" there was a - in principle constructive - description of a program P. Put G' := ~[P : P --> HALT]. Then neither [P : P --> HALT] nor ~[P : P --> HALT] can appear in the output of the Peano machine PA, since both results would lead to a contradiction to the prescribed behaviour of P. This therefore leads to the result that P does not halt on input P, yet neither this nor its negation is provable. QUESTION 1 (I am aware that it is imprecise, open to any nitpicking): How is G' related to Goedel's G? Is it just an analogon, or, when I translate programs into formulas, in some sense "really the same"? C) Relation to the Halting Problem and Goedel Triality ====================================================== "David K. Davis" wrote: > > In sci.math Joe wrote: > : On Mon, 31 Jul 2000 07:57:29 GMT, 11digitboy@my-deja.com wrote: > : >In article , > : > David K. Davis wrote: > : >> Some programs applied to themselves as input halt. Others do not. Let > : >P be > : >> a program that when applied to programs whose self-application does > : >not > : >> halt, halts, and otherwise not. Does the application of P to itself > : >halt? > : >> > : >> -Dave D. > : >> > : >> > : >------------------------- > : >This seems to me to be some kind of trick question. It appears that P > : >requires a program as input. If you have a program P (call it P-1) with > : >P (call THIS P-2) as input, what is the input of P-2?? Are you going to > : >try P-3, P-4, etc., and thus have an infinite regress?? > : > > : >Either that, or it's a little like determining the truth value of > : >Maláj's sentence: > : > > : > +------------------------------------------+ > : > | | > : > | Maláj's Sentence: | > : > | Maláj's Sentence is true. | > : > | | > : > +------------------------------------------+ > > : I think that your second objection is quite right. In fact, David's > : post more or less amounts to a proof that no such program P can > : exist. This looks to me like a weaker form of Turing's famous result > : that the halting problem is undecidable (David's program P would only > : decide that a program didn't halt, not that it did). > > : -- > : Joe. > > Suppose there were a program Q that could decide whether or not a > self-applied program halts. We could modify it: if it prints YES (meaning > it halts) then replace that code with a tight (endless) loop. Let this be > P. If P can't exist, then Q can't exist. > > -Dave D. > Again nice and to the point. What you prove here is that GIP implies UHP, hence by A), that GIT implies UHP. Conversely, UHP implies GIT. This, in essence, is in Turing`s 1937 paper [4] and has been reformulated by Chaitin ([5]) as follows: "Armed with the general definition of a formal axiomatic system ... in a formal language, one can immediately deduce a version of Goedel's incompleteness theorem from Turing's theorem... The reason is simply that if it were always possible to prove whether or not particular programs halt, since the set of theorems is r.e., one could use this to solve the halting problem for any particular program by enumerating all theorems until the matter is settled. But this contradicts the unsolvability of the halting problem. In fact, one has the following set of equivalences, which I would like to call for the moment "Goedel Triality": THEOREM (Goedel Triality) The following three properties are euivalent: (i) (RNE) There exists a set which is recursively, but not effectively, enumerable; (ii) (UHP) The halting problem is unsolvable; (iii) (GIT) There exists a sentence G in FPA such that neither G nor ~G is provable in FPA. SKETCH OF PROOF RNE implies UHP: Let K be a set that is recursively, but not effectively, enumerable. Let pi_K be the partial characteristic function of K: pi_K(x) = 1 if x in K pi_K(x) undefined else . Then the program which computes pi_K has an unsolvable halting problem. UHP implies GIT: That is the Turing-Chaitin argument just cited. GIT implies RNE: The set of provable sentences of FPA is recursively, butnot effectively, enumerable. QED What is nice is that it (apparently) cuts nicely diagonally through three different notions of computability: RNE applies to recursion theory - "Goedel computability" = computable via recursive functions UHP applies to computing machines - "Turing computability" = computable via Turing machines or other computers GIT applies to logic calculi - "Hilbert computability" = computable via a logic derivation in a sequent calculus (hypothetical) Goedel Triality can also be formulated in terms of one of these computability notions, e.g. in terms of Turing computability: THEOREM (Goedel Triality for Programs, GTP) The following three properties are euivalent: (i) (RNE) The set of programs terminating on their own input is recursively, but not effectively, enumerable; (ii) (UHP) The halting problem is unsolvable; (iii) (GIT) Suppose A is a Turing machine which is such that whenever A halts on an input (q,n) then C_q(n) does not halt. Then for some k, C_k(k) does not halt, yet A does not halt on (k,k). Or for Hilbert computability: THEOREM (Goedel Triality for Logic, GTL) The following three properties are euivalent: (i) (RNE) The set of provable sentences of FPA is recursively, but not effectively, enumerable (ii) (UHP) Hilbert's Entscheidungsproblem is unsolvable; (iii) (GIT) There exists a sentence G in FPA such that neither G nor ~G is provable in FPA. This is unsatisfactory in several aspects; I therefore have the following (informal) questions: QUESTION 2: What is the right notion of "Hilbert computability? How does it relate to other known notions of computability? QUESTION 3: GTL is unsatisfying as (i) it still refers to Goedel computability (notion of "recursively enumerable") and in (ii) to Turing computability (notion of "decision procedure" hidden in Hilbert's Entscheidungsproblem). Are there formulations fully in terms of logic and deduction rules? Related to this is QUESTION 4: In both formulations of triality the equivalences (i) - (iii) are easily proved. In addition to this, however, all three assertions (i), (ii), and (iii) in GTP, in particular UHP is apparently easily proved, wheres any of the three assertions (i), (ii), and (iii) in GTP on its own is hard to prove (Goedel's proof is usually considered to be hard, in particular in comparison with the one-line proofs of GIP or UHP above). Why is this so? Wouldn't, with a suitable notion of Hilbert computability, Goedel's proof become as easy as the proof of UHP? D) Relations with self-writing programs ======================================= > > Subject: An unprogrammable task > Date: Mon, 31 Jul 2000 04:37:28 GMT > From: David K. Davis > Organization: St. Peter's College, US > Newsgroups: sci.math, sci.logic > > > > > Programs can write programs. A program might or might not write itself. > Can there be a program that writes all and only those programs that don't > write themselves? Clearly not. It can neither write nor not write itself. > > -Dave D. > Nice, but how to the point I do not know. This shows that the set of self-writing programs is recursively, but not effectively, enumerable, and so the conclusion implies UHP and GIT. QUESTION 5: Is this, in fact, equivalent to UHP or GIT? Regards -- Boudewijn Moonen Institut fuer Photogrammetrie der Universitaet Bonn Nussallee 15 D-53115 Bonn GERMANY e-mail: Boudewijn.Moonen@ipb.uni-bonn.de Tel.: GERMANY +49-228-732910 Fax.: GERMANY +49-228-732712 REFERENCES ========== [1] H.D. EBBINGHAUS, J: FLUM, W. THOMAS: Mathematical Logic. Springer UTM 1984 [2] Nigel CUTLAND: Computability. Cambridge University Press, 1980. [3] KURT GOEDEL: Undecidable Propositions of the Principia Mathematica and Related Systems, I. Reprinted in [6], pp. 4-39 [4] ALAN M. TURING: On Computable Numbers with an Application to the Entscheidungsproblem. Reprinted in [3], pp. 116-154 [5] GREGORY CHAITIN: Goedel's theorem & information. Available on the web as http://www.cs.umaine.edu/~chaitin/georgia.html [6] MARTIN DAVIS (ed.): The Undecidable. Raven Press, New York 1965