On 03 Dec 2012, at 21:55, meekerdb wrote:
On 12/3/2012 10:03 AM, Bruno Marchal wrote:
On 03 Dec 2012, at 00:04, meekerdb wrote:
On 12/2/2012 7:27 AM, Bruno Marchal wrote:
The 1p truth of the machine is not coded in the machine. Some
actual machines knows already that, and can justified that If
there are machine (and from outside we can know this to correct)
then the 1p-truth is not codable. The 1p truth are more related
to the relation between belief and reality (not necessarily
physical reality, except for observation and sensation).
Even the simple, and apparently formal Bp & p is NOT codable.
Most truth about machine, including some that they can know, are
not codable.
Many things true about us is not codable either.
Let me see if I understand that. I think you are saying that p,
i.e. that "p" describes a fact about the world, a meta-level above
the coding of a machine.
No, p is for some statement at the base level, like 1+1 = 2.
Yes, I understand that. I didn't express myself clearly. p is a 0-
level statement. "That p" (i.e. that p is true, that "p"
describes a fact) is a 1-level statement.
p is "that p". When the machine asserts 1+1=2, she meant that it is
the case that "1+1=2", independently of the truth or falsity of the
assertion. But we mimit ourself to correct machine, so in this case
"p" and "p is true" are equivalent, and so we can model True("p"),
which is not expressible in the language of the machine, by
"p" (asserted by the machine).
That the Mars Rover believes it is south of it's landing point is
implicit in its state and might be inferred from its behavior, but
there is no part of the state corresponding to "I *believe* I am
south of my landing point."
Then Mars Rover is not Löbian. But I am not even sure that Mars
Rover is Turing universal, or that it exploits its Turing
universality.
Well not the current Mars Rover, but a Mars Rover could be, it's
just a matter of program. So the Rover could not only encode p,
also encode that it believed p.
OK.
But PA and ZF can represent "I believe". So we can study the logic
of a new 'knowledge" operator defined (at the meta level, for each
arithmetical proposition) by Bp & p. For example if p is "1+1=2",
it is
Believe"("1+1=2") & 1+1 = 2.
I don't understand the significance of the unpaired quote marks?
read:
Believe("1+1=2") & 1+1 = 2
(Sorry).
We cannot define such operator in arithmetic. We would need
something like Believe"("1+1=2") & True("1+1 = 2"), but True, in
general cannot defined in arithmetic. Yet, we can metadefine it and
study its logic, which obeys a soprt of temporal intuionistic logic
(interpreting the S4Grz logic obtained).
One could include such second-level states (which one might want
to communicate to Pasadena) but then that state would be just
another first-level state. Right?
Not sure I see what you mean. The meta, available by the machine is
in the "I believe". It is the 3-I. The presentation of myself to
myself. The 1-I will be the non definable operator above. We
connect the believer to the truth. It is easy to do for the sound
correct machine.
What I mean is that if you programmed the Rover to be Lobian and it
not only thought p but also though Bp, both of those would be just
be similar physical states within its computer memory - their
hierarchical relation would just be that encoded in the Lobian
program.
?
"s(0) + s(0) = s(s(0))" is far more shorter than the coding of
"Beweisbar ("s(0) + s(0) = s(s(0))")"
So a physical error in the computer could change Bp to ~Bp, yet this
would have no effect on the performance of the Rover except in
reporting what it believed.
To survive, such self-referential falsity will not help.
To do "philosophy of mind", such false reports can be disastrous.
But for the correct machine, by definition we don't have that problem.
Bp & p is strictly equivalent with Bp. Now the correct machine can
never prove ("for all p") such an equivalence. In fact by Löb theorem,
if ever the machine proves Bp -> p, she will always been able to prove
p.
G* proves ((Bp & p) <-> Bp)
G does not prove that. Indeed the machine can't prove Bf -> f.
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.
