avva: (Default)
[personal profile] avva
Эта запись продолжает цикл: задача о Геркулесе и гидре, решение, объяснение арифметики
ординалов
.

Наконец можно рассказать о самом (с моей точки зрения) интересном. Строго доказать я ничего не смогу, слишком много предварительной механики пришлось бы доказывать, но подробно объяснить и дать ссылку смогу.

Начну издалека — формальной логической системой PA (сокращённо Peano Arithmetic).

Ещё с конца 19-го века известно, что довольно простой набор аксиом полностью определяет все возможные арифметические истины. Аксиомы эти принято было называть аксиомами Пеано. Вот один возможных их набор. Скажем, у нас есть логический язык, в котором присутствует константа 0, функциональный символ S(x) (долженствующий обозначать "следующее за x натуральное число"), функциональные символы + и * (для сложения и умножения). Определим следующие аксиомы:

1. S(x) = S(y) => x=y.
2. ¬∃x ( S(x) = 0 ). ("не существует x такого, что S(x)=0")
3. x + 0 = x
4. x + S(y) = S(x+y)
5. x * 0 = 0
6. x * S(y) = x * y + x
7. Если M - множество натуральных чисел так, что 0 ∈ M, и для каждого x выполняется x∈M => S(x)∈M, тогда для каждого x выполняется x∈M (принцип индукции).

(словами без символов: 7. Если М - множество натуральных чисел, так, что 0 принадлежит к М и для каждого x из "x принадлежит к M" следует "S(x) принадлежит к M", то тогда любой возможный x принадлежит к M)

Можно (это довольно легко) доказать, что любые две структуры, выполняющие аксиомы 1-7, полностью изоморфны друг другу. Т.е. аксиомы 1-7 содержат в себе полную характеризацию множества натуральных чисел N с операциями сложения и умножения (а другие привычные операции и отношения, вроде порядка и возведения степень, можно определить через них).

Однако аксиома 7 является утверждением второго порядка: она говорит не о числах, а о произвольных множествах чисел. Если мы хотим оставаться в рамках логики первого порядка (и по многим разным причинам мы действительно этого хотим), то лучшее, на что мы можем надеяться, это следующая версия аксиомы 7:

7". Пусть φ(x) - некоторая формула со свободным параметром x. Если выполняется φ(0) , а также утверждение ∀x (φ(x) => φ(S(x))), тогда формула φ верна для всех натуральных чисел: ∀xφ(x) (индукция первого порядка).

(словами эта формула говорит: если выполняется phi(0), а также для любого x из phi(x) следует phi(S(x)), то тогда выполняется phi(x) для любого x).

7" на самом деле является не аксиомой, а схемой аксиом: для каждой возможной формулы φ существует отдельная аксиома 7", которую формально можно записать так: [φ(0)∧∀x (φ(x) => φ(S(x)))] => ∀xφ(x) .

Формальную систему, построенную из аксиом 1-6 и схемы 7", называют обычно системой PA, Peano Arithmetic (хоть это и несколько анти-исторично, т.к. сам Пеано индукцию первого порядка не предлагал и о ней не задумывался).

PA - очень мощная формальная система по своей доказательной силе. Логики изучают доказательную силу формальных систем при помощи формализации в них абстрактных понятий и доказательств. Так, например, в PA можно очень легко формализовать практически все комбинаторные рассуждения и теоремы, манипулирующие конечным кол-вом объектов; множество результатов из теории графов и других подобных "дискретных" областей математики. Вполне нетривиальным является, скажем, вопрос о том, достаточна ли сила PA для того, чтобы формализовать в ней недавнее доказательство теоремы Ферма. В PA можно формализовать и доказать части анализа и теории множеств, и т.д. и т.п.

Короче говоря, PA - очень мощная формальная система, не такая мощная, конечно, как теория множеств, в которой мы обычно проводим математические доказательства и рассуждения, но всё же очень мощная. Она очень хорошо, в частности, "схватывает" все наши интуитивные представления и методы работы с натуральными числами.
По множеству разных причин PA - очень популярная для изучения система аксиом в логике последних 50 лет; например, она тесно связана с теорией вычислимости, машинами Тюринга и т.п.

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

