On 30 Aug 2009, at 10:34, marc.geddes wrote:

> > > > On Aug 30, 7:05 pm, Bruno Marchal <marc...@ulb.ac.be> wrote: >> >> This does not make sense. > > You said; > >> The truth of Gödel sentences are formally trivial. >> The process of finding out its own Gödel sentence is > mechanical. >> The diagonilization is constructive. Gödel's > proof is constructive. That is what Penrose and Lucas are missing > (notably). > > This contradicts Godel. The truth of any particular Godel sentence > cannot be formally determined from within the given particular formal > system - surely that's what Godel says? Not at all. Most theories can formally determined their Gödel sentences, and even bet on them. They can use them to transform themselves into more powerful, with respect to probability, machines, inheriting new Gödel sentences, and they can iterate this in the constructive transfinite. A very nice book is the "inexhaustibility" by Torkel Franzen. Machine can determined their Gödel sentences. They cannot prove them, but proving is not the only way to know the truth of a proposition. The fact that G* is decidable shows that a very big set of unprovable but true sentences can be find by the self-infering machine. The machine can prove that if those sentences are true, she cannot prove them, and she can know, every day, that they don't have a proof of them. They can instinctively believe in some of them, and they can be aware of some necessity of believing in some other lately. > > The points are addressed in ‘Shadows of The Mind’ (Section 2.6, > Q6). Hmm... > > The point of Penrose/Lucs is that you can only formally determine the > Godel sentence of a given system from *outside* that system. The cute thing is that you can find them by inside. You just can prove them, unless you take them as new axiom, but then you are another machine and get some new Godel sentences. Machines can infer that some arithmetical sentences are "interesting question only". The machine can see the mystery, when she looks deep enough herself. I would say it is very well known, by all logicians, that Penrose and Lucas reasoning are non valid. A good recent book is Torkel Franzen "Use and abuse of Gödel's theorem". Another "classic" is Judson Webb's book. Ten years before Gödel (and thus 16 years before Church, Turing, ...) Emil Post has dicovered Church thesis, its consequences in term of absolutely insoluble problem and relatively undecidable sentences, and the Gödelian argument against mechanism, and the main error in those type of argument. Judson Webb has seen the double razor edge feature of such argument. If you make them rigorous, they flash back and you help the machines to make their points. > We > cannot determine *our own* Godel sentences formally, We can, and this at each level of substitution we would choose. But higher third person level exists also (higher than the substitution level) and are close to philosophical paradoxes. AUDA comes from the fact that ,not only machine can determined and study their Gödel sentences, but they can study how those sentences determined different geometries according to the points of view which is taken (cf the eight arithmetical hypostases in AUDA). 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 everything-list@googlegroups.com To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/everything-list?hl=en -~----------~----~----~----~------~----~------~--~---