Le 06-juil.-07, à 19:43, Brent Meeker a écrit :
> > Bruno Marchal wrote: > ... >> Now all (sufficiently rich) theories/machine can prove their own >> Godel's theorem. PA can prove that if PA is consistent then PA cannot >> prove its consitency. A somehow weak (compared to ZF) theory like PA >> can even prove the corresponding theorem for the richer ZF: PA can >> prove that if ZF is consistent then ZF can prove its own consistency. > > Of course you meant "..then ZF cannot prove its own consistency." Yes. (Sorry). > >> So, in general a machine can find its own godelian sentences, and can >> even infer their truth in some abductive way from very minimal >> inference inductive abilities, or from assumptions. >> >> No sound (or just consistent) machine can ever prove its own godelian >> sentences, in particular no machine can prove its own consistency, but >> then machine can bet on them or "know" them serendipitously). This is >> comparable with consciousness. Indeed it is easy to manufacture >> thought >> experiements illustrating that no conscious being can prove it is >> conscious, except that "consciousness" is more truth related, so that >> machine cannot even define their own consciousness (by Tarski >> undefinability of truth theorem). > > But this is within an axiomatic system - whose reliability already > depends on knowing the truth of the axioms. ISTM that concepts of > consciousness, knowledge, and truth that are relative to formal > axiomatic systems are already to weak to provide fundamental > explanations. With UDA (Universal Dovetailer Argument) I ask you to implicate yourself in a "thought experiment". Obviously I bet, hope, pray, that you will reason reasonably and soundly. With the AUDA (the Arithmetical version of UDA, or Plotinus now) I ask the Universal Machine to implicate herself in a formal reasoning. As a mathematician, I limit myself to sound (and thus self-referentially correct) machine, for the same reason I pray you are sound. Such a restriction is provably non constructive: there is no algorithm to decide if a machine is sound or not ... But note that the comp assumption and even just the coherence of Church thesis relies on non constructive assumptions at the start. Bruno http://iridia.ulb.ac.be/~marchal/ --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "Everything List" group. To post to this group, send email to [EMAIL PROTECTED] To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/everything-list?hl=en -~----------~----~----~----~------~----~------~--~---
