 Obviously, it is assumed that our formal systems are also equipped with a system of rules of inferences (and possibly some logical axioms), usually some standard system of classical logic (though the incompleteness theorems do not essentially presuppose classical logic, but also apply to systems with, e.g., intuitionistic logic). The above standard systems all come with classical logic. The standard notation \(F \vdash A\) is used to express (in the meta-level) that \(A\) is derivable in \(F\), that is, that there is a proof of \(A\) in \(F\), or, in other words, that \(A\) is a theorem of \(F\). Accordingly, \(F \not\vdash A\) means that \(A\) is not derivable in \(F\).