I am confused about how "belief" works in this logical reasoner of type 1.
Suppose I am such a reasoner. I can be thought of as a theorem-proving
machine who uses logic to draw conclusions from premises. We can imagine
there is a numbered list of everything I believe and have concluded.
It starts with my premises and then I add to it with my conclusions.

##
Advertising

In this case my premises might be:
1. Knights always tell the truth
2. Knaves always lie
3. Every native is either a knight or a knave
4. A native said, "you will never believe I am a knight".
Now we can start drawing conclusions. Let t be the proposition that
the native is a knight (and hence tells the truth). Then 3 implies:
5. t or ~t
Point 4 leads to two conclusions:
6. t implies ~Bt
7. ~t implies Bt
Here I use ~ for "not", and Bx for "I believe x." I am ignoring some
complexities involving the future tense of the word "will" but I think
that is OK.
However now I am confused. How do I work with this letter B? What kind
of rules does it follow?
I understand that Bx, I believe x, is merely a shorthand for saying that
x is on my list of premises/conclusions. If I ever write down "x" on
my numbered list, I could also write down "Bx" and "BBx" and "BBBx" as far
as I feel like going. Is this correct?
But what about the other direction? From Bx, can I deduce x? That's
pretty important for this puzzle. If Bx merely is a shorthand for
saying that x is on my list, then it seems fair to say that if I ever
write down Bx I can also write down x. But this seems too powerful.
So what are the correct rules that I, as a simple machine, can follow for
dealing with the letter B?
The problem is that the rules I proposed here lead to a contradiction.
If x implies Bx, then I can write down:
8. t implies Bt
Note, this does not mean that if he is a knight I believe it, but rather
that if I ever deduce he is a knight, I believe it, which is simply the
definition of "believe" in this context.
But 6 and 8 together mean that t implies a contradiction, hence I can conclude:
9. ~t
He is a knave. 7 then implies
10. Bt
I believe he is a knight. And if Bx implies x, then:
11. t
and I have reached a contradiction with 9.
So I don't think I am doing this right.
Hal Finney