Теорема о неполноте

[posic]

В ленте разные юзеры обсуждают теорему Геделя. Запишу-ка и я свое соображение на эту тему, оно вполне примитивное.

Я изучал это дело к экзамену по логике, и, натурально, тут же все забыл. Но у меня осталась идея, что трудность традиционных изложений связана по большей части с тем, что в них соединены два разных рассуждения -- собственно аргументы на основе self-reference и техника нумерации формул натуральными числами. Если изолировать эту технику в отдельный результат, все может оказаться гораздо более доступным.

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

После этого остается изолированное утверждение "формула n = 2^m выразима в языке арифметики Пеано", которое можно доказывать отдельно. С другой стороны, при наличии нумерации формул оставшаяся часть аргумента Геделя несложна. Я правильно понимаю?

Comments

[chaource.livejournal.com]

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

Перенумеровать всѣ утвержденія и потомъ доказать, что среди нихъ существуютъ недоказуемыя - ловкій трюкъ. Но не будетъ-ли такъ, что всѣ эти недоказуемыя утвержденія не имѣютъ большого значенія для науки?

[posic.livejournal.com]

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

Аналогичная ситуация с утверждениями. Утверждение "ZFC непротиворечива", рассматриваемое как утверждение из матлогики, очень интересно, недоказуемо средствами ZFC, и, насколько можно предположить, верно. Оно же, рассматриваемое как утверждение о натуральных числах, необычайно громоздко, неестественно и неинтересно.

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

Имеет ли теорема Геделя отношение к реальной работе математика? Короткий ответ на этот вопрос: в той же мере, в которой к ней имеет отношение любая другая математическая теорема. Например, к работе матлогика, изучающего формальные теории и аксиоматические системы -- имеет, и очень большое. К работе алгебраиста и аналитика -- скорее, разные неразрешимые вопросы теории множеств имеют небольшое отношение.

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

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

[avva.livejournal.com]

Примерно правильно. Нередко делают так, как вы предлагаете, только вместо конечных множеств используют арифметику с примитивной, т.е. бесплатной для использования, операцией возведения в степень. Есть несколько способов легко кодировать с помощью степени; например, если весь алфавит примитивных символов размером N, то каждую формулу можно прочитать просто как число в основании N.

А потом отдельно доказывают, что экспоненциация и ее аксиомы выразимы с помощью других символов и аксиом.

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

[posic.livejournal.com]

А как предполагать истинность всех аксиом, если речь идет о системе, более сильной, чем арифметика? Допустим, я хочу доказать, что непротиворечивость ZFC недоказуема средствами ZFC; истинность чего я должен предполагать, чтобы облегчить себе задачу?

[alexey-rom.livejournal.com]

По-моему, ещё проще заменить арифметику Пеано непосредственно на теорию конечных строк. Зачем кодировать формулы, если можно иметь их сами в качестве объектов теории?

[alexey-rom.livejournal.com]

Истинность ZFC в реальном мире множеств.

[posic.livejournal.com]

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

[avva.livejournal.com]

Нет такой возможности - у ZFC нет естественной модели (в том смысле, который тут необходим, как у PA есть модель N).

But that's OK, потому что в любом случае то док-во первой теоремы, которое предполагает истинность аксиом, не формализуется внутри самой системы (именно из-за непредставимости истинности), и не может поэтому помочь доказать вторую теорему, для которой эта формализуемость нужна.

Попросту говоря, есть два способа док-ть неполноту формальной системы:

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

2. Не предполагая истинность аксиом, а всего лишь их непротиворечивость. Заметно сложнее. Работает с системами сложнее арифметики, у которых нет естественной семантики и уверенности в истинности аксиом. Также работает с системами, у которых есть откровенно ложные аксиомы, бывает полезно. Не пересказывается интуитивно как парадокс лжеца, хотя все равно в общих чертах похоже. Требует значительно более тщательной арифметизации синтаксиса, в которой те или иные синтасические соотношения переводятся в арифметические утверждения, доказуемые из небольшого числа аксиом. Может быть формализовано внутри самой системы, и это необходимо для док-ва второй теоремы о неполноте.

[posic.livejournal.com]

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

[alexey-rom.livejournal.com]

Да, согласен -- в этом смысле она естественнее.

[flaass.livejournal.com]

Когда я разбирался для себя с теоремой Геделя, то всю механику кодирования просто объявил самоочевидной (сейчас это уже можно, все привыкли). Тогда и проявились основные трудности.
http://flaass.livejournal.com/tag/goedel

[nivanych.livejournal.com]

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