Теории с самопроверкой

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

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

$(\forall \; x,\; y)\; (\exists \; z)\; умножаем\; (x,\; y,\; z).\; \{\backslash \; displaystyle\; (\backslash \; forall\; x,\; y)\; \backslash \; (\backslash \; exists\; z)\; \backslash \; \{\backslash \; rm\; \{multiply\}\}\; (x,\; y,\; z).\}$

где $multiply\; \{\backslash \; displaystyle\; \{\backslash \; rm\; \{multiply\}\; \}\}$- трехзначный предикат, обозначающий $z\; /\; y\; =\; x\; \{\backslash \; displaystyle\; z\; /\; y\; =\; x\}$. Когда операции выражаются таким образом, доказуемость данного предложения может быть закодирована как арифметическое предложение, описывающее завершение аналитической таблицы. Тогда доказуемость непротиворечивости может быть просто добавлена ​​в качестве аксиомы. Результирующая система может быть доказана с помощью аргумента относительной согласованности по отношению к обычной арифметике.

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

• Роберт М. Соловей (9 октября 1989 г.). «Внесение несоответствий в модели PA». Анналы чистой и прикладной логики. 44 (1–2): 101–132. doi : 10.1016 / 0168-0072 (89) 90048-1.
• Уиллард, Дэн Э. (июнь 2001 г.). «Самопроверяющиеся системы аксиом, теорема о неполноте и соответствующие принципы отражения». Журнал символической логики. 66 (2): 536–596. doi : 10.2307 / 2695030.
• Уиллард, Дэн Э. (март 2002 г.). «Как расширить семантические таблицы и версии второй теоремы о неполноте почти до арифметики Робинсона Q». Журнал символической логики. 67 (1): 465–496. doi : 10.2178 / jsl / 1190150055.

• домашняя страница Дэна Уилларда.

.