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