 In standard metamathematics, an important role for a thorough understanding of the second incompleteness theorem is played by Löb’s theorem (Löb 1955). The proof of the theorem is related to Curry’s paradox (see this entry, and  Curry’s Paradox)  and to an informal argument due to Geach 1955. Furthermore, Löb’s theorem is essential for defining mathematical structures, which are adequate for providing versions of self-reference and incompleteness (see the so-called Magari algebras and the modal analysis of formal provability, Boolos 1993). In the same direction, there are applications of Berry’s paradox. For instance, in 1966 Vopenka proved the second incompleteness theorem for the Bernays-Gödel theory of sets and classes using a form of the same paradox. Boolos 1989 exploits a Berry-type argument to prove incompleteness in the form “there is no algorithm whose output contains all true statements of arithmetic and no false ones” without appealing to diagonalization. The Berry paradox has been related to the incompleteness phenomena also because of work (going back to the sixties and the seventies) in the so-called Kolmogorov complexity and algorithmic information theory. In particular, Chaitin has shown in a number of papers how to exploit randomness to prove certain limitations of formal systems (see Chaitin 1995). In connection with Chaitin’s results, Kritchman and Raz 2011 gives a proof of the second incompleteness theorem, which is based on an argument resembling the surprise-test paradox (see  epistemic paradoxes).  In turn, this paradox can be explicitly related to Solovay’s completeness theorem of provability logic (see Montagna 1994), and more recently Egré 2005, De Voos, Kooj and Verbrugge 2018 applied provability logic to solving the Knower’s paradox. It is worth recalling that – again on the side of epistemic logic – self-reference is applicable in order to prove incompleteness in belief models. Brandenburger and Keisler (2006) identified a paradox of self-reference in beliefs in games, which yields a game-theoretic impossibility theorem akin to Russell’s Paradox. An informal version of the paradox is that the following configuration of beliefs is impossible: Ann believes that Bob assumes that Ann believes that Bob’s assumption is wrong. This is formalized to show that any belief model of a certain kind must have a ’hole’. An interpretation of the result is that “if the analyst’s tools are available to the players in a game, then there are statements that the players can think about but cannot assume.” Also, the mere fact of paradoxes like this one, with a distinct logical “flavour”, but arising out of treatments involving epistemic notions, is notable, as it can be regarded as an indication for a direction of work that, hinging upon the many examples already available in the literature, is likely to expand and become systematic in the future thanks to the application of formal methods (see also this entry, §6.5 on this). Although not directly connected with the incompleteness phenomenon, there are indeed several accounts of antinomies affecting what appear to be sets of apparently legitimate, natural postulates involving certain epistemic notions. Let Leitgeb 2021 work as an ultimate example of sources of this sort, presenting a solution to the lottery paradox (see Kyburg 1961 and  epistemic paradoxes)  that affects principles relating categorical belief to graded belief (see also Douven 2021 that contains the former source).