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 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 Sat Jul 07 2007 - 07:17:41 PDT