From owner-cse584-sp07-list@LISTSERV.BUFFALO.EDU Sun Feb 25 19:23:08 2007 Received: from ares.cse.buffalo.edu (ares.cse.Buffalo.EDU [128.205.32.79]) by castor.cse.Buffalo.EDU (8.13.6/8.12.10) with ESMTP id l1Q0N7WJ019726 for ; Sun, 25 Feb 2007 19:23:07 -0500 (EST) Received: from front3.acsu.buffalo.edu (upfront.acsu.buffalo.edu [128.205.4.140]) by ares.cse.buffalo.edu (8.13.6/8.13.6) with SMTP id l1Q0N3ZZ056313 for ; Sun, 25 Feb 2007 19:23:03 -0500 (EST) Received: (qmail 16193 invoked from network); 26 Feb 2007 00:23:03 -0000 Received: from mailscan1.acsu.buffalo.edu (128.205.6.133) by front3.acsu.buffalo.edu with SMTP; 26 Feb 2007 00:23:03 -0000 Received: (qmail 11601 invoked from network); 26 Feb 2007 00:23:03 -0000 Received: from deliverance.acsu.buffalo.edu (128.205.7.57) by front2.acsu.buffalo.edu with SMTP; 26 Feb 2007 00:23:03 -0000 Received: (qmail 8812 invoked from network); 26 Feb 2007 00:22:56 -0000 Received: from listserv.buffalo.edu (128.205.7.35) by deliverance.acsu.buffalo.edu with SMTP; 26 Feb 2007 00:22:56 -0000 Received: by LISTSERV.BUFFALO.EDU (LISTSERV-TCP/IP release 14.5) with spool id 3550629 for CSE584-SP07-LIST@LISTSERV.BUFFALO.EDU; Sun, 25 Feb 2007 19:22:56 -0500 Delivered-To: cse584-sp07-list@listserv.buffalo.edu Received: (qmail 12655 invoked from network); 26 Feb 2007 00:22:56 -0000 Received: from mailscan8.acsu.buffalo.edu (128.205.7.55) by listserv.buffalo.edu with SMTP; 26 Feb 2007 00:22:56 -0000 Received: (qmail 10685 invoked from network); 26 Feb 2007 00:22:55 -0000 Received: from castor.cse.buffalo.edu (128.205.32.14) by smtp3.acsu.buffalo.edu with SMTP; 26 Feb 2007 00:22:55 -0000 Received: from castor.cse.Buffalo.EDU (rapaport@localhost [127.0.0.1]) by castor.cse.Buffalo.EDU (8.13.6/8.12.10) with ESMTP id l1Q0Mt5g019716 for ; Sun, 25 Feb 2007 19:22:55 -0500 (EST) Received: (from rapaport@localhost) by castor.cse.Buffalo.EDU (8.13.6/8.12.9/Submit) id l1Q0MtnW019715 for cse584-sp07-list@listserv.buffalo.edu; Sun, 25 Feb 2007 19:22:55 -0500 (EST) X-UB-Relay: (castor.cse.buffalo.edu) X-PM-EL-Spam-Prob: : 7% Message-ID: <200702260022.l1Q0MtnW019715@castor.cse.Buffalo.EDU> Date: Sun, 25 Feb 2007 19:22:55 -0500 Reply-To: "William J. Rapaport" Sender: "Philosophy of Computer Science, Spring 2007" From: "William J. Rapaport" Subject: HALTING PROBLEM To: CSE584-SP07-LIST@LISTSERV.BUFFALO.EDU Precedence: list List-Help: , List-Unsubscribe: List-Subscribe: List-Owner: List-Archive: X-UB-Relay: (castor.cse.buffalo.edu) X-DCC-Buffalo.EDU-Metrics: castor.cse.Buffalo.EDU 1335; Body=0 Fuz1=0 Fuz2=0 X-Spam-Status: No, score=-2.0 required=5.0 tests=AWL,BAYES_00,SUBJ_ALL_CAPS autolearn=no version=3.1.7 X-Spam-Checker-Version: SpamAssassin 3.1.7 (2006-10-05) on ares.cse.buffalo.edu X-Virus-Scanned: ClamAV 0.88.6/2653/Sun Feb 25 16:24:16 2007 on ares.cse.buffalo.edu X-Virus-Status: Clean Status: R Content-Length: 1838 ------------------------------------------------------------------------ Subject: HALTING PROBLEM ------------------------------------------------------------------------ A student writes: | | Would it be possible to write a program for a TM that would allow the TM | to "recognize" (or compute?) that the halting problem is undecidable? There are several things you might mean: 1. Would it be possible to write a program for a TM that would prove that HP is undecidable? If a human writes it and encodes it in a TM program, then yes. 2. Would it be possible to write a program for a TM that would enable that TM to create such a proof? In principle, possibly. (How's that for a hedged answer? :-) There are many research projects on automated theorem proving, whose goals are to write TM programs that will prove theorems. Some have succeeded, with human help, in replicating the proofs of previously proved theorems, sometimes with different proofs (Newell & Simon did this for some elementary theorems of logic; it was the first AI program). Others have succeeded, with human help, in proving hitherto unproved theorems (e.g., the 4-color problem--that 4 colors suffice to color any map so that no two adjacent countries have the same color)--was proved this way). Still others have succeeded in proving hitherto unproved theorems without human help. But I don't know the status of the HP with respect to this. Sounds like an interesting term paper topic :-) 3. Would it be possible to write a program for a TM that would allow the TM to "understand" the proof that HP is undecidable? This is in part an empirical question and in part a matter of what one means by "understand". I think it can be done, and Albert is writing his dissertation on a closely related topic. I'll let him elaborate.