Долгое время, однако, у математиков не было ни одного примера естественного математического утверждения, недоказуемого в PA. Например, в теории множеств таким утверждением является гипотеза о континууме. В арифметике же простого и естественного примера не было (конечно, "естественность" здесь - понятие очень неформальное; но ясно, что, например, недоказуемое утверждение, к-е строится в процессе док-ва теоремы Гёделя, независимого от логики математического интереса не имеет).

И вот в конце 70-х и начале 80-х Парис и Кирби нашли сразу несколько таких примеров — "естественных" математических утверждений, которые, с одной стороны, верны, с другой стороны, недоказуемы в PA. Само по себе это является очень интересным логическим результатом; но с интуитивной точки зрения что это говорит нам об этих проблемах? - да то, что любое их доказательство обязано использовать методы, не-формализуемые в PA, т.е. в какой-то мере "сложные", "бесконечные" методы. У такого рода задач не может быть "простых", легко формализуемых решений.

Первым примером такого рода утверждений была так называемая "конечная теорема Рамзи"; это теорема из комбинаторики. А вот задачка про Геркулеса и гидру тоже являет собой, открытый несколько позднее, пример утверждения, недоказуемого в PA. А именно: утверждение "Любая стратегия Геркулеса приводит к уничтожению гидры" верно, но недоказуемо в PA. Это и означает на практике невозможность относительно "простого" решения этой задачи, при помощи относительно элементарных рассуждений, стремящихся ограничить рост числа голов, или пытающихся перенумеровать гидры числами (а не ординалами, как в действительно работающем решении), и т.п.

Остаток записи посвящу краткому объяснению того, как доказывают, что утверждение о том, что любая стратегия выигрывает, недоказуемо в PA. То, что это утверждение верно, я уже объяснил в предыдущих записях.

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

Почему PA не может доказать "любая вычислимая стратегия Геркулеса приводит к победе"?

В середине 30-х годов немецкий учёный Генцен доказал непротиворечимость формальной системы PA (точнее , немного другой системы, но различия незначительны). Согласно второй теореме о неполноте Гёделя, никакая непротиворечимая и достаточно сложная формальная система не может доказать собственной непротиворечимости. В частности, PA не может доказать Cons(PA), где Cons(PA) означает утверждение о непротиворечимости (consistency) PA. Мы предполагаем при этом, что PA действительно непротиворечима, что в рамках современной математики является тривиальным утверждением (т.к. пользуясь всей мощью теории множеств мы просто можем построить модель для PA - а именно, множество натуральных чисел N. Любой набор аксиом, имеющий модель, непротиворечив). Но доказать непротиворечимость PA при помощи финитарных (конечных) методов - невозможно, поскольку все такие методы можно формализовать внутри самой PA, а сама PA своей непротиворечивости доказать не может.

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

Что такое эта индукция? Она совершенно аналогична обычной индукции по натуральным числам, только простирается "дальше" на бесконечные ординалы до ε0. Она говорит следующее: если некоторое утверждение верно для 0, а также его истинность для всех ординалов меньше α влечёт его истинность для ординала α (и это верно для любого α<ε0), тогда это утверждение верно для любого ординала меньше ε0.

Этот принцип трансфинитной индукции верен потому, что ординалы до ε0 (да и после тоже) вполне упорядочены (см. в записи про ординалы объяснение того, как из вполне-упорядоченности следует принцип индукции). То есть не существует бесконечной нисходящей последовательности таких ординалов.

Собственно говоря, доказательство Генцена можно представить в виде, напрямую использующем это свойство вполне-упорядоченности. Генцен построил некое отображение доказательств в формальной системе PA в ординалы, при котором каждому формальному док-ву присваивается свой ординал меньше ε0, и показал, что если существует доказательство противоречия в PA (т.е. если PA противоречива), то это док-во можно сократить так, чтобы получить другое док-во противоречия в PA, которому соответствует меньший ординал. Продолжая так неопределённо долго, мы построим бесконечныю нисходящую последовательность ординалов, что невозможно; поэтому доказательства противоречия в PA быть не может.

