?

Log in

No account? Create an account

Previous Entry | Next Entry

Гедель 3

1  2   3   4  5  6  7

VIII. Машина доказательств

ФСС элементарной арифметики (ФСЭА), как мы уже знаем, производит строки, интерпретируемые как утверждения арифметики. Она содержит аксиомы, начальные верные строки, и выводит новые строки — теоремы. Мы не будем рассматривать конкретные аксиомы8 и правила вывода новых строк из уже выведенных; нам достаточно помнить, что они заданы. В алфавит ФСЭА входят символы для кодирования чисел и переменных, операции + и ×, сравнение =, скобки, кванторы существования E и всеобщности A (мне придется обозначить их латинскими буквами из-за типографских ограничений), и логическое отрицание ~. Числа кодируются в такой же «единичной» системе, какую мы уже рассматривали, количеством «звездочек». Так же кодируются и переменные, только начинаются они со специального символа переменной x: вместо x, y, z, a, b система выдает x•, x••, x••• и т. д. В примерах ниже мы, однако, будем записывать числа в десятичной записи, а переменные буквами.

Примеры утверждений, которые выводит ФСЭА:

Ex:x×2=6

Здесь говорится, что число 6 четно (найдется такое число x, что 2×x=6)

~Ex:Ey:(x+1)×(y+1)=13

13 простое число: не существует таких x и y, что (x+1)×(y+1)=13. Прибавление единицы требуется, чтобы каждый сомножитель был больше 29.

Ax:Ea:~Eb:Ec:(x+a)=(b+1)×(c+1)

Здесь утверждается, что существует бесконечно много простых чисел. Следует читать это так: для любого x найдется a такое, что не существует таких b и c, чтобы равенство (x+a)=(b+1)×(c+1) выполнялось. Иными словами, для каждого x найдется такое a, что (x+a) будет простым числом. Поскольку a>0, то и x+a>x: какое число x ни возьми, найдется простое число, еще большее.

В образовании смысла строк мы следуем правилам, которые мы же сами установили для их интерпретации. Например, «~» мы читаем «неверно, что», A как «для всех», E как «для одного или более», «:» как «верно следующее:», и так далее. Тогда утверждения, выводимые ФСЭА, становятся теоремами. Являются ли они «истинными»? Здесь нужно задуматься о понятии истинности.

Мы изначально полагаем аксиомы истинными, верными утверждениями. Их запись в виде строк ФСЭА интерпретируется именно так, как мы того хотим, с тем смыслом, которые мы в них закладывали, когда придумывали эти строки10. Являются ли истинными в этом смысле и теоремы? Ровно настолько, насколько мы можем доверять формальному механизму вывода, аппарату формальных систем.

На поверхности кажется, что этот механизм работает надежно. Можно увидеть, как выводятся приведенные выше утверждения, которые мы понимаем как верные в арифметике. Но ведь теорем, которые производит ФСЭА, бесконечно много. Поэтому мы должны поставить вопрос «доверия» к нашей механике вывода. В ФСС сложения чисел доказательство было довольно простым, однако, ФСЭА намного сложнее, и ее «правильность» отнюдь не очевидна.

Вопросы касательно ФСЭА, которыми мы зададимся, следующие. Во-первых, нас интересует, все ли возможные теоремы арифметики выведет наша машина? Например, будет ли среди ее строк доказательство Великой теоремы Ферма? Предположения Гольдбаха? Свойство, которое нас интересует, мы назовем полнотой системы: система полна, если она выводит, в интерпретации смысла, все истинные утверждения в некоей области.

Второй, еще более важный вопрос, который нас волнует: не произойдет ли так, что два утверждения, полученных ФСЭА, будут противоречить одно другому? Например, одним путем мы получим утверждение, что предположение Гольдбаха истинно, а другим — что оно ложно. Такое нарушение будет фатальным для всей системы арифметики: из противоречия можно вывести все, что угодно! Это легко показывается в формальной логике. Из такого противоречия следует, что 0=1, что 2×2=5, что простых чисел не существует, что их существует конечное количество, что количество простых чисел бесконечно — все, что пожелаете. Противоречия в выведенных теоремах ни в коем случае быть не должно. Свойство системы не выдавать противоречивых (в интерпретации смысла) утверждений назовем непротиворечивостью.

