Откуда нам знать, что мы случайно не говорим о нестандартных целых числах?

[В этом ответе я буду считать само собой разумеющимся, что стандартные целые числа «существуют» в некотором платоническом смысле, поскольку в противном случае мне не ясно, имеет ли ваш вопрос даже смысл.]

Ты думаешь обо всем этом неправильно. Верите ли вы, что аксиомы PA верны для стандартных целых чисел? Тогда вы также должны верить, что все, что вы доказываете из PA, верно и для стандартных целых чисел. В частности, если вы докажете, что существует какое-то целое число с некоторым свойством, это утверждение о существовании будет истинным для стандартных целых чисел.

Иными словами, все, что вы доказываете на основе своих аксиом, истинно в любой модели аксиом, стандартной или нестандартной. Так что существование нестандартных моделей совершенно не имеет значения. Важно только, существует ли стандартная модель (другими словами, верны ли ваши аксиомы для стандартных целых чисел).

Теперь я должен указать, что это понятие намного более скользкое для чего-то вроде ZFC, чем для чего-то вроде PA. С философской точки зрения идея о том, что на самом деле существует платоновская «стандартная теоретико-множественная вселенная», которую правильно описывает ZFC, гораздо менее последовательна, чем соответствующее утверждение для целых чисел. Насколько нам известно, ZFC на самом деле может быть непоследовательным, и поэтому он доказывает все виды ложных утверждений о целых числах. Или, может быть, он непротиворечив, но все еще доказывает ложные утверждения о целых числах (потому что он имеет только нестандартные модели). Но если вы действительно верите, что аксиомы ZFC верны в их предполагаемой интерпретации, то вы должны верить, что любые их следствия также верны (включая следствия, касающиеся целых чисел).

Чтобы говорить о «стандартных» целых числах, у кого-то уже должна быть некоторая коллекция «целых чисел», которые они считают «стандартными». Конечно, они могут не знать всего об этих целых числах, но им нужно думать, что существует определенный набор объектов, которые являются «стандартными целыми числами». Точно так же у кого-то может быть набор объектов, который, по его мнению, является «стандартной» моделью теории множеств.

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

Например, аксиомы арифметики Пеано (ПА) обычно считаются верными в отношении стандартных натуральных чисел, а аксиомы ZFC — в отношении стандартной модели теории множеств. Это основной ответ на вопрос: если мы докажем, что машина Тьюринга останавливается, используя здравую теорию, то машина Тьюринга на самом деле остановится, потому что по определению каждое утверждение, доказуемое в здравую теорию, истинно относительно соответствующей стандартной модели.

Мы могли бы пойти дальше и спросить: как мы можем доказать эту надежность? Один из вариантов — прямое, неформальное обращение к интуиции. Другой вариант — доказать состоятельность одной системы аксиом в другой формальной системе аксиом — метатеории.

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

Например, ZFC доказывает, что арифметика Пеано верна, а теория множеств Морса-Келли доказывает, что теория множеств ZFC верна. Проблема здесь, как и в случае с последовательностью, заключается в том, что существует своего рода регресс. Чтобы доказать, что теория множеств Морса-Келли верна, нам нужно предположить еще более сильную метатеорию, а чтобы доказать, что она верна, нам нужно принять еще более сильную метатеорию.

Именно тогда вариант «прямое обращение к интуиции» становится более привлекательным. Точно так же, как мы могли бы поверить, что аксиомы евклидовой геометрии верны в отношении плоскости$\mathbb{R}^2$не доказывая этого в какой-либо конкретной метатеории, мы могли бы в принципе полагать, что PA и ZFC верны, не беспокоясь о том, в какой метатеории может быть доказана правильность. Это зависело бы от нашей веры в то, что аксиомы этих формальных систем являются истинными утверждениями о предпочтительные «стандартные» модели.

Мы знаем, что никакая формальная система не может полностью определить натуральные числа.

