  Still, Gödel’s original goal of defining intuitionistic logic in terms of classical provability was not reached, since the connection of \(\mathsf{S4}\) to the usual mathematical notion of provability was not established. Moreover, Gödel noted that the straightforward idea of interpreting modality \(\Box F\) as F is provable in a given formal system T contradicted Gödel’s second incompleteness theorem. Indeed, \(\Box ( \Box F \rightarrow F)\) can be derived in \(\mathsf{S4}\) by the rule of necessitation from the axiom \(\Box F \rightarrow F\). On the other hand, interpreting modality \(\Box\) as the predicate of formal provability in theory \(T\) and \(F\) as contradiction, converts this formula into a false statement that the consistency of \(T\) is internally provable in \(T\).