Теорема Лёба

[nikov]

Теорема Лёба гласит, что если в некоторой теории (в которой можно провести гёделеву нумерацию) доказуемо, что из доказуемости высказывания Ф следует Ф, то в ней доказуемо и само высказывание Ф. Следовательно, если в некоторой теории доказуемо, что для любого высказывания Ф из доказуемости Ф следует Ф, то в этой теории доказуемым будет любое высказывание, и она будет противоречивой.
Интересно, к каким практическим последствиям для математики это может привести? Если кто-то предъявит доказательство, что "Гипотеза Римана доказуема в ZFC", разве мы не будем после этого относиться к Гипотезе Римана, как к верному утвеждению?

[маткиб]

nikov в сообщении #167830 писал(а):

Интересно, к каким практическим последствиям для математики это может привести?

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

[nikov]

Хочу натренировать свою математическую интуицию, чтобы она подсказывала мне правильные вещи.
С первого взгляда кажется, что все доказуемые утверждения должны быть истинными. Но теорема Лёба говорит, что это возможно только в противоречивой теории. Значит ли это что в непротиворечивой теории будут доказуемые утверждения, не являющиеся истинными? Можно ли привести пример такого утверждения? Вот доказываешь-доказываешь теоремы, а они потом не истинными окажутся - обидно как-то.
Или я что-то не так понял?

[маткиб]

nikov в сообщении #167846 писал(а):

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

Теорема Лёба ничего такого не говорит. Можно смело считать, что все доказуемые в ZFC теоремы истинны в некоторой осмысленной вселенной множеств.

[nikov]

маткиб писал(а):

Теорема Лёба ничего такого не говорит. Можно смело считать, что все доказуемые в ZFC теоремы истинны в некоторой осмысленной вселенной множеств.

Тогда поясните, пожалуйста, что она говорит. Допустим, у нас есть некоторая недоказанная математическая гипотеза A (например, Гипотеза Римана). Некто предъявляет доказательство утверждения "гипотеза A доказуема в ZFC" (где, как положено, все закодировано с помощью гёделевской нумерации). Можем ли мы отсюда сделать вывод, что гипотеза A верна?

[маткиб]

nikov в сообщении #167869 писал(а):

Допустим, у нас есть некоторая недоказанная математическая гипотеза A (например, Гипотеза Римана). Некто предъявляет доказательство утверждения "гипотеза A доказуема в ZFC" (где, как положено, все закодировано с помощью гёделевской нумерации). Можем ли мы отсюда сделать вывод, что гипотеза A верна?

Можем. Кроме того, мы можем сделать вывод, что A реально имеет доказательство в ZFC. Это всё потому, что мы верим, что все доказуемые в ZFC утверждения являются в каком-то смысле истинными.

Но если доказателю разрешить пользоваться только ZFC, то, доказав доказуемость гипотезы A в ZFC, он ещё не доказал саму A. И он не может гарантировать, что A реально имеет доказательство в ZFC. Например, доказатель не может исключить такой случай, что ZFC непротиворечива, но (ZFC+"ZFC непротиворечива") противоречива, т.е., что в ZFC можно доказать доказуемость, например, 2+2=5, но реально такого доказательства для "2+2=5" не существует.

[AD]

Так, вот меня лично вы совсем запутали. Хотя я и так-то ничего не понимал ... То есть есть "доказуемость", "существование доказательства" ("выводимость"?), "истинность", ...

Короче, Карл Маркс и Фридрих Энгельс - это муж и жена или четыре разных человека?

Добавлено спустя 41 секунду:

Может, ссылочку какую-нибудь популярную дадите почитать, чтобы не позориться? Или учиться надо просто?

[nikov]

Кстати, я в русской википедии создал набросок статьи "Теорема Лёба". Прошу специалистов исправить и дополнить.

[маткиб]

AD в сообщении #167923 писал(а):

Так, вот меня лично вы совсем запутали. Хотя я и так-то ничего не понимал ... То есть есть "доказуемость", "существование доказательства" ("выводимость"?), "истинность", ...

Я бы скорее сказал так:
- можно задать какую-то интерпретацию I, тогда для формул можно ввести понятие истинности в этой интерпретации ($I\models A$);
- формула может быть доказуемой (выводимой) в теории, т.е. можно на бумажке выписать доказательство для этой формулы ($T\vdash A$);
- утверждение о доказуемости можно записать в виде формулы, используя гёделевскую нумерацию ($\mathrm{Prf}_T(A)$);
- можно говорить об истинности такой формулы ($I\models\mathrm{Prf}_T(A)$);
- можно говорить о доказуемости такой формулы ($T\vdash\mathrm{Prf}_T(A)$), это уже будет доказуемость доказуемости;
- это тоже можно записать в виде формулы ($\mathrm{Prf}_T(\mathrm{Prf}_T(A))$);
и т.д.
Ссылочки есть в соседней теме.

[Someone]

Я немного дополню. Предположим, у нас есть некая формальная теория $T$, сформулированная в языке первого порядка (например, арифметика или теория множеств). Высказывания такой теории говорят об объектах теории $T$. Поскольку алфавит, термы, высказывания и доказательства теории $T$ не являются её объектами, теория $T$ ничего не может сказать о доказуемости или недоказуемости какого-либо своего высказывания. Это невозможно никак сформулировать, оставаясь в рамках теории $T$. То же самое - с истинностью. Истинность конкретного высказывания может зависеть от интерпретации (модели) теории. Корректной интерпретацией нужно считать такую, в которой все аксиомы теории (как логические, так и математические) истинны, а правила вывода преобразуют истинные высказывания в истинные.
Что имеется в виду, когда говорят, что "достаточно богатая теория не может доказать свою непротиворечивость"? В теории $T$ вообще невозможно сформулировать утверждение о её непротиворечивости, поэтому указанное высказывание выглядит бессмысленным.

