We give a reframing of Godel's first and second incompleteness theorems that applies even to some undefinable theories of arithmetic. The usual Hilbert-Bernays provability conditions and the diagonal lemma are replaced by a more direct diagonalization argument, from first principles, based in category theory and in a sense analogous to Cantor's original argument. To this end, we categorify the theory G\"odel encodings, which might be of independent interest. In our setup, the G\"odel sentence is computable explicitly by construction even for $\Sigma ^{0} _{2}$ theories (likely extending to $\Sigma ^{0} _{n}$). In an appendix, we study the relationship of our reframed second incompleteness theorem with arguments of Penrose.
翻译:我们重新表述了哥德尔第一和第二不完备性定理,使其甚至适用于某些不可定义的算术理论。通常的希尔伯特-伯奈斯可证性条件和对角引理被更直接的对角化论证所取代,该论证基于范畴论,在某种意义上类似于康托尔的原始论证。为此,我们对哥德尔编码理论进行了范畴化,这可能具有独立的研究意义。在我们的框架中,即使对于$\Sigma ^{0} _{2}$理论(可能推广至$\Sigma ^{0} _{n}$),哥德尔语句也可通过构造显式计算。在附录中,我们研究了重新表述的第二不完备性定理与彭罗斯论证之间的关系。