Я, кстати, именно об этом и говорил здесь . Помимо того, что я сказал в этом посте, я хотел бы уточнить следующие моменты:

• Обобщенная версия теоремы Гёделя-Россера о неполноте убедительно показывает, что не существует практической формальной системы, которая могла бы определить натуральные числа. В частности, мы можем легко написать программу, которая по любой программе проверки доказательств для любой формальной системы, интерпретирующей арифметику, выдаст явное арифметическое предложение, которое эта система не может ни доказать, ни опровергнуть. Насколько убедительно? Если формулировать теорему о неполноте определенным образом, ее можно доказать даже в интуиционистской логике. Но нам все равно нужно работать в какой-то метасистеме, которая «имеет доступ» к модели PA или ее эквиваленту, иначе мы не можем даже говорить о конечных цепочках, которые являются базовыми строительными блоками любой практической формальной системы.

• Философская проблема заключается в том, что в том, что касается реального мира, эмпирические данные свидетельствуют о том, что реальной модели PA не существует, отчасти из-за конечного размера наблюдаемой Вселенной, а также из-за того, что физическое запоминающее устройство с чрезвычайно большой емкостью (порядка размера наблюдаемой Вселенной) будет деградировать быстрее, чем вы сможете его использовать! Таким образом, с предыдущим пунктом возникает странная философская проблема, потому что если кто-то не верит, что набор конечных строк встраивается в реальный мир, то теоремы о неполноте на самом деле неприменимы...

• С другой стороны, существуют неопровержимо огромные эмпирические доказательства того, что теоремы PA, переведенные в утверждения о программах реального мира, верны в человеческом масштабе. Например, не существует известного контрпримера к теоремам, лежащим в основе расшифровки RSA, которые зависят от малой теоремы Ферма среди других основных теоретико-числовых теорем, применяемых к натуральным числам порядка$2^{2048}$. Таким образом, все еще нужно объяснить невероятную точность PA в малых масштабах, даже если у нее нет реальной модели.

Но если отказаться от философского недоверия и работать со слабой формальной системой, называемой ВДА, которую практически каждый логик считает надежной (по отношению к реальному миру), мы действительно можем сказать о многом (кроме теоремы о неполноте) с уверенностью. ответьте на свой вопрос (если ВДА в порядке).