Является ли элементарная арифметика полной и непротиворечивой теорией? Над этим вопросом работали великие математики начала XX в. Попытка вывести самообоснованность теории множеств тогда потерпела неудачу11. В ответ на это Давид Гильберт сформулировал в начале 20-х гг. программу по поиску способа вывода всех математических утверждений из аксиом путем механической вычислительной процедуры. Формулировка требований, заданных Гильбертом к аксиомам и процедурам математики, такова: требуется найти (а) процедуру, которая бы выводила все без исключения истинные математические утверждения, и только истинные, из заданного однажды набора аксиом; (б) самый набор этих аксиом и (в) алгоритм доказательства любого наперед заданного утверждения, чтобы определить за конечное время, возможно ли вывести это утверждение из аксиом (в таком случае, оно истинно) или нет (и тогда оно ложно).

Таким образом, Гильберт сформулировал задачу поиска, в наших терминах, полной и непротиворечивой формальной системы арифметики, и дополнил ее требованием конструктивной вычислимости 12принадлежности лексически верной строки множеству синтаксически верных строк.

Над реализацией этой программы математики работали еще 10 лет, до тех пор, пока Курт Гедель не обнаружил фундаментальное свойство формальных систем, которое предопределило неудачу программы Гильберта и невозможность аксиоматизации математики.

IX. Бета-код Геделя

Рассуждение Геделя основано на арифметическом кодировании алфавита, строк и правил ФС. В самом деле, мы можем закодировать алфавит ФС числами. Когда мы это сделаем, правила переписывания строк ФС можно записать в виде арифметических операций над числами. О любом числе можно задать вопрос, является ли это число кодом лексически верной строки в данной ФС. Если ответ на него положительный, далее можно спросить, является ли это число также и кодом синтаксически верной строки. Если да — то мы имеем дело, на семантическом уровне, с кодом теоремы арифметики. Таким образом, выходит, что среди чисел есть подмножество кодов теорем арифметики. Множество всех остальных чисел можно назвать множеством не-теорем арифметики (либо они лексически недопустимы, либо не выводимы системой). Будем называть числа вычислимыми формальной системой, если они выводимы нашей закодированной числами ФС.

Для примера, закодируем нашу первую систему ХИХИ в виде чисел: заменим Х на 1, И на 2, А на 313. Начальная верная строка ХИ тогда первращается в число 12. Теперь перепишем на языке чисел правила системы.

1. К любому числу, заканчивающемуся на 2, можно дописать в конец 3. Математически это можно выразить так: если n вычислимое число, и остаток от деления его на 10 равен 2, то 10×n+3 тоже вычислимое число.

2. Любую «подстроку», следующую за 1, можно «удвоить». Операции «взятия подстроки» и «удвоения», разумеется, следует записать арифметически. Пусть наше число содержит в середине или в начале 1 (пример 23132). Часть, заканчивающуюся 1 (231 в примере) запишем как m×10+1, где m≥0 (в нашем примере m=23). Чтобы приписать к этому числу «хвост» (32), умножим его на 10n, где n — длина «хвоста» (у нас n=2, 10n=102=100): (m×10+1)×10n, в нашем примере это будет 23100, а затем просто прибавим «хвост», то есть запишем формулу как (m×10+1)×10n+j, где j обозначает «хвост» (у нас j=32). Чтобы он поместился в отведенное ему разрядное место, мы должны ввести ограничение j<10n. «Удвоить хвост» можно, еще раз умножив результат на 10n и прибавив j. Таким образом, правило (2) можно сформулировать так:

Если (m×10+1)×10n+j, где j<10n, вычислимое число, то и (m×10+1)×10n+j)×10n+j вычислимое число.

Запись правил (3) и (4) в арифметической форме оставим как упражнение читателю.

Все это выглядит чрезвычайно запутанным и искусственным, но нас сейчас не интересует сложность и «неинтересность» этого вывода. Самое главное здесь, что путем формального, механического преобразования можно перейти от записи правил операций над строками к записи правил в виде операций над их кодами, числами. А как только мы переведем описание ФС на язык арифметики, мы сможем сформулировать и задачи, ставящие вопросы об этой ФС, на том же языке арифметики. Например, задача о выводимости ХА переформулируется в таком виде: входит ли число 13 во множество чисел, вычисляемых данной, описанной в виде арифметических действий, ФС?

