Некоторые сомнения в теоремах о неполноте

Итак, я могу добавить аксиому, что моя система S непротиворечива, и прийти к новой системе S', где S' = S + (S непротиворечива)

Да это нормально. Если вы позволите мне переключиться на переменные, которые легче отличить друг от друга, вы можете:

B = A + (A непротиворечиво)

Или даже

C = A + (A несовместимо)

Ни один (!) из них не повлечет за собой противоречия (но C не будет омега-непротиворечивым , что является более сильной формой непротиворечивости, которая возникает, когда вы пытаетесь согласовать теорию и метатеорию друг с другом). Ни B, ни C не могут доказать, что B/C само по себе непротиворечиво, хотя B, очевидно, доказывает, что A непротиворечиво.

Полное объяснение C здесь не рассматривается, но вкратце оно утверждает, что доказательство некоторого противоречия, такого как 0 = 1, существует и может быть закодировано с помощью некоторого гёделевского числа, но оказывается, что это число на самом деле не существуют в стандартной модели арифметики (это не 0, 1, 2 и т. д.). Арифметика Пеано недостаточно сильна, чтобы опровергнуть существование таких нестандартных чисел, поэтому внутри системы C не возникает противоречия. Тем не менее интуитивно очевидно, что C в каком-то смысле «неправильна», и именно в этом заключается омега-непротиворечивость.

Но есть большое исключение: если A уже несовместима, то она доказывает все , включая собственную непротиворечивость и собственную несовместимость, и эта несовместимость наследуется B и C. Когда мы говорим о какой-либо теореме о неполноте, мы всегда берем непротиворечивость теории как базового предположения, потому что мало что можно сказать о непоследовательной теории арифметики.

С другой стороны, мы не можем обойтись без чего-то вроде этого:

D = A + (D непротиворечиво)

Потому что оказывается, что если предположить, что вы можете найти способ выразить самореференцию (с умным использованием нумерации Гёделя), результирующая система будет противоречить второй теореме о неполноте и, следовательно, будет непоследовательной.

Теперь возвращаясь к вашим вопросам:

Это все еще не делает S последовательным! Или это так? Если я понимаю правила системы S, могу ли я снова увидеть, но не доказать непротиворечивость S, или непротиворечивость S все еще остается открытым вопросом?

Если вы считаете, что S' не доказывает каких-либо противоречий (или, что то же самое, что S' непротиворечиво), то вы обязательно верите, что S непротиворечиво, и поэтому доказательство не требуется. Если бы S было непоследовательным, то S' также было бы непоследовательным, и любые «доказательства», которые оно предоставляло, были бы бесполезны. Следовательно, вы не можете использовать S' для доказательства непротиворечивости S, потому что либо вы уже верите в непротиворечивость S, либо уже сомневаетесь в непротиворечивости S', и поэтому S' ничего для вас не дает.

Как непротиворечивость системы S связана с универсальной машиной Тьюринга для логики первого порядка? Я имею в виду, что является техническим аналогом непротиворечивости в машинах Тьюринга? Действительно ли мой компьютер не является доказуемо последовательным? И значит ли это, что когда-нибудь это может дать узнаваемое противоречие?

Тот факт, что вы не можете доказатьнепротиворечивость не означает, что система обязательно непоследовательна. Математики очень долго тщательно рассматривали непротиворечивость арифметики Пеано и теории множеств Цермело-Френкеля, и никто так и не доказал, что обе системы несовместимы. Мы могли бы представить себе, что однажды может быть сконструировано какое-то невероятно тонкое и сложное противоречие, но это не будет простым переформулированием, например, парадокса Рассела, потому что все «простые» проблемы, такие как парадокс Рассела, уже исследованы и «решены». Если бы мы когда-нибудь обнаружили такое противоречие, оно, вероятно, могло бы быть ограничено небольшой модификацией аксиом, чтобы исключить любую линию аргументации, ведущую к противоречию, поэтому мы, вероятно, могли бы восстановить большинство существующих математических теорем с небольшим нарушением.

Откровенно говоря, меня гораздо больше беспокоила бы возможность того, что программное обеспечение вашего компьютера содержит ошибки или неправильно разработано, чем то, что вся переписка Карри-Ховард рухнет в какой-то момент в ближайшем будущем. Программные ошибки случаются постоянно; математические ошибки (в последние годы) встречаются гораздо реже.

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

Возьмите несовместную систему S и создайте другую систему S', добавив аксиому «S' непротиворечива». Теперь у вас есть очень простое доказательство непротиворечивости S'. Но у вас все еще есть некоторое утверждение X с доказательством s как для X, так и для X, поэтому S' так же противоречиво, как и S, плюс вы имеете прямое противоречие с добавленной аксиомой!

Вместо этого добавьте аксиому «S' завершена». Но так же, как и в случае S, вы можете выразить утверждение X, говоря простым языком: «Для утверждения X нет доказательств». Нам не нужно доказывать или опровергать X, просто тот факт, что мы можем выразить это, приводит к срабатыванию закона Гёделя. Существование X показывает, что S' либо неполное, либо противоречивое. Конечно, добавленная аксиома показывает, что S' не является неполным, а, следовательно, противоречивым.

Что, если мы добавим «S' неполное»? Каждая несовместная система полна, так что мы снова имеем непосредственное доказательство того, что S' непротиворечива. Но доказательство того, что S' непротиворечиво, не избавляет его от непротиворечивости, так что ничего не выиграно.