  which does not seem to have an epistemically acceptable explicit  version. Consider, for example, the case where \(F\) is the  propositional constant \(\bot\)  for false. If an analogue of  Theorem 4 would cover the Löb Principle there would be  justification terms \(s\) and \(t\) such that  \(x :( s : \bot \rightarrow \bot ) \rightarrow t : \bot\) .  But this is intuitively false for factive justification. Indeed,  \(s : \bot \rightarrow \bot\)  is an instance of the Factivity Axiom. Apply Axiom Internalization to obtain  \(c :( s : \bot \rightarrow \bot )\) for some constant  \(c\). This choice of \(c\) makes the antecedent of  \(c :( s : \bot \rightarrow \bot ) \rightarrow t : \bot\)   intuitively true and the conclusion   false[4].  In particular, the Löb Principle (5) is not valid for the proof  interpretation (cf. (Goris 2007) for a full account of which  principles of \(\mathsf{GL}\) are realizable).