  (Pacuit 2006, Rubtsova 2006) considered the Negative Introspection operation ‘?’ which verifies that a given justification assertion is false. A possible motivation for considering such an operation is that the positive introspection operation ‘!’ may well be regarded as capable of providing conclusive verification judgments about the validity of justification assertions \(t : F\), so when \(t\) is not a justification for \(F\), such a ‘!’ should conclude that \(\neg t : F\). This is normally the case for computer proof verifiers, proof checkers in formal theories, etc. This motivation is, however, nuanced: the examples of proof verifiers and proof checkers work with both \(t\) and \(F\) as inputs, whereas the Pacuit-Rubtsova format ?\(t\) suggests that the only input for ‘?’ is a justification \(t\), and the result ?\(t\) is supposed to justify propositions \(\neg t : F\) uniformly for all \(F\)s for which \(t : F\) does not hold. Such an operation ‘?’ does not exist for formal mathematical proofs since ?\(t\) should then be a single proof of infinitely many propositions \(\neg t : F\), which is impossible.  The operation ‘?’ was, historically, the first example that did not fit into the original framework in which justifications were abstract versions of formal proofs. 