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).


> 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).



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 
For more options, visit this group at 

Reply via email to