From kragen@dnaco.net Sat Aug 29 22:39:12 1998 Date: Sat, 29 Aug 1998 22:39:10 -0400 (EDT) From: Kragen To: clug-user@clug.org Subject: computability and decidability Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Keywords: X-UID: 1579 Status: O X-Status: On the relationship between undecidable propositions and uncomputable functions, which we discussed very fuzzily at dinner: An undecidable proposition in a formal system is a proposition for which neither proof nor disproof exists inside that formal system. (This requires that the formal system have some way of stating a contradiction -- let's denote the contradiction of proposition X with the notation NOT(X) -- and that both X and NOT(X) are never both provable inside the formal system for any X.) An uncomputable function is a function it is impossible to give an algorithm to compute. Because the cardinality of the set of functions is aleph-one and the cardinality of the set of algorithms is aleph-null, there are as many uncomputable functions as there are real numbers. One particular set of functions has to do with provability. For any formal system of axioms and reasoning rules, such as the predicate calculus, there's a function PROVABLE(S) which maps strings S of that formal system's alphabet to the values "true" and "false", according to whether or not S is a theorem of that formal system. If a particular formal system contains undecidable propositions, I believe that means that its PROVABLE function is uncomputable. If a particular formal system contains no undecidable propositions, it definitely means that its PROVABLE function is computable. Since the set of theorems of the formal system can be enumerated, all you have to do is enumerate theorems until you find either S or NOT(S). I don't know if all uncomputable functions can be expressed as the PROVABLE function for some consistent formal system. The ones I know of are. Kragen -- Kragen Sitaker We are forming cells within a global brain and we are excited that we might start to think collectively. What becomes of us still hangs crucially on how we think individually. -- Tim Berners-Lee, inventor of the Web