X. Теоремы Геделя

Ничто не препятствует нам распространить рассуждения о кодах ФС на самое арифметику, вернее, ее формальную систему — ФСЭА. Переписав ее правила в виде арифметических алгоритмов, мы закодируем каждое утверждение, получаемое ФСЭА, натуральным числом.

Что интересного произойдет, когда мы сделаем это? ФСЭА достаточно мощна, чтобы порождать язык арифметики. В тоже самое время, мы переписали ее правила на тот же самый язык! Иными словами, в таком выражении ФСЭА формулирует утверждения о себе. Например, мы можем спросить, входит ли число X во множество чисел-кодов утверждений ФСЭА? Тем самым, мы задаем вопрос, является ли число Х кодом верного утверждения, то есть теоремы, арифметики. Понятно, что число мы можем теперь рассматривать двояко: как собственно число, и как код утверждения о числах.

Гедель доказывает, что возможно (и показывает, как) сконструировать в ФСЭА утверждение «Число G не входит во множество кодов теорем, выводимых ФСЭА», таким образом, чтобы код этого утверждения в точности совпал с самим числом G14. Каковы последствия существования такого числа?

Попробуем «спросить» арифметику об истинности этого утверждения. Верно ли на самом деле, что число G не входит во множество кодов теорем, выводимых ФСЭА?

Предположим, что ответом арифметики на этот вопрос будет «да». Это означает, что утверждение это выводимо в ФСЭА, а это в свою очередь, означает, что число G, его код, входит во множество кодов выводимых теорем… Но позвольте-ка, ведь если это так, то в арифметике оказывается противоречие: получается, что число G и входит во множество кодов теорем, и не входит в него — результат получается разным в зависимости от пути формального вывода, которым мы идем.

Предположим теперь, что число G, код утверждения о том, что G не является кодом теоремы, и на самом деле не является кодом теоремы. В таком случае, противоречие снимается. Однако, в этом случае арифметика оказывается неполной! У нас есть верное утверждение (о том, что G не является кодом теоремы), которое, хоть и верное, но не входит в число теорем арифметики. Получается тогда, что арифметика «не знает» всех верных утверждений о натуральных числах.

Это рассуждение и является основным в первой теореме Геделя о неполноте. Формулировка этой теоремы была в дальнейшем значительно усилена Россером; когда говорят о теореме Геделя, имеют в виду обычно первую теорему о неполноте арифметики в формулировке Россера.

Обратите внимание, что такое замыкание нашего рассуждения возможно не в любой ФС. Например, утверждения системы ХИХИ не являются таковыми о натуральных числах; строку системы ХИХИ нельзя интерпретировать как «x не входит во множество Z», ведь у нас нет отображения этих строк на утверждения о числах. Кроме того, она не описывает и системы кодирования утверждений на языке, который она производит. Таким образом, ФС, попадающая под обсуждение теоремы Геделя, должна быть достаточно мощна, чтобы выражать, в некоей интерпретации смысла, действия элементарной арифметики. Системы, для которых такая интерпретация в принципе возможна, мы, вслед за Подниексом [2] назовем фундаментальными.

Давайте теперь проговорим суть вывода теоремы Геделя-Россера:

Фундаментальная система теорем, выводимых формальной системой, не может быть одновременно полной и непротиворечивой.

Этот вывод остается верным применительно к любой фундаментальной системе (то есть, с различными наборами аксиом и правил), не только к конкретной ФСЭА. Например, вполне естественно включить G в число аксиом нашей системы. Раз уж мы знаем, что утверждение G истинно, давайте добавим его к списку аксиом нашей ФСЭА. К сожалению, это не снимает противоречия. Сделав это, мы получим другую формальную систему, ФСЭА′, в которой, по теореме Геделя, есть свое геделево число G′. Можно и его добавить к аксиомам ФСЭА′ — мы получим новую систему ФСЭА′′, но и в ней будет свое геделево число G′′ — и так далее до бесконечности.

