О новом классе теорий, удовлетворяющих второй теореме Гёделя о неполноте

Популярная нестрогая формулировка второй теоремы Гёделя о неполноте утверждает Всякая достаточно выразительная теория не доказывает собственной непротиворечивости. Стандартным способом уточнить формулировку "достаточно выразительная теория" являются требования о том, что теория интерпретирует некоторую арифметическую теорию, в которой можно развить теорию работы с формулами и доказательствами, как гёделевыми номерами. Нами будет рассмотрен другой подход к уточнению этой формулировки, фактически, позволяющий приблизиться к нестрогой формулировке Всякая теория, которая может выразить утверждение о своей непротиворечивости не может его доказать. Формальнее, нами рассматриваются классические первопорядковые теории, в которых есть некоторое кодирование формул языка самой теории и теория доказывает ряд свойств формул при этом кодирование. Для таких теорий нами устанавливается лемма о неподвижной точке. Далее, стандартным методом может быть установлено, что для любого предиката, удовлетворяющего условиям Гильберта-Бернайса-Лёба, в такого рода теориях не может доказать свою непротиворечивость относительно этого предиката. Отметим, что само требование на кодирование формул не гарантирует, что теории интерпретируют даже такую слабую теорию, как арифметика Робинсона Q и, более того, такие теории даже могут быть разрешимы. В частности, примером разрешимой теории с таким свойством является теория канторовской функции пары (хотя обратим внимание, что для этой теории нет невырожденных предикатов, удовлетворяющих условиям Гильберта-Бернайса-Лёба).