On 30 Aug 2009, at 10:34, marc.geddes wrote:
>
>
>
> On Aug 30, 7:05 pm, Bruno Marchal <marc....domain.name.hidden> 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.domain.name.hidden
To unsubscribe from this group, send email to everything-list+unsubscribe.domain.name.hidden
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---
Received on Sun Aug 30 2009 - 18:55:01 PDT