Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!zaphod.mps.ohio-state.edu!rpi!batcomputer!cornell!oravax!ian From: ian@oravax.UUCP (Ian Sutherland) Newsgroups: comp.theory Subject: Re: Question on halting problem Keywords: for 10 bonus points... Message-ID: <2283@oravax.UUCP> Date: 29 Apr 91 04:39:38 GMT References: <1991Apr26.135918.8607@m.cs.uiuc.edu> <1161@creatures.cs.vt.edu> Reply-To: ian@cambridge.oracorp.com (Ian Sutherland) Organization: ORA Corporation, Cambridge, MA Lines: 9 If what we're after is programs whose halting is difficult to prove, how about a program that searchs for a proof of "A & ~A" from the axioms of ZFC? If it doesn't halt, we can't prove in ZFC that it doesn't. We have reason to believe, however, that any obvious proof that this program halts would have been found a while back. -- Ian Sutherland ian@cambridge.oracorp.com Sans peur