 This is clearly an idealization, and as such it makes sense only under certain interpretations; still, it might imply more than meets the eye. Assuming that the agent never forgets the truth-value of an atomic proposition p might be reasonable; but, what if \(\varphi\) is a more complex formula, in particular one involving the epistemic modality? For example, take the formula \(\lnot Kp \land \lnot K\lnot p\) (“the agent does not know whether p”), yielding the instance \(K(\lnot Kp \land \lnot K\lnot p) \rightarrow GK(\lnot Kp \land \lnot K\lnot p)\) (“if the agent knows of her ignorance about whether p, then she will always know about such ignorance”). Is this within the expected consequences?