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