The latter embodies the idea of unrestricted Logical Awareness for \(\mathsf{J}\). A similar rule appeared in the Logic of Proofs \(\mathsf{LP}\), and has also been anticipated in Goldman’s (Goldman 1967). Logical Awareness, as expressed by axiomatically appropriate Constant Specifications, is an explicit incarnation of the Necessitation Rule in Modal Logic: \(\vdash F \Rightarrow\, \vdash \Box F\), but restricted to axioms. Note that \(\mathsf{J}\) coincides with \(\mathsf{J}_{TCS}\).