 In \((M, w)\), the atomic proposition p is the case, but the agent does not know it: \((M, w) \Vdash p \land \lnot Kp\). Thus, \(p \land \lnot Kp\) can be truthfully announced, which produces the pointed model \((M_{(p \land \lnot Kp){!}}, w)\) on the right. Note how w has survived the operation (it satisfies \(p \land \lnot Kp)\), but u has not (it does not satisfy \(p \land \lnot Kp\), as it makes p false). In the resulting pointed model, the agent indeed knows that p is the case: \((M_{(p \land \lnot Kp){!}}, w) \Vdash Kp\). Nevertheless, she does not know that she does not know p: \((M_{(p \land \lnot Kp){!}}, w) \not\Vdash K\lnot Kp\); in fact, she knows that she knows p: \((M_{(p \land \lnot Kp){!}}, w) \Vdash  KKp\).[12]