Однако Гёдель придумал очень хитрый фокус.
Для описания языка теории $T$ используется некоторая другая теория $S$ (не обязательно формальная), которая называется метатеорией. Алфавит, термы, высказывания и доказательства теории $T$ являются объектами теории $S$, и в $S$ мы можем формулировать утверждения о доказуемости высказываний теории $T$, о её непротиворечивости и так далее. Если теория $T$ "достаточно богата" (а арифметика Пеано оказывается "достаточно богатой"), то мы можем средствами метатеории закодировать алфавит, термы, высказывания и доказательства теории $T$ объектами этой теории и превратить метатеоретические высказывания о доказуемости, непротиворечивости и так далее в высказывания теории $T$ об этих кодах.

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

Вообще, перемешивание теории и метатеории - страшный грех, быстро приводящий к полной путанице и противоречиям.

[epros]

маткиб писал(а):

Но если доказателю разрешить пользоваться только ZFC, то, доказав доказуемость гипотезы A в ZFC, он ещё не доказал саму A. И он не может гарантировать, что A реально имеет доказательство в ZFC.

Звучит как какой-то абсурд. Существование доказательства доказано, но что оно "реально существует" мы утверждать не можем??

По-моему, если мы способны утверждать подобные вещи, то у нас что-то не так с метатеорией. А точнее, та метатеория, в которой мы рассуждаем о теориях, сама по себе противоречива, т.е. в ней можно утверждать всё, что угодно, в том числе и то, что существование доказательства не означает его "реального" существования.

[маткиб]

epros в сообщении #168392 писал(а):

Звучит как какой-то абсурд. Существование доказательства доказано, но что оно "реально существует" мы утверждать не можем??

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

epros в сообщении #168392 писал(а):

По-моему, если мы способны утверждать подобные вещи, то у нас что-то не так с метатеорией. А точнее, та метатеория, в которой мы рассуждаем о теориях, сама по себе противоречива, т.е. в ней можно утверждать всё, что угодно, в том числе и то, что существование доказательства не означает его "реального" существования.

Метатеория тут не причём. Пример я уже приводил (опираясь на незамысловатое предположение о вменяемости ZFC) в соседней теме: T=ZFC+"ZFC противоречива". В этой теории можно доказать (т.е. непосредственно выписать доказательство на бумажке): "в T существует доказательство, что 2+2=5", но нельзя доказать "2+2=5".

[nikov]

маткиб писал(а):

В этой теории ... нельзя доказать "2+2=5".

А вот это спорный вопрос.

Добавлено спустя 13 минут 25 секунд:

маткиб писал(а):

Пример я уже приводил (опираясь на незамысловатое предположение о вменяемости ZFC) в соседней теме: T=ZFC+"ZFC противоречива". В этой теории можно доказать (т.е. непосредственно выписать доказательство на бумажке): "в T существует доказательство, что 2+2=5"

Но ведь это будет значить, что данная система по крайней мере не $\omega$-consistent, правда? Потому что она утверждает, что существует число, которое является номером доказательства ее противоречивости, хотя такого числа нет (если она действительно consistent).

[маткиб]

nikov писал(а):

маткиб писал(а):

В этой теории ... нельзя доказать "2+2=5".

А вот это спорный вопрос.

Да уж, на эту тему любят иногда поспорить. Хотя я бы сказал, что он не спорный, а требующий осмысления.

nikov писал(а):

Но ведь это будет значить, что данная система по крайней мере не $\omega$-consistent, правда?

Правда.

[epros]

маткиб писал(а):

epros в сообщении #168392 писал(а):

Звучит как какой-то абсурд. Существование доказательства доказано, но что оно "реально существует" мы утверждать не можем??

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

Я ведь всего лишь "грамматически проанализировал" Вашу фразу. Речи о конструктивности или неконструктивности не было. Вы с одной стороны сказали, что доказуемость (т.е. существование доказательства) доказана, а с другой стороны сказали, что при этом нельзя гарантировать то, что доказательство "реально имеется".

Давайте уж остановимся на чем-то одном:
1. Либо Вы признаёте неконструктивные доказательства, и тогда, неконструктивно доказав, что "доказательство существует", Вы можете быть уверены, что доказательство "реально имеется".
2. Либо Вы признаёте только конструктивные доказательства, и тогда Вы можете быть уверены в том, что доказательство "реально имеется" только после того, как продемонстрируете способ его построения.

Т.е. варианта, когда Вы неконструктивно "доказали доказуемость", но при этом высказывание осталось недоказанным, быть не может - это просто эклектическое смешение разных подходов.

маткиб писал(а):

Метатеория тут не причём. Пример я уже приводил (опираясь на незамысловатое предположение о вменяемости ZFC) в соседней теме: T=ZFC+"ZFC противоречива". В этой теории можно доказать (т.е. непосредственно выписать доказательство на бумажке): "в T существует доказательство, что 2+2=5", но нельзя доказать "2+2=5".

Мне этот пример пока непонятен. Я понимаю, что высказывание "ZFC противоречива" можно арифметизировать по Гёделю, а потом получившееся арифметическое выражение добавить к ZFC в качестве новой аксиомы. Но мне не очевидно, что в итоге мы получим противоречивую теорию (в смысле $(\exists S \in T)((T \vdash S) \wedge (T \vdash \neg S))$, откуда следует доказуемость 2+2=5).