  From the provability perspective, it is the right form of negative  introspection. Indeed, let \(\Box F\) be interpreted as F  is provable and \(t : F\) as t is a proof of  F in a given formal theory \(T\), e.g., in Peano Arithmetic \(\mathsf{PA}\). Then (6) states  a provable principle. Indeed, if \(t\) is not a proof of  \(F\) then, since this statement is decidable, it can be  established inside \(T\), hence in \(T\) this sentence is  provable. On the other hand, the proof \(p\) of  ‘\(t\) is not a proof of \(F\)’ depends on both \(t\) and \(F , p = p ( t , F)\) and  cannot be computed given \(t\) only. In this respect, \(\Box\)   cannot be replaced by any specific proof term depending on \(t\) only and (6) cannot be presented in an entirely explicit  justification-style format.