Разрешения у этой проблемы нет: арифметика не может быть полностью выражена набором аксиом и механических правил вывода, то есть и арифметика, как и теория множеств, не обосновывает сама себя. Открытие Геделя предопределило крах программы Гильберта по поиску самообоснованной, самосовершенной, заключенной самой в себе арифметики — и математики вообще.

Здесь можно увидеть некоторое сходство с геометрией. Изменяя пятый Евклидов постулат о том, что через заданную точку проходит ровно одна прямая, параллельная заданной прямой, мы получим разные непротиворечивые системы геометрии. Существенная разница в том, что геометрия, в отличие от арифметики, не порождает языка, на котором можно выразить аксиомы и правила геометрии. Тем не менее, общая картина арифметического состояния дел нам ясна: имеются некоторые истинные, в смысле более сложных, «внешних» теорий, утверждения, которые не могут быть ни доказаны, ни опровергнуты в арифметике. В то же время, эти внешние теории страдают тем же недостатком: в них имеются свои геделевы утверждения — и так, опять же, до бесконечности. Единой совершенной теории арифметики не существует. Есть более сильные фундаментальные теории и более слабые — например, аксиоматическая теория множеств ZFC сильнее аксиоматической арифметики Пеано в том смысле, что первая доказывает утверждения, недоказуемые в последней, но «абсолютной» фундаментальной теории все-таки существовать не может,

Стоит, для полноты картины, привести здесь, без доказательства или рассуждения, формулировку второй теоремы Геделя о неполноте арифметики:

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

Далее нам следует порассуждать о последствиях результатов, полученных Геделем, для математики, и лишь затем мы рассмотрим различные аргументы о применимости этих результатов к моделям и сущности сознания и мышления.

1  2   3   4  5  6  7
__________________________________
8. Множество аксиом ЭА счетно-бесконечно, они тоже выводятся правилами.

9. В ЭА рассматриваются натуральные числа, поэтому переменная может принимать значения 1, 2, 3 и так далее. Если x переменная, то (x+1) будет иметь значения 2, 3, 4 — иными словами, 2 или больше.

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

11. Парадокс, обнаруженный Бертраном Расселом в теории множеств, популярно сформулирован в википедии (англ.) так. Введем признак «нормальности»: нормальное множество не является своим собственным подмножеством. Например, множество всех квадратов нормально, потому что оно само не есть квадрат. Его дополнительное множество, множество всех неквадратов, не нормально, потому что оно само не квадрат и, следовательно, должно включать и себя. Теперь возьмем множество всех нормальных множеств, и зададимся вопросом, нормально оно или нет? Это парадокс. Если мы предположим, что оно нормально, то оно входит само в себя, и, следовательно, не нормально. Если предположить, что оно не нормально, то его не будет среди всех нормальных множеств, и, значит, оно не подмножество себя — то есть, нормально. Противоречие возникает при любом предположении.

12. Конструктивной в математическом смысле: требуется не только доказать существование алгоритма, доказывающего теоремы, но и отыскать сам этот алгоритм.

13. Бета-код Геделя основан на взаимно-простых числах и формулируется сложнее, но делает дальнейшие доказательства более эффективными. Для наших качественных рассуждений, однако, конкретный способ кодирования не важен.

14. Замечательное неформальное описание этого вывода дается в [1], глл. XIII и XIV, а формальный вывод в [2].

Tags:

Comments

( 27 comments — Leave a comment )
(Anonymous)
Dec. 18th, 2009 01:05 pm (UTC)
Спасибо, очень интересно
(Anonymous)
Dec. 18th, 2009 08:49 pm (UTC)
Спасибо за статью, интересно.

Правда 3 часть получилась гораздо сложнее для чтения, чем первые две. И хотелось бы еще более подробное объяснение (или хотя бы пример) какие системы могут быть фундаментальными, т.е. чем такие ФС отличаются от всех остальных.
fregimus
Dec. 19th, 2009 01:52 am (UTC)
Дальше будет проще. Здесь действительно сложные рассуждения, но это необходимо.

Фундаментальные системы. Для наших целей, система должна быть способна выразить теорию, в которую могут быть переведены ее правила, то есть вся манипуляция со строками, нужная, чтобы ФС «работала», могла бы быть проделана внутри ФС (пусть даже в отличающемся «коде» — тут строки, там числа, но это все равно, если они механически преобразуемы в обе стороны).

