Почему Тьюринг утверждает, что полная и вычислимая аксиоматизация арифметики подразумевает разрешимость логики первого порядка?

Итак, я читаю известную статью Тьюринга «О вычислимых числах с приложением к проблеме Entscheidungs». В начале своего доказательства неразрешимости логики первого порядка (FOL) он утверждает следующее:

Следует, пожалуй, заметить, что то, что я буду доказывать, сильно отличается от хорошо известных результатов Гёделя. Гёдель показал, что (в формализме Principia Mathematica) существуют предложения 𐌵 такие, что ни 𐌵 , ни ¬𐌵 недоказуемы. Как следствие этого показано, что в рамках этого формализма невозможно дать доказательство непротиворечивости Principia Mathematica (или K ). С другой стороны, я покажу, что не существует общего метода, который говорит, доказуема ли данная формула 𐌵 в K или, что то же самое, непротиворечива ли система, состоящая из K с присоединенной ¬𐌵 в качестве дополнительной аксиомы .

K является аксиоматизацией FOL, данной Гильбертом и Аккерманом . Кроме того, он утверждает:

Если бы было доказано отрицание того, что показал Гёдель, т. е. если бы для каждого 𐌵 доказуемо либо 𐌵 , либо ¬𐌵 , то мы должны были бы иметь немедленное решение проблемы Entscheidungsproblem. Ведь мы можем изобрести машину 𐌺 , которая будет последовательно доказывать все доказуемые формулы. Рано или поздно 𐌺 достигнет либо 𐌵 , либо ¬𐌵 . Если оно достигает 𐌵 , то мы знаем, что 𐌵 доказуемо. Если оно достигает ¬𐌵 , то, поскольку K непротиворечиво (Гильберт и Аккерман, стр. 65), мы знаем, что 𐌵 недоказуемо.

Таким образом, на первый взгляд и без дополнительных пояснений с его стороны, он, кажется, приравнивает два разных вида формальных аксиоматических систем: те, которые пытаются механизировать понятие достоверности в логике, и те, которые пытаются механизировать понятие истины в арифметике. .

Вероятно, он пытается понять, что существует способ закодировать в арифметике понятие 𐌵 как доказуемого предложения в K , так что, если арифметика завершена, то это предложение можно было бы доказать или опровергнуть в арифметике.

Любые предложения, чтобы понять, о чем он говорит здесь?

Заранее спасибо :)

Я не думаю, что он что-то приравнивает, он делает тривиальное наблюдение, что все теоремы в рекурсивно аксиоматизированной системе могут быть получены алгоритмически. Следовательно, если система также полна, это дает процедуру решения для доказуемости любого предложения. Потому что, когда мы просто генерируем все теоремы одну за другой, в конечном итоге генерируется либо 𐌵, либо ¬𐌵, и процедура гарантированно завершится.
Аксиоматические системы ЛЖ имеют иную природу, чем аксиоматические системы математики (кодифицированные как постулаты ЛЖ). Возьмем аксиоматическую систему арифметики. В арифметике любое выражение без свободных переменных либо истинно, либо ложно. Итак, если есть полная система, в ней рано или поздно появится любое выражение (утверждаемое или отрицаемое). В аксиоматизации FOL это не так, он выводит только допустимые выражения, а выражение, отрицание которого является допустимым, является противоречием, а не тавтологией. Полнота подразумевает разрешимость только в случае арифметики, а не в логике.
В этом посте более подробно рассказывается о разнице между обоими этими типами систем. Философия.stackexchange.com/ questions/15525/… Полная система логики (которая выводит каждое из допустимых выражений этой логики) не подразумевает разрешимости (поскольку она сообщает вам, когда выражение является допустимым или противоречащим, но не когда оно только выполнимо). Когда я говорю, что, по-моему, он приравнивает два разных вида систем, я имею в виду именно это различие.
Я не думаю, что он заботится о выполнимости. «Полнота» здесь просто означает, что все доказуемо или опровергаемо, поэтому по определению она подразумевает «разрешимость» как для арифметики, так и для логики.
Полнота в логической системе означает, что система способна выводить одно за другим каждое правильное выражение логики. Опять же, полнота в логической системе не означает разрешимости. «Вполне выполнимое» выражение никогда не появится в доказательствах, и его нельзя узнать, поскольку это может быть действительное выражение, которое просто еще не появилось. Опять же, аргумент Тьюринга применим к аксиоматизации арифметики, но не к аксиоматизации логики.
Статья Тьюринга написана в 1936 году. То, что сейчас подразумевается под полнотой в логической системе, в отличие от математической системы, спорно, важно только то, что он имеет в виду. И «полнота», как использует это слово Тьюринг, подразумевает разрешимость.
Они тесно связаны: если PA является конъюнкцией аксиом арифметики первого порядка, а T является формулой арифметики, мы имеем, что PA доказывает T тогда и только тогда, когда если PA, то T является допустимой формулой FO.
@MauroALLEGRANZA: Это ложь. PA не является конечно аксиоматизируемым. Однако смотрите мой ответ; Арифметика Робинсона (а также TC) конечно аксиоматизируема.