Что из этого следует? А следующее: принцип трансфинитной индукции до ε0, а вместе с ним и вполне-упорядоченность всех ординалов до ε0, невозможно доказать в PA. Потому что если бы их там можно было доказать, всё док-во Генцена можно было бы формализовать в PA и тогда PA доказывала бы свою непротиворечимость, что невозможно согласно второй теореме Гёделя о неполноте.

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

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

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

В этом месте я вынужден несколько затушевать подробности (чтобы их определить и доказать, потребовалось бы слишком много технических результатов и методов) и сказать следующее. Вполне-упорядоченность ординалов означает, что любая нисходящая последовательность ординалов имеет конечную длину. Стратегия, описанная выше, даёт нам для каждого начального ординала (=каждой начальной гидры) некую определённую спускающуюся, но очень медленно спускающуюся, последовательность ординалов. Можно показать, что если бы PA могла доказать, что такая медленно спускающаяся последовательность ординалов неизбежно заканчивается за конечное числов шагов, то PA могла бы показать то же самое для любой спускающейся последовательности ординалов, возникающей в доказательстве Генцена, о котором см. выше.

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

А если PA не может доказать это для данной конкретной стратегии, то естественно она не может доказать и более сильное, и верное, утверждение "любая вычислимая стратегия приводит к победе Геркулеса". И поэтому "простого" доказательства у задачи о Геркулесе и гидре нет.

Всё.

P.S. Reference:
L. Kirby and J. Paris, Accessible independence results for Peano arithmetic. Bull. London Math. Soc. 14 (1982), p.285-225.

Âèäèìî, íå÷èòàåìûé ñèìâîë

Date: 2002-02-26 09:34 am (UTC)
From: [identity profile] boroda.livejournal.com
â PA2 - êâàíòîð ñóùåñòâîâàíèÿ, à â PA7- çíàê "ïðèíàäëåæàòü ìíîæåñòâó"? Ãðå÷åñêèå áóêâû â IE âèäíî, à âîò ýòè ñèìâîëû íè îí, íè Îïåðà íå ïîêàçûâàþò :(
From: [identity profile] avva.livejournal.com
Äà, âñ¸ âåðíî. PA2: "íå ñóùåñòâóåò x òàêîãî, ÷òî S(x)=0". PA7: "åñëè 0 â X è äëÿ êàæäîãî n èç ïðèíàäëåæíîñòè n ê X ñëåäóåò ïðèíàäëåæíîñòü S(n) ê X, òî ëþáîå ÷èñëî íàõîäèòñÿ â X".

Ó ìåíÿ â IE âñ¸ âèäíî ;)

Ñåé÷àñ ïðîéäó åù¸ ðàç ïî çàïèñè è âåçäå ñëîâàìè äîáàâëþ, ãäå ìîæåò áûòü íå âèäíî.
From: [identity profile] boroda.livejournal.com
Ïîõîæå, ýòî ãëþê ýêñïëîðåðà 5.5 - øåñòîé âñ¸ ïîêàçûâàåò ïðàâèëüíî. Íàäî, íàäî îáíîâëÿòüñÿ ïî óòðàì è âå÷åðàì ;)

Date: 2002-02-26 10:29 am (UTC)
From: [identity profile] french-man.livejournal.com
Äåéñòâèòåëüíî êðóòî. Òû ýòèì ïðîôåññèîíàëüíî çàíèìàåøüñÿ?

Date: 2002-02-26 10:55 am (UTC)
From: [identity profile] avva.livejournal.com
Íåò, íå ïðèõîäèëîñü. Ïðîñòî ýòà òåìà (model theory of PA and in particular natural independence results) î÷åíü íðàâèòñÿ.

