 Thus, it seems misguided to compare the strength of both notions or to combine them in one modal system. Perhaps formal provability is indeed in some sense a stronger notion than informal provability, but definitely this is not an arithmetic truth or validity, nor is the other direction. Discussions of the consequences of Gödel’s incompleteness theorems sometimes involve confusion around the notion of provability, giving rise to claims that humans could beat formal systems in “knowing” theorems (see Davis (1990, 1993) for good discussions of such claims).