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

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

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

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

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

В дальнейшем можно добавить к теории любое истинное арифметическое предложение, сохраняя при этом последовательность теории. ${\ displaystyle \ 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 .

Внешние ссылки [ править ]

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

Эта статья о логике - незавершенная . Вы можете помочь Википедии, расширив ее .