Подходят только те, которые могут по крайней мере выразить элементарную арифметику — четыре действия над натуральным числами. Есть доказательство, что ЭА действительно минимальная из фундаментальных систем.
yurvor
Dec. 19th, 2009 10:54 am (UTC)
"Что интересного произойдет, когда мы сделаем это? ФСЭА достаточно мощна, чтобы порождать язык арифметики. В тоже самое время, мы переписали ее правила на тот же самый язык! Иными словами, в таком выражении ФСЭА формулирует утверждения о себе."

Здесь есть дополнительная неясность. На каком основании мы причисляеи саму ФСЭА к ЭА? Если эта ФС описывает ЭА, но не входит в ЭА как объект, то никаких утверждений о самой себе она не формулирует.

fregimus
Dec. 19th, 2009 08:55 pm (UTC)
ФСЭА именно что становится, после кодирования, объектом ЭА. ФСЭА — алгоритм операций над строками. Путем арифметического кодирования, мы делаем ее алгоритмом операций над числами. ЭА содержит все алгоритмы операций над числами — включая, стало быть, и данный.
yurvor
Dec. 19th, 2009 09:54 pm (UTC)
Погоди, вопрос в другом. ФС ЭА - это действительно алгоритмы операций над строками. Но чтобы выразить что-то осмысленное об этой ФС, надо иметь её символ в самой ФС. Ну, чтобы закодировать утверждение "ФСЭА существует", в самой ФС должны быть символы для существования и для ФС самой. Вот этот последний символ - он откуда там внутри неё берётся?
fregimus
Dec. 20th, 2009 06:22 am (UTC)
Чтобы закодировать утверждение «существует бесконечно много простых чисел» (см пример), не требуется символов для «бесконечно много», «простого числа» или «бесконечного множества простых чисел». Комбинация логических утверждений, которая описывает данную ФС в арифметическом виде на языке ЭА, возможна. Не символ, а целое выражение. Боюсь, правда, подумать о ведрах чернил, потребных его записать.

justso123
Dec. 19th, 2009 01:22 pm (UTC)
Хотела сказать спасибо и за посты, и за рекомендацию: читаю Хофштадтера с огромным удовольствием (и это дошла примерно до середины, до мумзиков в мове)
fregimus
Dec. 19th, 2009 08:52 pm (UTC)
А Вам все понятным кажется (у меня, не у Хофштадтера, конечно)?

Хофштадтера по-английски читаете? Перевод я видел неплохой, но это одна из тех вещей, которые переводу вообще не поддаются, как мне кажется. Хуже «Финнегана».
justso123
Dec. 19th, 2009 09:22 pm (UTC)
Основное - точнее, то, что мне кажется основным (но все-таки это не первая математическая книжка, которую я читаю, даже если все остальные давно и прочно забыты). Читаю по-русски (как уж попалось), но перевод, насколько могу судить, неплохой, но все переводы не без греха. В предисловии к русскому изданию сам автор пишет, как он пытался перевести "Онегина" - там ведь тоже непереводимая игра намеков и аллюзий - а они и от русского-то читателя в оригинале ускользают. C математикой в этом смысле чуть проще. Кстати, забавно, что хороших популярных математических книг как-то больше, чем окологуманитарных - может, у гуманитариев другое отношение к своему предмету, а может, это у меня выборка смещенная.
gdt
Dec. 20th, 2009 02:22 pm (UTC)
фигово он "Онегина" перевел, говорят. впрочем, не удивительно.

> хороших популярных математических книг как-то больше, чем окологуманитарных
вы думаете? я бы так не сказал... но и противоположного тоже бы не сказал :)
gdt
Dec. 20th, 2009 02:27 pm (UTC)
хотелось бы глянуть на перевод (точнее, я видел книгу, но слишком уж мельком). многие диалоги Ахилла и Черепахи просто построены на игре слов, интересно, как их перевели (точнее, перевела -- как я читал, GEB переводила "babysitter'ша" Хофштадтера)
ext_206442
Dec. 21st, 2009 08:00 am (UTC)
да неплохо

вот там как пример из предисловия,

POPcorn - vitaskin==вытаскин
PUSHcorn - протолкин

соответственно

pushkin - про толкиена

