Самопроверяющиеся теории

Самопроверяющиеся теории — это непротиворечивые первого порядка системы арифметические , гораздо более слабые, чем арифметика Пеано , которые способны доказывать свою собственную непротиворечивость . Дэн Уиллард был первым, кто исследовал их свойства, и описал семейство таких систем. Согласно теореме Гёделя о неполноте , эти системы не могут содержать ни теорию арифметики Пеано, ни ее слабый фрагмент арифметики Робинсона ; тем не менее, они могут содержать сильные теоремы.

Вкратце, ключом к построению Уиллардом своей системы является формализация достаточного количества механизма Гёделя , чтобы говорить о доказуемости внутри системы, не имея возможности формализовать диагонализацию . Диагонализация зависит от способности доказать, что умножение является полной функцией (а в более ранних версиях результата также и сложением). Сложение и умножение не являются функциональными символами языка Уилларда; вместо этого вычитание и деление являются предикатами сложения и умножения, определяемыми в их терминах. Здесь невозможно доказать $\Pi _{2}^{0}$ предложение , выражающее совокупность умножения:

(\forall x,y)\ (\exists z)\ {\rm {multiply}}(x,y,z).

где

{\rm {multiply}}

- это трехзначный предикат, обозначающий

z/y=x.

Когда операции выражаются таким образом, доказуемость данного предложения может быть закодирована как арифметическое предложение, описывающее завершение аналитической таблицы . Тогда доказуемость непротиворечивости можно просто добавить как аксиому. Непротиворечивость полученной системы можно доказать с помощью аргумента относительной непротиворечивости относительно обычной арифметики.

Далее можно добавить любое истинное $\Pi _{1}^{0}$ арифметическое предложение теории, сохраняя при этом последовательность теории.