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 - øåñòîé âñ¸ ïîêàçûâàåò ïðàâèëüíî. Íàäî, íàäî îáíîâëÿòüñÿ ïî óòðàì è âå÷åðàì ;)

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 11:00 pm
Powered by Dreamwidth Studios