Peano's smart children: A provability logical study of systems with built-in consistency (Q1262309)

This very interesting paper studies several arithmetic systems with built-in consistency intended to escape the dire consequences of Gödel's second incompleteness theorem. One key notion is that of provably extensional self-reference by means of which the systems can prove their own consistency. The study adds further light and new questions to the relations between Gödel's two incompleteness theorems, as well as to the theory of bimodal systems.