In the book Forever Undecided, Raymond Smullyan discusses four different types of reasoners with increasing levels of self-awareness:
• A reasoner of type 1 is a perfect logician. She believes all tautologies, and if she believes the prepositions P and "P implies Q", then she also believes Q. However, she need not know anything about her own beliefs.
• A reasoner of type 2 is of type 1 and also knows that for any P and Q, if she believes both P and P implies Q then she will believe Q. I.e., she knows the rule by which she reasons, but she doesn't necessarily know what she believes.
• A reasoner of type 3 is of type 2 and is also aware of her own beliefs. If she believes P, then she will believe that she believes P. Reasoners who are aware of their own beliefs are said to be normal.
• A reasoner of type 4 is of type 3 and also knows that she is aware of her own beliefs. (For any P, she believes that if she believes P, she will believe that she believes P.)

Type 4 is the highest level of self-awareness. You might think it would be useful to say that a reasoner of type 5 knows that she is of type 4, but in fact a reasoner of type 4 already knows that she is of type 4. The proof is quite simple: we work through the things she has to know about herself in order to know that she is type 4. (In the context of this discussion, "know", and "correctly believe" are equivalent.)

• She must know that she believes all tautologies. This is easy: she does believe them, and because she is normal she knows that she believes them.
• She must know her inference rule that (P & (P->Q)) -> Q. This is just part of the definition of a type 2 reasoner.
• She must know that she knows her inference rule. She does, by the principle that a type 3 reasoner is aware of what she knows.
• She must know that she is normal (aware of her own beliefs). This was the final part of the definition of a type 4 reasoner.
• She must know that she knows she is normal. Again, this is an instance of the principle that she is aware of what she knows.