Re: ... cosmology? KNIGHT & KNAVE

From: Hal Finney <hal.domain.name.hidden>
Date: Thu, 29 Jul 2004 09:53:18 -0700 (PDT)

Tell me again where I am going wrong. Consider each of these examples:

117. q
...
191. Bp
...
207. p -> q

Now, we will say that the machines "believes" something if it is one of
its theorems, right? So we can say that the machine "believes q", it
"believes Bp", and it "believes p->q", right? We could equivalently say
it "believes q is true", etc., but that is redundant. If it writes x
down as a theorem, we will say it believes x, which is shorthand for
saying that it believes x is true. The "is true" part has no real
meaning and does not seem helpful.

We also have this shorthand Bx to mean "the machine believes x". So we
(not the machine, but us, you and I!) can also write, Bq, BBp and B(p->q),
and all of these are true statements, right?

The problem arises when we start to use this same letter B in the
machine's theorems. It is easy to slide back and forth between the
machine's B and our B. But there is no a priori reason to assume that
they are the same. That is something that has to be justified.

Focus on 207. p->q for a moment. We know that, according to the machine's
rules, this theorem means that if it ever writes down p as a theorem,
it will write down q. Therefore it is true that Bp->Bq. This is simply
another way of saying the same thing! Bp means that p is a theorem,
by definition of the letter B, in the real world. And similarly Bq
means that q is a theorem. Given that p->q is a theorem, then if p is
a theorem, so is q. Therefore it is true that B(p->q) -> (Bp -> Bq).
This is not a theorem of the machine, it is a truth in the real world.

What I want to say is that 207. p->q "means" Bp -> Bq. It means that if
the machine ever derives p, it will derive q. This is a true statement
about the operations of the machine. It is not a theorem of the machine.

When we talk about what something "means", I think it has to be what it
means to us, not what it means to the machine. When the machine writes
117.q, it doesn't mean anything to the machine. To us it means that the
machine believes q, or that the machine believes q is true.

Given this approach, I am very hesistant to say that 191. Bp means that
the machine believes that it believes p. I have no problem saying that it
means that the machine believes Bp. But to say that the machine "believes
that it believes p" uses the word "believes" in two very different and
confusing ways. The first "believes" is just a statement about what the
machine has derived as a theorem. We choose to say that the machine's
theorems are what it "believes". I am OK with that. But the second
"believes" refers to the letter B, which we are arbitrarily choosing to
identify with this word "belief".

To the machine, B is just a letter. I still say that I need to know what
the rules are that the machine will apply to that letter. I see that I
was wrong to think that p -> Bp was a rule the machine would have if it
were "normal". You said that for a normal machine, if it ever proved p,
it would also prove Bp. Okay, but how could it possibly do this without
ANY rules to deal with the letter B?

Normality is not something one can just assert about a machine. You would
need to give it a rule for dealing with the letter B, then you could prove
(not the machine proving, you would prove it) that if the machine ever
derived p, its rules for dealing with the letter B would then cause it
to derive Bp. In this way you would show that the machine was normal.

My axiom, which I should have written as, "0a. for all x, x->Bx", would
in fact be sufficient to show that a machine which had that axiom would
be normal. A machine which had this rule for dealing with the letter
B would be normal, because any time it derived p, it could immediately
derive Bp using this axiom.

However, this machine may be too powerful. Although it is normal, it
is much more.

So my question to you is, what is an example of an axiom for dealing
with the letter B that would make a machine be "just" normal, but no more?

Hal Finney
Received on Thu Jul 29 2004 - 13:40:02 PDT