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.


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 [EMAIL PROTECTED]
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at 
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---

Reply via email to