:-)
andrey_bovykin
Dec. 20th, 2009 04:24 pm (UTC)
Я не согласен с предпоследним абзацем этого текста, начиная с предложения "Тем не менее, общая картина арифметического состояния дел нам ясна".

Трудно понять и двойственый пассаж про "истинные, но недоказуемые" утверждения.

Самые важные темы для размышлений в современной науки о недоказуемости такие:

1. арифметическая бифуркация (теории, чьи арифметические фрагменты противоречат друг другу)
2. степени непротиворечивости и два лагеря, по-разному рассуждающих о степенях непротиворечивости теорий (например о теориях, нe знающиx о непротиворечивости друг дружки)
3. комбинаторика (понимание таких вещей, как Парис-Харрингтон, БРТ и т.д.).

Практически, тема (1) - очень сложная, например доказать, что ZFC и NF противоречат друг дружке на арифметическом утверждении.

Тема (2) - доступна, но неизвестны естественные примеры, только диагонализационные извращения в стиле середины 20 века

Тема (3) - удивительная современная наука о недоказуемости, сотни интереснейших резулътатов о недоказуемости, и интересных явлений.
Программа Фридмана, Программа Вейерманна о фазовых переходах между доказуемостью и недоказуемостью, моя программка тоже движется.

Кстати, у меня в контакте есть группка про недоказуемость: http://vkontakte.ru/club338191 пока что театр одного актера, но надеюсь на интересные обсуждения.
fregimus
Dec. 20th, 2009 07:43 pm (UTC)
Истинные, но недоказуемые в некоей теории, конечно. Неаккуратно написал.

Я не сомневаюсь, что в этой области вглубь копают, хотя я и не слышал даже о большинстве вещей, что Вы упоминаете. Тут у меня тема другая: мне бы до сознания добраться, дурацкие тезисы изгонять, а то эта зараза уже и до наименее неприличных из научно-популярных мест добралась — «Элементов», например.

Думаю, что я Вам вряд ли смог бы помочь — уровень совершенно разный. Я тут могу с грехом пополам теорию 80-летней давности популярно изложить, но не более того.
andrey_bovykin
Dec. 20th, 2009 08:21 pm (UTC)
теорему Гёделя, в современном понимании, не "изложить", не понимая Париса-Харрингтона, Фридмана, фазовые переходы и, самое главное, всего спектра будущих (поке не реализованных) возможностей.

Можете посмотреть мои недоделки здесь:

http://www.maths.bris.ac.uk/~maaib/logic/

(но готово будет только следующим летом).

(Anonymous)
Dec. 21st, 2009 09:08 am (UTC)
Посмотрел, спасибо, исключительно интересно и почти все понятно (я не математик, но социально близкий). Жду завершения отделочных работ ;)
andrey_bovykin
Dec. 20th, 2009 08:23 pm (UTC)
я имею в виду в основном logic6.pdf

Надеюсь это всё станет классическим учебником, только дописать надо.
readership
Jan. 12th, 2010 03:49 am (UTC)
тут у меня возник вопросик, сорри за задержку.

= Гедель доказывает, что возможно (и показывает, как) сконструировать в ФСЭА утверждение...

сконструировать разве не означает вывести в ФСЭА?

А будущее противоречие снимается тем, что выражение "число G, код утверждения о том, что G не является кодом теоремы, и на самом деле не является кодом теоремы" означает, что изначально сконструированное утверждение просто не считается доказанной теоремой?

. В таком случае, противоречие снимается.

fregimus
Jan. 12th, 2010 06:23 am (UTC)
Речь идет не о том, как это утверждение вывести, а о том, как его закодировать в ФС. Вывести его можно только тогда, когда ФС противоречива: ведь если оно выводится — доказывается — то мы тем самым доказали, что его нельзя доказать, а это противоречие. С другой стороны, если оно невыводимо, то оно содержит верное утверждение об ФС — ведь G и в самом деле невыводимо — а, значит, наша ФС неполна.

изначально сконструированное утверждение просто не считается доказанной теоремой?
Не так «просто»: ведь оно еще и верное.
readership
Jan. 12th, 2010 09:27 am (UTC)
= Вывести его можно только тогда, когда ФС противоречива: ведь если оно выводится — доказывается — то мы тем самым доказали, что его нельзя доказать, а это противоречие. С другой стороны, если оно невыводимо, то оно содержит верное утверждение об ФС — ведь G и в самом деле невыводимо — а, значит, наша ФС неполна.

