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.



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 

Reply via email to