  One of the common principles of knowledge is identifying  knowing and knowing that one knows. In a modal setting, this corresponds to \(\Box F \rightarrow \Box \Box F\). This principle has an adequate explicit counterpart: the fact that an agent accepts \(t\) as sufficient evidence for \(F\) serves as sufficient evidence for \(t : F\). Often such ‘meta-evidence’ has a physical form: a referee report certifying that a proof in a paper is correct; a computer verification output given a formal proof \(t\) of \(F\) as an input; a formal proof that \(t\) is a proof of \(F\), etc. A Positive Introspection operation ‘!’ may be added to the language for this purpose; one then assumes that given \(t\), the agent produces a justification !\(t\) of \(t : F\) such that \(t : F \rightarrow ! t :( t : F)\).  Positive Introspection in this operational form first appeared in the Logic of Proofs \(\mathsf{LP}\).