эта логика мне понятна.

=Речь идет не о том, как это утверждение вывести, а о том, как его закодировать в ФС.
=="изначально сконструированное утверждение просто не считается доказанной теоремой? "
=Не так «просто»: ведь оно еще и верное

а вот эта - не понятна. Получается, что мы волевым решением ранее выведенное утверждение считаем верным, но не считаем выведенным и закодированным ФС? то есть, буквально выводим его ЗА пределы ФС. так?

fregimus
Jan. 12th, 2010 11:21 am (UTC)
Мы не считаем его верным «волевым решением», нет. Строго говоря, из ТГ следует, что G верно (а оно утверждает, что G невыводимо в арифметике Т, вернее, что код G не принадлежит множеству кодов всех строк, выводимых в Т), только если Т непротиворечива. G кодируется в Т, разумеется, но не выводится в ней: например, мы можем закодировать 2×2=5 в арифметике, но не можем вывести (правда, в отличие от G, мы можем вывести отрицание этого утверждения, ~2×2=5).
readership
Jan. 12th, 2010 12:00 pm (UTC)
= Строго говоря, из ТГ следует, что G верно, только если Т непротиворечива.

Вот-вот, эту логику и пытаюсь ухватить. Получается, что у нас возникает формальное противоречие с утверждением G и мы его снимаем тем, что просто не признаем это противоречием! Считаем арифметику непротиворечивой и утверждению G приписываем значение "истинно". А действительно, истина же говорит не о форме, а о содержании утверждения. И только это содержание G мы признаем истинным, хотя формально вся запись выглядит "противоречиво".

Но если мы признали его истинным, то тем самым одновременно признали, что оно не является теоремой арифметики, хотя только что мы его формально построили в ФС. Итак, не всякая арифметическая истина принадлежит арифметике.

А игра на том, что истина содержательна...

Спасибо. хотя мне надо еще покрутить...
fregimus
Jan. 12th, 2010 06:54 pm (UTC)
«Получается, что у нас возникает формальное противоречие с утверждением G и мы его снимаем тем, что просто не признаем это противоречием!» — здесь нет более глубокого логического хода, нежели обычное доказательство от противного.

«не всякая арифметическая истина принадлежит арифметике.» — да, именно так. В интерпретации некоей большей теории, включающей данную, мы можем доказать истинность этого утверждения — но опять же если мы верим, что эта охватывающая теория непротиворечива. А оставаясь внутри формальной теории, не обращаясь к большей, доказать ее собственную непротиворечивости нельзя.
readership
Jan. 12th, 2010 07:28 pm (UTC)
= здесь нет более глубокого логического хода, нежели обычное доказательство от противного.

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

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

Фактически, мы дополняем или уточняем наш метаязык интерпретацией арифметики, при этом уточняя и ее саму (интерпретацию арифметики).

Вот так у меня вырисовывается. Но возможно, я еще не на должной глубине :)
zlyuk
May. 19th, 2010 05:48 pm (UTC)
наверное, немного глупо комментировть 5 месяцев спустя, но я только что набрёл на Ваш пост и не смог удержаться от нескольких мелочных придирок (формальности):
1. "13 простое число: не существует таких x и y, что (x+1)×(y+1)=13. Прибавление единицы требуется, чтобы каждый сомножитель был больше 2" должно быть "каждый сомножитель был не меньше 2"
2. в прим. 11, парадокс Рассела, "нормальность" должна определяться так, что нормальное множество не является своим собственным элементом (не подмножеством)
3. В формулировке тероемы Геделя-Россера (или определении фундаментальности) необходимо указать требование о рекурсивности набора аксиом, иначе она неверна. Согласно Вашему определению, например, полная и непротиворечивая теория, заданная как все высказывания истинные в стандартной модели арифметики является фундаментальной.
4. Совсем мелочное: в формулировке второй теоремы Геделя, первое "Если" - лишнее.
fregimus
May. 20th, 2010 02:35 am (UTC)
Спасибо, очень хорошо, что Вы вычитали и заметили!
( 27 comments — Leave a comment )