Ответы (2)

Вероятно, он пытается понять, что существует способ закодировать в арифметике понятие 𐌵 как доказуемого предложения в K, так что, если арифметика завершена, то это предложение можно было бы доказать или опровергнуть в арифметике.

Вы абсолютно правы. Гедель показал (с помощью своей β-леммы), что можно кодировать конечные последовательности натуральных чисел как натуральные числа и манипулировать ими, и все это в рамках PA (или эквивалента). Доказательство в любой вычислимой ЛОЛ-теории T — это просто последовательность формул, удовлетворяющих правилам вывода, которая, очевидно, может быть закодирована как конечная последовательность натуральных чисел. Кроме того, независимо от того, кодирует ли натуральное число доказательство над T, является Σ1-предложением (т. е. формой «∃k (...)», где все кванторы в «...» ограничены). Теперь PA является Σ1-полным, а это означает, что если Σ1-предложение истинно, то PA может это доказать. Итак, если T что-то доказывает, то PA может доказать этот факт!

Символически для любой вычислимой формальной системы T и любого предложения Q над T, если ( T ⊢ Q ), то ( PA ⊢ ProvT ), где Prov[T] — предикат языка PA.

Теперь должно быть ясно, что проблема заключается в случае ( T ⊬ Q ); где у нас нет гарантии, что ( PA ⊢ ¬ProvT ). (И на самом деле Гедель показал, что это вообще неверно.)

Но комментарий Тьюринга можно усилить, заявив, что если существует вычислимое непротиворечивое расширение E PA, которое доказывает каждое истинное Σ1-предложение и опровергает каждое ложное Σ1-предложение, то мы можем определить, является ли ( T ⊢ Q ), просто перечислив все теоремы из E, пока мы не найдем доказательство или опровержение ProvT.

Его первоначальный более слабый комментарий состоит просто в том, что не существует вычислимой непротиворечивой полной аксиоматизации натуральных чисел N (т. е. модели PA). Но даже просто просить о возможности опровергнуть каждое ложное Σ1-предложение уже достаточно плохо, как объяснялось выше. Все это по-прежнему опирается на β-лемму Гёделя, но объяснение несколько проще. Нужно только, чтобы ( T ⊢ Q ) тогда и только тогда, когда ( N ⊨ ProvT ).

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

Если вас интересует полностью обобщенная теорема Гёделя-Россера о неполноте, см. этот пост для простого доказательства, основанного на вычислимости.

