Про Гёделя, Пенроуза и вычислимость

[gul_kiev]

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

Почему это интересно?
С одной стороны это одна из наиболее удивительных и неожиданных теорем математики - о том, что (если опустить детали) в любой математической системе найдутся утверждения, которые

Comments

[iaroshenko]

>Когда говорим про аксиоматику системы натуральных чисел без явного указания системы аксиом, подразумеваем аксиоматику Пеано.

Из аксиоматики Пеано можно доказать не так много. Вообще это минимальная асиоматика, к которой доказана т.Гёделя

>> Утверждения "А истинно (в математическом смысле)" и "А выводится из каких-то аксиом" не эквивалентны
>Это для меня выглядит парадоксально.
>Если не привязываться к конкретной системе аксиом, то как можно говорить об истинности утверждения в математическом смысле?

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

К примеру, доказательство гипотезы Пуанкаре (Перельман) было принято матсообществом, и гипотеза считается истинной, т.е. доказанной. Доказательство abc-гипотезы (Мотидзуки) не было принято, и гипотеза считается в лучшем случае спорной.

Говорить о выводимости таких доказательств (а их большинство) в рамках какой-то формальной системы не приходится. Т.е. почти вся математика у вас становится "гёделевской".

Боюсь, даже доказательство самой т.Гёделя нельзя формализовать до автоматического, и тогда вы получите результат, что т.Гёделя есть гёделевское утверждение. Но внести в систему аксиом отрицание т.Гёделя нельзя, ибо это не так, как "на самом деле"

[gul_kiev]

> Когда я говорю, что что-то истинно в математическом смысле (или как вы говорите, "на самом деле"), я имею в виду консенсус математиков о том, что это утверждение доказано.

Ой-ой. Это кардинально отличается от моего представления о математике.

В частности, в моём представлении математическое утверждение не может изменить своё значение с истинного значения на ложное или наоборот (без изменения системы аксиом), в отличие от мнения консенсуса математиков. Например, если сначала консенсус математиков считал, что существует восемь типов пятиугольников, которыми можно замостить плоскость, а потом изменил своё мнение на 15, то для меня это означает, что консенсус математиков ошибался, а не что в то время утверждение о том, что существует всего восемь типов пятиугольников, было истинно в математическом смысле, а потом перестало быть истинным.
Иными словами, я считаю, что математическая истинность объективна и зависит от принятой системы аксиом, понятий и методов, а не от субъективного мнения некоторых людей-математиков.
И я предполагаю, что мнение консенсуса математиков об истинности в математическом смысле ближе к изложенному мной, чем вами.

Апелляция к системе авторитетов (а не к проверяемости и воспроизводимости) для науки как правило считается моветоном, а уж при определении истинности в математическом смысле - и вовсе выглядит странно.

[iaroshenko]

Я в третий раз отсылаю вас к проекту Володарского и к причинам, по которым он начал этот проект.

Консенсус математиков никогда не считал, что пятиугольников 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/

[gul_kiev]

> Если вы отрицаете апелляцию к авторитетам, то для вас и большая теорема Ферма, и гипотеза Пуанкаре остаются недоказанными.

Нет, одно из другого не следует.
Из того, что я по разным причинам не имею возможности у себя на чердаке провести, скажем, эксперимент Майкельсона-Морли или, тем более, зарегистрировать гравитационные волны, вовсе не следует, что я считаю, что критерий истины в физике - консенсус физиков, или что эти эксперименты невоспроизводимы. Нет, критерий истины - воспроизводимость эксперимента и проверяемость теории. В этом основное отличие науки от религии.

Лично перепроверять все научные знания, доказательства и эксперименты слишком накладно и для человека нереально, поэтому мы доверяем это другим людям. Но доверять верификацию и делегировать установление истины - совсем не одно и то же.

Истинность или ложность гипотезы Пуанкаре или ABC-гипотезы не зависит от того, принято ли доказательство консенсусом математиков или не принято.

[gul_kiev]

Проект Воеводского - спасибо, буду смотреть.

[gul_kiev]

Похоже, тут смешались два по сути разных значения слова "доказательство" и именно из-за этой путаницы (поочерёдного применения одного или второго смысла в последовательном рассуждении) и возникли странные последствия вроде неалгоритмизуемости сознания.

Я попробую изложить концепцию, которая у меня сложилась в голове на основании чтения книг о метаматематике и общения с математиками, но именно в таком виде я её не видел, поэтому, возможно, это лишь мои далёкие от реальности фантазии.

Есть доказательство в теории формальных систем. Оно формально и проверяемо. Тут нет места сентенциям вроде "но мы же понимаем" - если утверждение не следует из аксиом, то оно не может считаться истинным. К таким системам применима теорема Гёделя, и именно в таком ракурсе обычно рассматривают теорию чисел, планиметрию, теорию множеств, теорию групп. Утверждение "сумма углов произвольного треугольника равна 180°" истинно при одном выборе системы аксиом и ложно при другом, это нормально. Вполне можно изучать свойства формальной системы без понятной интерпретации - именно так делал Лобачевский.

И есть доказательство "по сути", неформальное. Оно не основывается на аксиомах, а применимо к платоновским мирам, которые в какой-то степени синхронизированы в головах математиков. В этом мире есть геометрия, есть числа, есть алгоритмы - как некие объекты со своими вполне определёнными свойствами, которые можно описывать аксиомами. Но, как выяснил Гёдель, полностью описать все свойства этих объектов аксиомами невозможно, т.е. невозможно построить формальную систему, описывающую все свойства этих объектов. Сложные математические доказательства вроде приведённых вами примеров - это про вот эти объекты, а не про формальные системы. Формализация их черезмерно сложна и громоздка, поэтому даже не пытаются.

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