Date: 2002-02-26 01:52 pm (UTC)
From: [identity profile] squadette.livejournal.com
à Âû ñîçíàòåëüíî ïèøåòå ñëîâî "íåïðîòèâîðå÷èìîñòü"?

Re:

Date: 2002-02-26 07:14 pm (UTC)
From: [identity profile] avva.livejournal.com
Íåò, ýòî ïðîñòî ãëóïàÿ îïèñêà, ÿ ïèñàë â îäèí ïðèñåñò è òîðîïèëñÿ (îò íåõâàòêè âðåìåíè).ß ïîòîì ïðîéäóñü ïî çàïèñè è èñïðàâëþ ýòî, ñïàñèáî.

Date: 2002-02-26 09:34 pm (UTC)
From: [identity profile] kukutz.livejournal.com
Ñïàñèáî!

Î÷åíü èíòåðåñíî.

Åñëè ó âàñ êîãäà-íèáóäü áóäåò âðåìÿ, íå ðàññêàæåòå â äâóõ íàó÷ïîï-ñëîâàõ ïðî èñïîëüçîâàííûå â çàäà÷å ïðî ìàòåìàòèêîâ óëüòðàôèëüòðû?

Date: 2002-02-27 12:26 am (UTC)
From: [identity profile] sova.livejournal.com
Ýòî íàäî áóäåò ïåðå÷èòàòü. Explicit==ÿâíî. metamath.org

Date: 2002-02-27 02:41 pm (UTC)
From: [identity profile] d-off.livejournal.com
Îäíàêî êàêîâ èíòåðåñ! ß ïîëàãàþ, ÷òî áîëüøèíñòâî çàèíòåðåñîâàâøèõñÿ íåïîñðåäñòâåííîãî îòíîøåíèÿ ê ìàòåìàòèêå íå èìåþò è òåì íå ìåíåå íèêîãî íå îñòàíàâëèâàåò íåäîñòàòîê èíôîðìàöèè î òåõ èëè èëè èíûõ âåñüìà ñïåöèôè÷íûé îáúåêòàõ. ×òî-òî â íå-ðóññêîé ñðåäå ìíå íå äîâîäèëîñü íàáëþäàòü ïîäîáíîãî èíòåðåñà... Ìîæåò íå ïîâåçëî èëè äåéñòâèòåëüíî åñòü â íàñ ÷òî-òî îñîáåííîå?

Date: 2015-05-07 09:21 am (UTC)
From: [identity profile] gul-kiev.livejournal.com
Мне в этом не дают покоя два вопроса.

1. Истинна ли трансфинитная индукция, или это нечто вроде континуум-гипотезы, которую можно принять произвольным образом? Если второе, то доказательство не очень убеждает. Ведь Геркулес либо на самом деле в любом случае победит гидру за конечное число ходов, либо нет, и ответ "если примем трансфинитную индукцию, то победит, а если нет, то нет" кажется странным.

2. Могут ли какие-то из известных недоказанных утверждений в теории чисел оказаться гёделевскими? Например, гипотеза Гольбаха (что любое чётное число можно представить в виде суммы двух простых чисел), или её всё-таки наверняка возможно либо доказать, либо опровергнуть?

Date: 2015-05-07 10:35 am (UTC)
From: [identity profile] avva.livejournal.com
Трансфинитная индукция следует из стандартных аксиом теории множеств, в отличие от континуум-гипотезы. Если вы принимаете истинность аксиом теории множеств, то можно пользоваться трансфинитной индукцией (подозреваю, что даже аксиома выбора для проблемы Геркулеса и гидры не нужна, или может быть очень слабая ее версия).

Если вы согласны пользоваться только аксиомами арифметики Пеано включая индукцию (PA), то вы не можете доказать, что Геркулес побеждает гидру за конечное число ходов. Остается ли это тем не менее верным утверждением о натуральных числах? Предположим, я скажу 'да', этого будет достаточно для вас - наверное нет, вы потребуется доказательства, так? Доказательство этого факта доступно двумя способами:

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