Предположим, что для некоторой конкретной машины Тьюринга$Z$, я доказал, что$Z$останавливается [через некоторое число$N$шагов. Как я могу знать наверняка, что$N$является стандартным натуральным числом, а не нестандартным?

Ваше доказательство сделано в рамках некоторой формальной системы$S$. Если$S$является$Σ_1$-звук (по отношению к реальному миру), то вы можете точно знать, что$Z$действительно останавливается. Вполне возможно, что$S$не является$Σ_1$-звук, и что вы никогда не сможете понять это. Например, для любой практической формальной системы$S$который интерпретирует арифметику, пусть$S' = S + \neg \text{Con}(S)$. Если$S$непротиворечиво, то$S'$также соответствует, но$Σ_1$- нездоровый. В частности, это доказывает, что верификатор доказательства для$S$останавливается на каком-то предполагаемом доказательстве противоречия$S$, это именно тот тип вопроса, который вас беспокоит!

Что еще хуже, арифметическая несостоятельность формальной системы может лежать на любом уровне арифметической иерархии, как конструктивно показано в этом посте . Именно, если$S$является$Σ_n$-звук, то есть$Σ_n$-звуковое расширение$S$то есть$Σ_{n+1}$- нездоровый.

Это означает, что может быть трудно быть уверенным в надежности формальной системы без какого-либо философского обоснования. Во-первых, несостоятельность нельзя обнаружить, проверив доказательство несоответствия. Сейчас если$S$достаточно выразительно, мы можем сказать:$S$арифметически правильно" над$S$, и в этом случае мы можем проверить доказательство его отрицания над$S$, и если это так, мы знаем, что что-то действительно не так. Но даже для простой непротиворечивости, если мы перечисляем (бесконечно) все возможные доказательства и никогда не находим противоречия, мы по-прежнему перечисляем только «бесконечно малую» долю всех возможных доказательств, слишком мало, чтобы быть уверенным, что противоречия действительно нет.

Становится хуже. Рассмотрим следующее:

Позволять$Q$быть некоторым$Π_1$-предложение такое, что$S$доказывает ($Q$верно, если нет доказательства$Q$над$S$с менее чем$2^{10000}$символы).

Оказывается, мы действительно можем легко построить такое предложение$Q$, используя стандартные приемы гёделевского кодирования и теорему о неподвижной точке. Что может шокировать тех, кто не знаком с этим, так это то, что$Q$на самом деле довольно короткий (менее миллиарда символов, если$S$что-то вроде ZFC), и если$S$является$Σ_1$-полный, то$Q$доказуемо более$S$(потому что$S$может проверить каждое возможное доказательство менее чем$2^{10000}$символы), но его кратчайшее доказательство имеет по крайней мере$2^{10000}$символы!

Теперь пусть$T = S + \neg Q$, где$S$имеет любую разумную дедуктивную систему. Во-первых,$T$непоследовательно. Во-вторых, кратчайшее доказательство его несостоятельности порядка$2^{10000}/len(Q)$, потому что его можно преобразовать в доказательство ($\neg Q \to \bot$) над$S$, что после конечного числа дополнительных шагов дало бы доказательство$Q$над$S$.

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

Окончательно:

Я понимаю, что ответ на этот вопрос может зависеть от характера доказательства того, что$Z$остановки, которые я не указал. Если это так, то какие виды доказательств подлежат этой проблеме, а какие нет?

Из всего вышесказанного должно быть ясно, что это действительно так. Чтобы повторить, вам нужно доказательство того, что$Z$останавливается в формальной системе, которая$Σ_1$-звук. Как ты мог это знать? Ну, мы не можем знать ничего подобного наверняка. Почти все логики считают, что АСА арифметически корректен, но разные логики начинают сомневаться в правильности в разных точках по мере того, как вы поднимаетесь вверх по иерархии формальных систем. Некоторые сомневаются в полной арифметике второго порядка, называемой Z2, из-за ее непредикативной аксиомы понимания. Другие думают, что все еще в порядке, но сомневаются в ZFC. Некоторые думают, что ZFC — это хорошо, но сомневаются в некоторых больших кардинальных аксиомах.

Потому что у вас есть явное формальное описание (как кодировать) машины Тьюринга и их выполнение.

К особенностям этого формального описания относятся:

• места на ленте пронумерованы натуральными числами
• шаги трассировки выполнения индексируются натуральными числами
• интерпретация строк как чисел приводит к выводу натуральных чисел

^{Таким образом, вы можете быть уверены, что какую бы модель} анализа вы ни использовали в качестве исходных данных для теории вычислений, все числа, которые выведет ваша машина, будут натуральными числами этой модели.

_{*: Под «моделью анализа» я в основном подразумеваю модель любого ограниченного количества теории множеств / теории типов / логики высшего порядка / всего, что вам нужно рассуждать.}

Однако вы можете развить теорию вычислений в нестандартной модели анализа. Натуральные числа, которые может вычислить такая машина, конечно, вполне могут быть нестандартными.

Однако должна быть возможность взять стандартную машину Тьюринга и преобразовать ее в нестандартную. И вполне возможна ситуация, когда у вас есть стандартная машина Тьюринга и нестандартная модель анализа, для которой стандартная машина может работать вечно, а нестандартная ее версия останавливается.

Я даже думаю, что возможно, что какая-то нестандартная модель говорит, что ваша стандартная машина останавливается, а какая-то другая нестандартная модель говорит, что машина не только работает вечно, но и будет работать вечно в каждом нестандартном расширении этой модели!