  This theorem establishes that a system of justification terms for  \(\mathsf{S4}\) will necessarily  be self-referential. This creates a serious, though not directly  visible, constraint on provability semantics. In the Gödelian  context of arithmetical proofs, the problem was coped with by a  general method of assigning arithmetical semantics to  self-referential assertions \(c : A ( c)\) stating that \(c\) is a proof of \(A ( c)\). In the Logic of Proofs \(\mathsf{LP}\) it was  dealt with by a non-trivial fixed-point construction.