Про Гёделя, Пенроуза и вычислимость
Ещё раз про вычислимость, теорему Гёделя о неполноте, алгоритмизуемость человеческого сознания и Роджера Пенроуза, получившего в этом году Нобелевку.
Почему это интересно?
С одной стороны это одна из наиболее удивительных и неожиданных теорем математики - о том, что (если опустить детали) в любой математической системе найдутся утверждения, которые ( Read more... )
Почему это интересно?
С одной стороны это одна из наиболее удивительных и неожиданных теорем математики - о том, что (если опустить детали) в любой математической системе найдутся утверждения, которые ( Read more... )
Во второй части довольно много ошибок.
>Мне это кажется странным. В формальной математической системе, если решение (доказательство) есть, то есть и алгоритм для его нахождения за конечное время.
пока правильно
>Как минимум, можно последовательно перебирать все возможные математические фразы, и для каждой проверять, не является ли она искомым доказательством. Пусть это долго и неэффективно, но это вполне корректный алгоритм, который наверняка рано или поздно найдёт доказательство, если оно существует.
а если не существует, "алгорим" не остановится никогда
>И поэтому отсутствие алгоритма для поиска решения означает отсутствие решения.
а как мы определим, что он не остановится?
далее вы совершаете подобную ошибку еще, плюс неправильно употребляется понятие "гёделевское утверждение" и делаете на его основе неверные выводы (в частности, гипотеза Гольдбаха может быть истинной или ложной, но в любом случае она не является гёделевским утверждением)
Reply
То есть, не существует алгоритма, который способен ответить на вопрос останова про любой другой алгоритм, но при этом не существует алгоритма, про который невозможно сказать, остановится он или нет - правильно?
А почему, из чего это следует? В частности, почему гипотеза Гольбаха не может являться гёделевским утверждением?
Reply
1) Утверждения типа гипотезы Гольдбаха или теоремы Ферма до 1996 года. Утверждение есть, оно содержит смысл и проверяема одна из его версий (позитивное или негативное утверждение)
В частности, если мы найдем число, которое нельзя представить в виде соответствующей суммы - мы ее опровергнем
И наоборот - если мы сможем _доказать_, что соответствующий алгоритм проверки не останавливается, мы покажем, что для всех N гипотеза справедлива, т.е. подтвердим ее
В данный момент мы не знаем, остановится ли алгоритм, но он либо остановится, либо нет (как и любой алгоритм)
2) Гёделевские утверждения - те, которые нельзя ни доказать, ни опровергнуть в указанной системе аксиом. Иначе говоря, если мы в существующую систему добавим утверждение А, получим непротиворечивую систему, и если добавим утверждение !A, то тоже получим непротиворечивую систему
В терминах формального вывода машиной Тьюринга, попытка доказать A приводит к бесконечной работе машины, и попытка доказать !А приводит к тому же
Если гипотезу можно доказать или опровергнуть, перебирая все выводы, то одна из двух запущенных машин (А или !А) когда-нибудь остановится
3) Теперь, если в вашем вопросе имеется в виду 1), то существует много алгоритмов, про которые на данном этапе развития математики мы не знаем, остановятся они или нет.
Если имеется в виду 2), то, по-видимому, таких машин нет, т.к. если принципиально нельзя сказать, остановится ли машина или нет, то она не остановится (в этом и заключается, вроде бы, аргумент Пенроуза)
Reply
И да, я о том и говорил, что Пенроуз (если я его правильно понял) считает, что человек из недоказуемости утверждения о том, остановится ли алгоритм, делает вывод, что этот алгоритм не остановится, а машина такой вывод сделать не сможет, т.к. формально этот вывод из аксиом не следует.
Добавление аксиомы о том, что все гёделевские алгоримы будем считать не останавливающимися, не изменит ситуацию, потому что утверждение о том, что этот алгоритм гёделевский, тоже может оказаться гёделевским.
То есть, в моих рассуждениях всё правильно?
И гипотеза Гольбаха не может оказаться гёделевским утверждением лишь в том смысле, что мы её в таком случае будем считать доказанной (ведь это будет значить, что привести пример такого числа невозможно), даже если отсутствие такого числа не будет следовать из аксиом Пеано - так?
Reply
Если предположить, что это алгоритмы, про которые нельзя (принципиально) сказать, останавливаются ли они, то, по моему мнению, это множество пусто.
Гипотеза Гольдбаха не доказана лишь в смысле 1). Можем ли мы вывести ее из системы аксиом - зависит от системы аксиом.
Кстати, вот и ошибка в предыдущем рассуждении. Утверждения "А истинно (в математическом смысле)" и "А выводится из каких-то аксиом" не эквивалентны. Т.е. факт того, что утверждение не вывелось из одной системы аксиом, не значит, что оно "невыводимо в принципе" (возможно, нужно притянуть другие области математики, как гипотезу Таниямы-Шимуры-Вейля, а дальше смотрите замечание про проект Володарского)
Reply
> Гипотеза Гольдбаха не доказана лишь в смысле 1). Можем ли мы вывести ее из системы аксиом - зависит от системы аксиом.
Когда говорим про аксиоматику системы натуральных чисел без явного указания системы аксиом, подразумеваем аксиоматику Пеано. Впрочем, не очень существенно, какую именно - достаточно того, что какую-то определённую. Гипотеза Гольдбаха взята просто как пример конкретного утверждения, ответ на которое мы не знаем. Можно было бы говорить "некое утверждение A", но с конкретным примером оно обычно воспринимается лучше. И вот это "некое утверждение A" в принятой аксиоматической системе может оказаться истинным, ложным или гёделевским.
> Утверждения "А истинно (в математическом смысле)" и "А выводится из каких-то аксиом" не эквивалентны
Это для меня выглядит парадоксально.
Если в аксиоматической системе S не выводится ни утверждение A, ни утверждение "не A", то мы можем расширить систему S, добавив в неё утверждение A или добавив в неё утверждение "не A", и получим две разных системы аксиом P и P', каждая из которых непротиворечива (при условии непротиворечивости S). Известные примеры такой ситуации - аксиома выбора и континуум-гипотеза.
Если у исходной системы S есть известная модель (интерпретация), то, возможно, лишь одна из систем P и P' будет соответствовать этой модели. Но с другой стороны, из теоремы о существовании модели следует, что и у второй из этих систем тоже есть модель.
Если не привязываться к конкретной системе аксиом, то как можно говорить об истинности утверждения в математическом смысле? Истинно ли в математическом смысле утверждение "сумма углов произвольного треугольника равна 180 градусам"? В одной системе аксиом истинно, в другой ложно, и говорить о математической истинности в отрыве от аксиоматики бессмысленно, как мне кажется.
> факт того, что утверждение не вывелось из одной системы аксиом, не значит, что оно "невыводимо в принципе"
Конечно, для любого гёделевского утверждения можно дополнить систему аксиом таким образом, чтобы оно перестало быть гёделевским. Например, какое-то утверждение из теории чисел (пусть та же гипотеза Гольдбаха) может оказаться недоказуемым в аксиоматике Пеано, но доказуемым, если добавить трансфинитную индукцию, подобно задаче о гидре и Геркулесе.
Мы знаем, что в любой системе аксиом (непротиворечивой и включающей арифметику) существуют гёделевские утверждения. Из этого следует, что в любой системе аксиом существуют гёделевские алгоритмы, т.е. алгоритмы, про которые в рамках этой системы аксиом невозможно ни доказать, что они остановятся, ни что они будут работать вечно.
Но это значит, что в этой системе аксиом невозможно привести пример невычислимого числа (по крайней мере, ни одним из известных мне способов), потому что все эти способы опираются на то, что произвольная машина Тьюринга либо остановится, либо не остановится. Если же остановка какой-то машины Тьюринга является гёделевским утверждением, то и утверждение о том, чему равна какая-то цифра невычислимого числа тоже является гёделевским утверждением. И число является невычислимым, потому что некоторые его цифры не следуют из аксиом. Скажем, оно может быть больше пяти или меньше пяти - и ни одно из этих утверждений не противоречит аксиомам. И для любой системы аксиом найдётся такой алгоритм и, соответственно, такая цифра этого невычислимого числа.
Вы говорите, что "на самом деле" (вы употребляете для этого термин "в математическом смысле") утверждение может быть истинно несмотря на то, что из аксиом это не следует. Именно об этом я говорил в посте. Что такое это "на самом деле", если это и не формально выводимое из данной системы аксиом, и не апелляция к реальному миру?
Reply
Из аксиоматики Пеано можно доказать не так много. Вообще это минимальная асиоматика, к которой доказана т.Гёделя
>> Утверждения "А истинно (в математическом смысле)" и "А выводится из каких-то аксиом" не эквивалентны
>Это для меня выглядит парадоксально.
>Если не привязываться к конкретной системе аксиом, то как можно говорить об истинности утверждения в математическом смысле?
Когда я говорю, что что-то истинно в математическом смысле (или как вы говорите, "на самом деле"), я имею в виду консенсус математиков о том, что это утверждение доказано. При доказательстве утверждений используются не только аксиомы Пеано, а вообще все. что наработано человечеством, плюс новые доказательства иногда вводят новые принципы (или правила вывода). Поэтому утверждение вполне может быть истинным, но даже понять доказательство смогут от силы десяток человек во всем мире.
К примеру, доказательство гипотезы Пуанкаре (Перельман) было принято матсообществом, и гипотеза считается истинной, т.е. доказанной. Доказательство abc-гипотезы (Мотидзуки) не было принято, и гипотеза считается в лучшем случае спорной.
Говорить о выводимости таких доказательств (а их большинство) в рамках какой-то формальной системы не приходится. Т.е. почти вся математика у вас становится "гёделевской".
Боюсь, даже доказательство самой т.Гёделя нельзя формализовать до автоматического, и тогда вы получите результат, что т.Гёделя есть гёделевское утверждение. Но внести в систему аксиом отрицание т.Гёделя нельзя, ибо это не так, как "на самом деле"
Reply
Ой-ой. Это кардинально отличается от моего представления о математике.
В частности, в моём представлении математическое утверждение не может изменить своё значение с истинного значения на ложное или наоборот (без изменения системы аксиом), в отличие от мнения консенсуса математиков. Например, если сначала консенсус математиков считал, что существует восемь типов пятиугольников, которыми можно замостить плоскость, а потом изменил своё мнение на 15, то для меня это означает, что консенсус математиков ошибался, а не что в то время утверждение о том, что существует всего восемь типов пятиугольников, было истинно в математическом смысле, а потом перестало быть истинным.
Иными словами, я считаю, что математическая истинность объективна и зависит от принятой системы аксиом, понятий и методов, а не от субъективного мнения некоторых людей-математиков.
И я предполагаю, что мнение консенсуса математиков об истинности в математическом смысле ближе к изложенному мной, чем вами.
Апелляция к системе авторитетов (а не к проверяемости и воспроизводимости) для науки как правило считается моветоном, а уж при определении истинности в математическом смысле - и вовсе выглядит странно.
Reply
Консенсус математиков никогда не считал, что пятиугольников 8 или 15, он считает, что их по крайней мере 15.
Если вы отрицаете апелляцию к авторитетам, то для вас и большая теорема Ферма, и гипотеза Пуанкаре остаются недоказанными.
Edit: прошу прощения, это моя вина. По ошибке я трижды назвал фамилию Володарский. Должно быть: Воеводский.
https://posic.livejournal.com/613891.html
http://philomatica.org/2017/10/%D0%B2%D0%BB%D0%B0%D0%B4%D0%B8%D0%BC%D0%B8%D1%80-%D0%B2%D0%BE%D0%B5%D0%B2%D0%BE%D0%B4%D1%81%D0%BA%D0%B8%D0%B9-1966-2017/
Reply
Нет, одно из другого не следует.
Из того, что я по разным причинам не имею возможности у себя на чердаке провести, скажем, эксперимент Майкельсона-Морли или, тем более, зарегистрировать гравитационные волны, вовсе не следует, что я считаю, что критерий истины в физике - консенсус физиков, или что эти эксперименты невоспроизводимы. Нет, критерий истины - воспроизводимость эксперимента и проверяемость теории. В этом основное отличие науки от религии.
Лично перепроверять все научные знания, доказательства и эксперименты слишком накладно и для человека нереально, поэтому мы доверяем это другим людям. Но доверять верификацию и делегировать установление истины - совсем не одно и то же.
Истинность или ложность гипотезы Пуанкаре или ABC-гипотезы не зависит от того, принято ли доказательство консенсусом математиков или не принято.
Reply
Reply
Я попробую изложить концепцию, которая у меня сложилась в голове на основании чтения книг о метаматематике и общения с математиками, но именно в таком виде я её не видел, поэтому, возможно, это лишь мои далёкие от реальности фантазии.
Есть доказательство в теории формальных систем. Оно формально и проверяемо. Тут нет места сентенциям вроде "но мы же понимаем" - если утверждение не следует из аксиом, то оно не может считаться истинным. К таким системам применима теорема Гёделя, и именно в таком ракурсе обычно рассматривают теорию чисел, планиметрию, теорию множеств, теорию групп. Утверждение "сумма углов произвольного треугольника равна 180°" истинно при одном выборе системы аксиом и ложно при другом, это нормально. Вполне можно изучать свойства формальной системы без понятной интерпретации - именно так делал Лобачевский.
И есть доказательство "по сути", неформальное. Оно не основывается на аксиомах, а применимо к платоновским мирам, которые в какой-то степени синхронизированы в головах математиков. В этом мире есть геометрия, есть числа, есть алгоритмы - как некие объекты со своими вполне определёнными свойствами, которые можно описывать аксиомами. Но, как выяснил Гёдель, полностью описать все свойства этих объектов аксиомами невозможно, т.е. невозможно построить формальную систему, описывающую все свойства этих объектов. Сложные математические доказательства вроде приведённых вами примеров - это про вот эти объекты, а не про формальные системы. Формализация их черезмерно сложна и громоздка, поэтому даже не пытаются.
И вот мы берём алгоритм из формальной системы. Находим его свойство, не следующее из аксиом (существует алгоритм, про который утверждение о том, что он остановится, невозможно ни доказать, ни опровергнуть). Теперь берём этот же алгоритм из платоновского мира. Там он не останавливается. Теперь из двух утверждений "невозможно доказать, что алгоритм останавливается" и "алгоритм не останавливается", которые по сути являются противоречивыми, получаем всякие интересные следствия. Потом эти следствия (полученные с применением платоновских свойств) запихиваем обратно в формальную систему, в теорию чисел. Получаем прикольные объекты вроде "невычислимое число", а при небольшой модификации даже "невычислимое целое неотрицательное число, меньше двух".
Reply
И что получим в итоге?
Если расширяем S утверждениями А или неА, то получаем непротиворечивые высказывания о условиях существования или несуществования объекта высказывания А.
Не так?
Reply
Например, в евклидовой геометрии и в геометрии Лобачевского существует прямая, параллельная данной, проходящая через точку, не лежащую на этой прямой (в геометрии Лобачевского таких прямых бесконечно много).
А в сферической геометрии таких прямых не существует.
Это и есть разные формальные системы, отличающиеся аксиомой - в одной из этих систем приняли A, а в другой - "не A", причём A - это как раз таки утверждение о существовании некого объекта.
Подобное можно сделать с аксиомой выбора: если её принять, появляется возможность построить нестандартный анализ, в котором существуют бесконечно малые и бесконечно большие числа, но и возникают некоторые неинтуитивные утверждения вроде парадокса Банаха-Тарского. Без аксиомы выбора получается другая система.
Reply
Геометрия Лобачевского не отменила известную теорему, а всего лишь в новой расширенной системе S предложила решение.
Неважно, что геометрия Евклида вырожденный случай геометрии Лобачевского - опровержения нет.
В гипотезе Гольдбаха мы тоже можем многое ввести и, при желании, можем доказать или опровергнуть формально, но нас интересует доказательство в определённой системе координат, которая постулируется натуральным и простым числом.
Reply
Возьмём алгоритм, который в одной своей ветке перебирает возможные решения уравнения, которое ему дано на вход, а в другой - все математические фразы в поисках доказательства, что это уравнение не имеет решения. Если такой алгоритм существует и будет на любых входных данных останавливаться, то это и будет универсальным алгоритмом решения произвольного диофантова уравнения. Но раз ответ на эту задачу звучит как "такого алгоритма не существует", это значит, что существует какое-то диофантово уравнение, для которого этот алгоритм никогда не остановится, т.е. не найдёт ни решение, ни доказательство отсутствия решения. Но то, что такой алгоритм никогда не остановится, означает, что вопрос наличия решений такого уравнения - гёделевское утверждение, т.к. его на основании системы аксиом невозможно ни доказать, ни опровергнуть.
В этих рассуждениях всё правильно или где-то ошибка?
Но раз вопрос наличия решений уравнения - гёделевское утверждение, то и вопрос о том, остановится ли алгоритм, занимающийся поиском этого решения, тоже является гёделевским утверждением. И это получается конкретный пример "гёделевского алгоритма".
Reply
Leave a comment