Hal,

I didn't see the whole post. So here is a sequel.

At 11:01 28/07/04 -0700, Hal Finney wrote:

`BM:`

> You are right. It is powerful, but rather fair also. > let us define a machine to be stable if that is the case. When the > machine believes Bx the machine believes x.

HAL: So in my terms, I can add two axioms:

0a. x implies Bx 0b. Bx implies x

The first is the axiom of normality, and the second is the axiom of stability.

No, I stop you right here. You redo the error. No problem, I still do it 1 or 2 times a day. And, would have I not made it persistently in my youth, I would be much farther. You must be very careful reading a proposition in english, and then translating in the machine language.

Your axiom 0a says that the truth of x implies the truth of Bx. It is really the usual implication:

x implies Bx 1 1 1 1 0 0 0 1 1 0 1 0

Would it be true. Then would x be true, Bx would be true too. "x implies Bx" means either x is false or Bx is true. It really means that the machine is truth complete, that is omniscient, that is ... the contrary of the consequence of Godel theorem. It is also the reason why i use generally "->" instead of "implies". Ah, perhaps that is the root of the confusion.

Same remark for your axiom 0b. Bx implies x, or better, Bx -> x, means that the machine is accurate. It is built in such a way that if Bx is true (that is if the machine believe x, then x is true).

We can sum up: 0a = the machine believes all the truth. 0b = the machine believes only the truth.

(And so new exercise: what happens with complete and /or accurate machine of type 1 when they meet the Knight saying the usual proposition?)

Normality and stability are much weaker notion: A machine is normal means: if the machine ever believe p then sooner or later the machine will believe Bp. Now, please, just translate *carefully* this in the language of the machine. Let us do it by stage: the machine believe p is Bp the machine believe Bp is BBp if the machine believes p then the machine believes Bp becomes Bp implies BBp, or perhaps better: Bp -> BBp

The same for stability, it will gives BBp -> Bp.

Summing up:

Stability is: BBp -> Bp Normality is: Bp -> BBp

I don't find these words to be particularly appropriate, by the way, but I suppose they are traditional.

More or less traditionnal. Normality is very traditionnal, although in slightly strict or broader sense. Stability is less tarditionnal, but Smullyan uses that term. Anyway, it is not logically relevant ...

It also seems to me that these axioms, which define the behavior of the letter B, don't particularly well represent the concept of belief. The problem is that beliefs can be uncertain and don't follow the law of the excluded middle. If p is that there is life on Mars, then (p or ~p) is true. Either there's life there or there isn't. But it's not true that (Bp or B~p).

Be reassured. Our reasoner believes in the excluded middle:

that is they believe in (x v -x). In machine Lang.: B(x v -x), but this will not imply (Bp or B~p)

Unless your axiom 0a is true, but that will be impossible, by Godel. No machine can be complete (except inconsistent one).

I will read the rest at ease, but I think it follows from your axioms 0a, and 0b, but 0a does not apply for any reasoner who believes in arithmetic ... The rest of your post is correct deduction, but with wrong premise.

When you said:

Suppose for some proposition q the machine deduces it on step 117:

117. q

Does this mean that q is true? No, it means that that the machine believes q.

Yes but the machine believes q is true, or assert q is true. The machine is not asserting it believes true.

Does it mean that Bq is true? Yes. Bq is true, because Bq is a shorthand for saying that the machine believes q, and by definition the machine believes something when it writes it down in its numbered list. We can see it right there, number 117. So the machine believes q and Bq is true. But q is not (necessarily) true. The machine writing something down does not "mean" it is true. By definition, it means the machine believes it.

Consider a different example:

191. Bp

What does this mean? Does it mean that Bp is true? No, it means that the machine believes Bp, because by definition, what the machine writes down in its numbered list is what it believes. Is BBp true? Yes, it is true, because that says that the machine believes Bp, and that means that Bp is in the machine's numbered list, which it is, right there. The machine believes Bp, but Bp is not (necessarily) true. BBp is necessarily true.

Another example

207. p implies q

By the same reasoning, this does not mean that if p is true, then q is true. It means that if the machine ever believes p (i.e. it writes it down in its list of theorems), then it will believe q (i.e. it will eventually write down q in its list of theorems). The true statment is that Bp implies Bq. You can also (trivially) conclude B(p implies q). But "p implies q" is not (necessarily) true.

Here you are incorrect again, ok, I diagnose that it is the "implies" you have a problem of translation. If at stage 207 the machine print "p implies q" it means the machine believes (p->q), that is: that if p is true then q is true. The machine does not mention any explicit believe in the sentence.

Actually we never said that the machine believes something like B(p implies q) implies (Bp implies Bq), which is what you say. You are anticipating on the type 2 reasoner.

Now we are ready for:

>8. t implies Bt

It is not mean that "t implies Bt" is true, any more than "207. p implies q" was true. What it means is that if the machine ever believes t, it will believe Bt. Given that t means the native is a knight, it means that, as I wrote before, "if I ever deduce he is a knight, I believe it", where I am the machine. The true meaning is that Bt implies BBt.

So I don't see why you said that this was wrong, and that

> Here you are mistaken. It is funny because you clearly see > the mistake, given that you say 'attention (t implies Bt) does > not mean "if he is a knight the I believe it". But of course (t implies Bt) > *does* mean "if he is a knight the I believe it".

While it is true that, by itself, (t implies Bt) does mean "if he is a knight then I believe it", in the context of the machine, "8. t implies Bt" doesn't mean that. It means that the machine believes the implication, not that the implication is true.

Yes, but that's equivalent to B(p->q), meaning that for the machine p->q has been proved. The machine is close for the modus ponens, but is (not yet) supposed to know that.

> You add it means only > (and here I add a slight correction) "if I ever deduce he is a knight I > will deduce I believe he is a knight" which really is, in the machine > language: (Bt implies BBt) instead of (t implies Bt).

Right, or as in my simpler example, when I wrote "207. p implies q" that truly means Bp implies Bq.

Not at all: it "means" B(p implies q).

> To be sure: a machine is normal if for any proposition p, if the machine > believes p, it will believe Bp. But this is equivalent with saying > that for any proposition p, the proposition (Bp implies BBp) is true > *about* the machine. > Same remark for stability: you can say a machine is stable > if all the propositions (BBp implies Bp) are true about the machine. > This does not mean the stable or normal machine will ever believe > being stable or normal. You have (momentarily) confuse a proposition > being true on a machine, and being believe by a machine.

I agree with everything here except the last sentence. I don't see what I have confused, or what is wrong with my derivation. If you assume both 0a. and 0b., meaning that I am both normal and stable, then the proof is correct, right? If not, which step fails?

Oa means complete, and 0b means accurate. Stable is (BBp -> Bp) and normal is (Bp -> BBp)

Hal, I think the confusion comes from the use of "imply" instead of "->". Sorry if I have not been clear. If you (or anyone else) has still a problem, please ask. If possible by short post. We will have plenty of occasion to be familiarized with that matter.

Bruno

http://iridia.ulb.ac.be/~marchal/