Automated proofs of Löb's theorem and Gödel's two incompleteness theorems (Q1110495)

In the seventies, a number of logicians began the study a system of propositional modal logics now known as provability logic. In the paper, the author formalizes the modal logic K4 within the automated reasoning system ITP, which is a powerful resolution theorem prover. Based on the connections between propositional modal logic K4 and notions relating to provability in formalized Peano arithmetic, the author represents Löb's theorem, Gödel's first incompleteness theorem and Gödel's second incompleteness theorem within ITP as follows: If ThmK4\(((x\leftrightarrow (b(x)\to y)))\) and ThmK4\(((b(y)\to y))\) then ThmK4\((y)\). If ThmK4\(((x\leftrightarrow \sim b(x)))\) \& ThmK4\((x)\) then ThmK4\((F)\). If ThmK4\(((x\leftrightarrow \sim b(x)))\) \& ThmK4\((\sim b(F))\) then ThmK4\((F)\). Where the predicate ``ThmK4(x)'' in ITP means that the formula x is a theorem of K4, ``F'' represents falsity. (The provability of F means that the system is inconsistent.) Then, using ITP, the author provides very high level automated proofs of Löb's theorem and Gödel's two incompleteness theorems.