Спасибо за ваш внимательный ответ, я посмотрю сообщение в блоге, которым вы любезно поделились. Только один дополнительный вопрос, последний абзац вашего объяснения мне не совсем ясен. Я знаю, что, будучи сформулированным как предложения FOL, доказуемость арифметического предложения будет эквивалентна доказуемости того, что предложение FOL действительно. Тем не менее, это не исключает возможности того, что какое-то понятие логической достоверности не будет отражено в конкретной модели РА. Почему необходимо, чтобы он был конечно аксиоматизируемым.
@JavierDiego-Fernández: То, что вы сказали во втором предложении, не соответствует действительности. Доказуемость всегда над некоторой заданной формальной системой. Нельзя просто сказать «доказуемо». Доказуемо чем? И, похоже, у вас есть базовые заблуждения о логической достоверности и моделях. В любом случае верно вот что: RA конечно аксиоматизировано, поэтому мы имеем ( RA ⊢ Q ) тогда и только тогда, когда ( ⊢ RAX⇒Q ), где RAX — это конъюнкция аксиом RA. Вы не можете сделать это с PA, потому что у него бесконечно много аксиом (и нет такой вещи, как бесконечная конъюнкция).

Вероятно, он пытается понять, что существует способ закодировать в арифметике понятие 𐌵 как доказуемого предложения в K, так что, если арифметика завершена, то это предложение можно было бы доказать или опровергнуть в арифметике.

На самом деле я не думаю, что он этого добивается. Похоже, он предполагает, что вы могли бы написать компьютерную программу, которая рекурсивно перечисляет все возможные доказательства (например, используя алгоритм поиска в ширину по дереву всех возможных доказательств, которые вы можете составить из аксиом, с некоторыми дополнительными тонкостями). иметь дело со схемами аксиом ). Это общая техника, которой «не важно», как выглядят ваши аксиомы. Если вы знаете, что система, что бы она ни кодировала, полна (что она доказывает каждое утверждение или его отрицание) и непротиворечива (что она никогда не доказывает утверждение и его отрицание), то эта техника всегда найдет доказательство или опровержение любого утверждения. вы хотите спросить о.

Однако, как признает Тьюринг, Гедель уже доказал, что любая система, которая может кодировать арифметику, не может быть одновременно полной и непротиворечивой, поэтому на самом деле это не работает. Затем аргумент Тьюринга доказывает более сильное утверждение о том, что не существует алгоритма , который действительно работает в этом случае.

Привет! Я заметил ваш комментарий здесь и хочу ответить на него, но не хочу привлекать нежелательное внимание со стороны чудаков (думаю, вы знаете, о ком я говорю). Ваш скептицизм неверен, и предположительно это потому, что вы на самом деле не знакомы с математической логикой и ZFC. Тривиально формализовать и сделать содержательные рассуждения о ТМ в достаточно естественной форме (т.е. без гёделевского кодирования) в ACA, который является явно предикативным фрагментом арифметики второго порядка Z2, которая намного слабее, чем ZFC .
По прочности PA = ACA0 < ACA << ATR << Z2 << ZC << ZFC. С кодированием Геделя можно фактически «делать» рассуждения о TM в PA (и в любой системе, которая интерпретирует PA). Вот как мы можем получить PA ⊢ Con(PA)⇒¬⬜Con(PA), где «⬜» — предикат доказуемости. Вы правы в том, что эти теоремы являются просто аргументами диагонализации (проблемы кодирования по модулю и симуляции), и именно поэтому теоремы Гёделя о неполноте доказуемы в столь слабых метасистемах. ACA доказывает, что каждое вычислимое подмножество N, которое кодирует теорию, интерпретирующую PA-, либо непоследовательно, либо неполно.
Только PA может доказать теорему о неполноте для любой конкретной вычислимой формальной системы, которая вычислимо интерпретирует PA- (т. е. при наличии компьютерной программы, которая является верификатором доказательств или генератором теорем для формальной системы, и программой, которая является переводом арифметических предложений в эту форму). системы, которая свидетельствует о том, что она интерпретирует PA-), мы можем построить доказательство по PA, что ассоциированная теория несовместима или неполна), и даже сделать это вычислимо (т. е. мы можем написать одну программу, которая дает программы для формальной системы и перевод выведет желаемое доказательство).
Вас могут заинтересовать некоторые другие подробности о теоремах о неполноте в этом посте и о ACA здесь . Если вы хотите узнать больше, добро пожаловать в этот чат .
Почему Тьюринг утверждает, что полная и вычислимая аксиоматизация арифметики подразумевает разрешимость логики первого порядка?
СпросиСетьПолитика конфиденциальности1y, 0v