Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP Posting-Version: version B 2.10.3 alpha 4/15/85; site kestrel.ARPA Path: utzoo!watmath!clyde!burl!ulysses!bellcore!decvax!decwrl!glacier!kestrel!ttp From: ttp@kestrel.ARPA Newsgroups: net.ai,net.philosophy Subject: Re: A halting problem: a meaty response Message-ID: <4395@kestrel.ARPA> Date: Thu, 30-Jan-86 03:40:13 EST Article-I.D.: kestrel.4395 Posted: Thu Jan 30 03:40:13 1986 Date-Received: Sat, 1-Feb-86 04:25:23 EST References: <2175@aecom.UUCP> <14551@rochester.UUCP> <3978@kestrel.ARPA> <4374@kestrel.ARPA> Distribution: net Organization: Kestrel Institute, Palo Alto, CA Lines: 82 Xref: watmath net.ai:3240 net.philosophy:4011 Summary: a summary, the world, oracles, induction ... (somewhat long) In article <4374@kestrel.ARPA>, ladkin@kestrel.ARPA (Peter Ladkin) writes: > There are theorems such as Kruskal's, the Paris-Harrington > version of the Ramsey Theorem, and Friedman's various principles > that are provable stronger than the generally acceptable > principles of arithmetic, and recursive set theory. They are > arguably consistent, since there are `proofs' of them. > These proofs must depend upon stronger principles than all > mathematicians are willing to accept (e.g. intuitionists). > If you believe these proofs, you will nevertheless be > unable to persuade those who are sceptical of their validity, > and furthermore, there is a proof of this fact. Summary as I understand it so far: I first asked whether, assuming that the human race had the computational power of a Turing machine, that it followed that there was some PARTICULAR problem (e.g. a halting problem) that could be EXHIBITED that could never be "decided" by the human race, that is, no one would ever come along with a proof that the particular machine would or would not halt. Matt Wiener and Peter Ladkin have contributed various mathematical problems such as: initialize generator of consequences from the Peano axioms; (loop c := the "next" consequence of Peano axioms if c is equal to `false' then exit else continue) This program halts if the Peano axioms are inconsistent, otherwise loops forever. If this program ever halts, we'll know the axioms are inconsistent (you with Cray's out there, take note -:). But how could we justify to ourselves that this program doesn't halt? Most people assume the Peano axioms are consistent; this cannot however be proved within the Peano axioms -- and known "proofs", e.g.Gentzen's proof requires that one appeal to "higher" principles (transfinite induction up to some large set) that not all mathematicians accept. And even if you're not as radical as the intuitionists, and accept these proofs, Matt produced other problems that are even more difficult to intuit. So my first idea that there come to be cleverer people over the years who think up new ways to combine existing FACTS and will eventually be able solve everything is wrong. The kind of insight that such people have is not a consequence of deduction from existing facts, but rather to intuit new PRINCIPLES which at least some schools of mathematical thought will gradually accept. And Peter has pointed out that if such a principle proves the goal statement you'd like to show, then it is stronger than the goal, so such a proof only really assumes something stronger than the original goal to be proved. The thing I NOW wonder about is from where these principles arise. I expect the philosophers will now enter the fray if they are not too appalled by my naivete, perhaps waving appropriate references ("the philosophy section of the library" -:). Assume people have computational power reducible to Turing machines (ignore finite/infinite memory). People are, however, situated in the world, and this may be able to give (some of) them (somehow) glimpses of infinity. Where did the Peano axioms come from in the first place? Perhaps the world somehow interacts with (some) people so as to be a sort of oracle, where certain undecidable-from-a-formal-theory consequences become known as intuitively obvious (e.g. the joke about the Peano axioms are consistent because obviously the natural numbers are a model). Also it is known that some great (and not so) mathematicians intuit truth without at first being able to construct any formal proof. This could of course mean that they're simply working in some better formal system than whatever "formal proof" means. Or it could mean they see something that would have been impossible to jump too unless they had interacted with the world. The world, one expects, is a model of truth. We've evolved evolutionarily to embody an understanding of certain principles (Hume?). Perhaps armed with world experience and some INDUCTION axioms (I'm thinking of Doug Lenat's EURISKO work here), people can concoct higher and higher truths. Or it could be that we're stuck at some large cardinality set, and as Matt implied, we'll have to wait for the answers from some other race with a "higher" intuition. -tom Note: "experience with the world", I assume, is finite, so induction is necessary to generate any infinite consequences.