Теория множеств (ZFC) доказывает много разных утверждений о натуральных числах, включая все аксиомы PA. Отсюда следует, что теория множеств доказывает также все, что доказуемо в PA. Но кроме этого теория множеств доказывает еще всяческие утверждения о натуральных числах, и возможно, не все они истинны. Например, если теория множеств противоречива, она доказывает вообще все что угодно. Но может случиться и так, что теория множеств непротиворечива, однако она доказывает какое-то утверждение T о натуральных числах, которое является ложным. Тогда отсюда следует, что его противоположность not-T, истинное утверждение, должно быть слишком сложным для PA (если бы PA доказывала not-T, то и ZFC бы его доказывала, и тогда not-T и T дают противоречие в ZFC). Следует отметить, что есть широкий класс утверждений, которые, если они истинны, PA точно может доказать (например, все утверждения вида 10+10=20 с любыми числами).

Теперь предположим, что есть гидра, которую Геркулес никогда не побеждает. ZFC доказывает, что Геркулес побеждает любую гидру, включая эту, и отсюда следует (опускаю технические подробности), что есть конкретное натуральное число X и конкретная стратегия поведения Геркулеса, про которые ZFC доказывает утверждение T "после X-го хода из этой последовательности ходов гидра мертва". Но из нашего предположения следует, что T ложно, а его противоречие not-T "после X-го хода из этой последовательности ходов гидра жива" истинно. Однако not-T достаточно простое утверждение, чтобы его истинность была доказуема в PA.

Могут ли какие-то из известных недоказанных утверждений в теории чисел оказаться гёделевскими? Например, гипотеза Гольбаха (что любое чётное число можно представить в виде суммы двух простых чисел), или её всё-таки наверняка возможно либо доказать, либо опровергнуть?

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

Такой мета-аргумент работает только для относительно простых утверждений в теории чисел (и других частях математики). Скажем, его не применить к гипотезе Римана. Так что она может быть неразрешима, и при этом как ложной, так и истинной. На практике вряд ли можно найти хотя бы одного эксперта в теории чисел, который бы всерьез думал, что гипотеза Гольдбаха неразрешима (и то же верно про гипотезу Римана).

Date: 2015-05-07 12:25 pm (UTC)
From: [identity profile] gul-kiev.livejournal.com
Большое спасибо за развёрнутый ответ.

Аргументация про простоту утверждения not-T и, соответственно, логика "если такое утверждение недоказуемо, то оно верно" мне понятна.
Только мне кажется, что по такой же логике получается, что если континуум-гипотеза недоказуема, то она верна, и, что интереснее, если аксиома выбора недоказуема, то она неверна. Однако математиков нисколько не смущает доказуемая невозможность привести пример объекта - они вполне свободно принимают аксиому выбора и, соответственно, существование таких заведомо неизвестных объектов. Не могут ли они столь же свободно принять аксиому "гипотеза Гольбаха неверна" (в предположении, что она недоказуема) и оперировать чётными числами, не являющимися суммой двух простых, зная, что пример таких чисел привести заведомо невозможно, как сейчас они оперируют ультрафильтрами и вполне упорядочивают множество действительных чисел?

Кстати, почему такая аргументация неприменима к гипотезе Римана? Там ведь, казалось бы, ситуация очень похожа: либо существуют нетривиальные нули дзета-функции Римана с действительной частью не 1/2 (и тогда можно привести пример), либо их не существует. Из недоказуемости должно следовать их отсутствие, разве нет?

Ну и в порядке игры разума - может ли утверждение "гипотеза Римана является гёделевским утверждением" оказаться гёделевским? Допустима ли бесконечная степень косвенности таких утверждений (глубина рекурсии)?

December 2025

S M T W T F S
  123 4 56
78 9 10 11 1213
1415 1617181920
21 22 23 24 2526 27
28293031   

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Dec. 28th, 2025 05:14 pm
Powered by Dreamwidth Studios