On Aug 31, 4:55 am, Bruno Marchal <marc...@ulb.ac.be> wrote:
> 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.
Yes, ok, fair enough, they can formally FIND the Godel sentences, but
can't formally PROVE them, that's what I meant.
> 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.
Right, they can't formally prove them, and require an additional step
('instinctively believe')mathematical intuition (analogical reasoning)
to actualy believe in them.
> > 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.
Sorry, see above, I meant to say,
'the point of Penrose/Lucus is that you can only formally PROVE the
Godel senetence of a given systen from *outside* that system'
I accept that the 'machine can see the mystery', but not through any
ordinary reasoning methods. (you need analogical reasoning)
> 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.
OK, sorry, I should have said 'we cannot PROVE *our own* Godel
sentences fomally - getting to the 'higher order' levels needs
acccepting Godel sentences as an axiom, and this needs 'mathematical
intuition' at each step (analogies)
> 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 firstname.lastname@example.org
To unsubscribe from this group, send email to
For more options, visit this group at