Теорема Гёделя о полноте

[epros]

Заранее извиняюсь за тупой вопрос, но может быть кто-нибудь растолкует мне смысл сабжа?

На первый взгляд, те формулировки, которые на слуху, кажутся понятными: "Исчисление предикатов первого порядка полно". Что такое полнота теории - принципиальных вопросов не вызывает: это когда теория доказывает или опровергает любое предложение своего языка. Но заглянув сюда видим, что исчисление предикатов первого порядка, собственно говоря, не совсем теория. Чтобы получился конкретный язык, в котором можно формулировать "предложения языка", нужно определить хотя бы один функциональный или предикатный символ: Иначе мы не сможем составить ни одного терма, ни одной формулы, а стало быть - и ни одного предложения. Вот в языке арифметики Пеано: функциональные символы - "0", "S", "+", "*", а предикатный - только "=". Но арифметика Пеано, как это известно из другой теоремы того же Гёделя, неполна. И не станет полной, каких бы аксиом мы к ней ни добавляли. Или другой пример: вроде бы доказано, что неполна любая теория, сформулированная в языке исчисления предикатов первого порядка, в котором помимо предиката "=" определён ещё хотя бы один предикатный символ (по этой причине неполны будут любые варианты теории множеств - т.е. использующие предикатый символ $\in$).

О полноте чего же тогда идёт речь? Я слышал ещё такой вариант формулировки: "Существует полная теория, формализуемая в языке исчисления предикатов первого порядка". Действительно, есть пример: т.н. арифметика Пресбургера - в её языке нет символа "*", в результате чего произведение оказывается в такой теории невыразимым, зато сама теория - полной, т.е. она доказывает или опровергает любое предложение соответствующего языка. Но в чём тогда глубокий смысл такой теоремы о полноте? Утверждается, что теорема о полноте "устанавливает фундаментальную эквивалентность понятий доказуемости и общезначимости" (из той же статьи википедии). С понятием доказуемости всё ясно, но причем тут общезначимость? Если я правильно понимаю, общезначимость (logical validity?) утверждения означает, что оно верно в любой "модели" ... э-эээ ... модели чего? Если речь о модели теории (например, арифметики Пресбургера), то понятно, что любая её теорема должна быть верна в любой модели теории (иначе это не модель этой теории по определению). Очевидно, что для полной теории имеется эквивалентность между доказуемостью и общезначимостью (в таком смысле), ибо всё недоказуемое - опровержимо, а стало быть - ложно в любой модели. Но каков глубокий смысл в этой "общезначимости" (и в её эквивалентности доказуемости) с учётом того, что в исчислении предикатов первого порядка могут формализовываться и неполные теории?

[mkot]

А вы аккуратно сформулируйте, что такое
(1) теория,
(2) исчисление предикатов,
(3) общезначимость,
(4) выводимость,
(3) полнота теории,
(4) полнота исчисления предикатов
и всё встанет на свои места.

(Оффтоп)

и 'туда' не заглядывайте =) Возьмите Верещагина-Шеня или Мендельсона.

[epros]

mkot, нумерация пунктов меня несколько озадачила. Будем считать, что последние два - это (5) и (6)?

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

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

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

(3) Самое загадочное для меня понятие. Как я понял, общезначимо то, что верно в любой модели. Как это применимо к исчислению предикатов самому по себе - непонятно. Я пойму, если Вы приведёте пример какого-нибудь общезначимого предложения. Скажем, $\forall x (x=x)$ - вроде бы "общезначимо", но это - не предложение исчисления предикатов "самого по себе", это - предложение языка некоторой теории, в котором определена переменная $x$ (про предикатный символ равенства я уж и не говорю - предполагая, что мы договоримся считать отношение равенства неотъемлемой частью исчисления предикатов).

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

(5) = выводимость в теории любого предложения её языка или его отрицания. Иногда говорят: "выводимость всех истинных предложений языка", однако понятие "истинности" является внешним по отношению к рассматриваемой теории, поэтому я не считаю правильным его привлекать.

(6) В этом и весь вопрос. Если мы считаем, что исчисление предикатов - не просто "набор правил по формализации теорий", а некий язык в законченной форме + аксиоматика, то, разумеется, его можно считать "теорией" и применять к нему понятие полноты. Только тогда возникают вопросы:
А) Какова именно эта "теория"? Например, может быть мы должны считать, что в исчислении предикатов "самом по себе" определена строго одна переменная $x$ (не больше и не меньше)? Или мы должны считать, что определено бесконечное количество преременных $x_1, x_2, \dots$? А может быть мы должны считать, что определено бесконечное множество нуль-арных функциональных символов (констант) $c_1, c_2, \dots$?
Б) Каков смысл в полноте этой куцей "теории"? Если речь идёт о том, что только те тривиальные предложения, которые мы сможем сформулировать в этом языке, типа $\forall x (x=x)$, являются доказуемыми или опровержимыми, то я не вижу в такой полноте никакой особой ценности. В полноте арифметики Пресбургера ценности поболее, ибо её язык всё же побогаче.

[mkot]

ОК, хорошо, я понял в чём проблема, кажись.

Будем отталкиваться от того, что у вас написано. То что написано в (1) и (2) объединим и назовём теорией (первого порядка). Заметим, что аксиомы теории состоят как из логических аксиом, так и из собственных аксиом теории. При этом важно отметить, что в самом начале фиксируется сигнатура, только потом можно говорить про какие либо формулы и теории. Теперь если собственные аксиомы теории отсутствуют и получается то, что называется исчислением предикатов первого порядка. Тогда становится удобно говорить что теория это исчисление предикатов + собственные аксиомы теории. И тогда понятно почему собственное множество аксиом тоже называют теорией.

(3) Общезначимость. Вы не правы, $\forall x \, x = x $ -- не общезначима. Так как она должна быть истинна на любой модели (про нормальные модели молчим пока), а $=$ -- это просто бинарный предикатный символ, его можете интерпретировать как $=$, как $<$, как $>$, как $\not{=}$, ... вообще любым бинарным отношением заданным на носителе.

А общезначимой формулой будет, например, $\forall x \, ((x = x) \vee \neg (x = x)) $, $(\forall x \, x = x) \to (\exists x \, x = x)$, и так далее. Это понятие нужно для установления свойств кванторов и логических связок, а не для символов сигнатуры.

Что такое выводимость вам понятно. Так вот важный факт -- корректность исчисления предикатов -- любая выводимая в исчислении предикатов формула является общезначимой.
Что и записывается в виде
$\vdash \varphi \; \Rightarrow \; \models \varphi$.
Заметьте, здесь пока что нет собственных аксиом теории.

Теперь пусть есть собственные аксиомы теории $T$ (можно мыслить $T$ и как обозначение теории и как обозначение множества аксиом теории). В этом случае также имеется теорема о корректности, которая утверждает, что всякая выводимая в теории $T$ формула, истинна на любой модели теории $T$, что и записывается в виде
$T \vdash \varphi \; \Rightarrow \; T\models \varphi$.
Заметьте отличие от предыдущей теоремы, там общезначимость, то есть истинность на _любой_ модели, а здесь истинность на моделях теории. Вернёмся к вашему примеру $\forall x \, x = x$, рассмотрим теперь теорию равенства, то есть аксиомы (то есть предложения) которые говорят, что значок $=$ обладает привычными на свойствами (в любой книге их найдёте). Тогда
это формула будет истинной на любых моделях в которых равенство проинтерпретировано естественным образом.

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

Теперь перейдём к полноте теории.
Как вы правильно сказали, что теория полна, если для любой формулы, выводится либо она сама, либо её отрицание.

Простой содержательный пример неполной теории -- теория групп. Так как существуют коммутативные и некоммутативные группы.

Другими словами теория полна, если про любое предложение можно сказать, истинно оно или ложно.

А что такое полнота исчисления предикатов? Это утверждение о том, что любая общезначимая формула выводима в исчислении предикатов, то есть
$\models \varphi \; \Rightarrow \; \vdash \varphi$
То есть вывести мы можем всё, что истинно всегда и везде.
Или сильная форма утверждения о полноте исчисления предикатов (когда добавляются аксиомы теории)
$T \models \varphi \; \Rightarrow \; T\vdash \varphi$.

Таким образом собрав всё вместе и немножко допустив вольность речи понимаем что это разные понятия:
(1) Полнота теории -- это значит что для любой формулы мы можем установить истинна она или ложна на любых моделях этой теории. (то есть про все формулы можно что-то сказать.)
(2) Полнота исчисления предикатов -- всё что истинно на моделях можно вывести. (то есть меньше не получилось).

Спасибо. Вопросы?

(а с нумерацией я прокосячил, сначала хотел о четырёх вещах спросить.)

[arseniiv]

(То, что внутри, совершенно не относится к теме)

mkot в сообщении #377088 писал(а):

$\not{=}$

Может, вы хотели сказать $\ne$?

[epros]

mkot, рассказанное Вами сейчас не новость для меня, но не снимает вопроса.

mkot в сообщении #377088 писал(а):

И тогда понятно почему собственное множество аксиом тоже называют теорией.

Как раз непонятно, ибо:

mkot в сообщении #377088 писал(а):

в самом начале фиксируется сигнатура, только потом можно говорить про какие либо формулы и теории

А какова она, сигнатура "чистого" исчисления предикатов? Чтобы построить хотя бы одну формулу, нужно иметь хотя бы один предикатный символ. А они у нас есть? Поэтому и возник мой вопрос: О полноте чего говорит теорема?

mkot в сообщении #377088 писал(а):

$\forall x \, x=x$ -- не общезначима

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

mkot в сообщении #377088 писал(а):

А общезначимой формулой будет, например, $\forall x \, ((x = x) \vee \neg (x = x)) $, $(\forall x \, x = x) \to (\exists x \, x = x)$, и так далее.

Опять остаются те же вопросы:
- Откуда взято, что в языке "чистого" исчисления предикатов есть предикатный символ "="?
- Откуда взято, что в языке "чистого" исчисления предикатов есть символ переменной "x"?

Подобных тавтологий я могу записать сколько угодно. Например, $p \rightarrow p$ тоже общезначимо, поскольку должно быть верно для любого $p$. Только вот есть ли у нас в языке "чистого" исчисления предикатов нуль-арный предикатный символ "p"?

Т.е. возвращаемся к вопросу: В чём именно заключается "чистое" исчисление предикатов, о полноте которого говорит теорема?

mkot в сообщении #377088 писал(а):

А что такое полнота исчисления предикатов? Это утверждение о том, что любая общезначимая формула выводима в исчислении предикатов, то есть
$\models \varphi \; \Rightarrow \; \vdash \varphi$
То есть вывести мы можем всё, что истинно всегда и везде.

С формулой всё понятно, она всего лишь говорит о том, что всё, истинное из каких-то "высших" соображений, доказуемо. Непонятно только к чему её применять, ибо непонятно какие предложения есть в языке, а какие появятся только после того, как мы определим сигнатуру прикладной теории. Например, вот такое предложение есть ли в языке:
$\forall x,y \, (\forall z \, (z \in x \rightarrow z \in y) \wedge (z \in y \rightarrow z \in x)) \rightarrow x=y$?
Наверное нет, ибо символ $\in$ определяется только на уровне конкретной теории. А символы $=$, $x$, $y$, $z$ заранее определены в рамках самого исчисления предикатов? Или нет?

mkot в сообщении #377088 писал(а):

$T \models \varphi \; \Rightarrow \; T\vdash \varphi$
...
Полнота исчисления предикатов -- всё что истинно на моделях можно вывести

Вот такая формулировка теоремы интересна. Правильно ли я понимаю, что она относится не только к полным теориям? Т.е. то самое истинное, но недоказуемое в арифметике Пеано предложение не является "истинным на всех моделях"? А в каком же смысле тогда оно истинно?

[Профессор Снэйп]

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

Многабукафф не читал...

[mkot]

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

А какова она, сигнатура "чистого" исчисления предикатов? Чтобы построить хотя бы одну формулу, нужно иметь хотя бы один предикатный символ. А они у нас есть? Поэтому и возник мой вопрос: О полноте чего говорит теорема?

Ответ 'какая угодно' устроит? Возьмите сигнатуру $\{{=},{<}, {+}\}$, возьмите просто $\{{=}\}$. Главное какую-то зафиксировать. (Как правильно замечено хоть один предикат нужен, чтоб что-то получить) А потом по этой сигнатуре определяем множество формул. И дальше уже определяем вывод и всё что хотите.

Ведь заметьте, мы говорим 'формула истинна в некоторой модели', мы употребили слово модель. А что такое модель? Это множество-носитель $A$ плюс функция интерпретации, которая каждому функциональному символу $f$ ставит в соответствие функцию из$A^{n_f} \to A$, каждому предикатному -- подможество $A^{n_P}$, каждому константному -- элемент носителя.

Так что теорема о полноте говорит о произвольной выбранной (но фиксированной) сигнатуре.

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

- Откуда взято, что в языке "чистого" исчисления предикатов есть предикатный символ "="?
- Откуда взято, что в языке "чистого" исчисления предикатов есть символ переменной "x"?

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

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

$T \models \varphi \; \Rightarrow \; T\vdash \varphi$
...
Полнота исчисления предикатов -- всё что истинно на моделях можно вывести
Вот такая формулировка теоремы интересна. Правильно ли я понимаю, что она относится не только к полным теориям? Т.е. то самое истинное, но недоказуемое в арифметике Пеано предложение не является "истинным на всех моделях"?

Да, она относится к любым теориям.
Да, если некоторая теория не полна, то есть найдётся предложение, которое не выводится из аксиом, то найдутся модели на которых оно ложно и на которых оно истинно.

[Xaositect]

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

Т.е. то самое истинное, но недоказуемое в арифметике Пеано предложение не является "истинным на всех моделях"? А в каком же смысле тогда оно истинно?

Не является. Оно истинно в том смысле, что оно истинно в стандартной модели арифметики.

[epros]

mkot в сообщении #377510 писал(а):

Ответ 'какая угодно' устроит?

Да, устроит, спасибо. Следующая формулировка:

mkot в сообщении #377088 писал(а):

$T \models \varphi \; \Rightarrow \; T\vdash \varphi$

(применительно к любой теории $T$ и любому предложению в её языке $\varphi$) понятна.

Хотелось бы ещё осмыслить, почему этой теореме придают такое большое значение. Вот, для логики второго порядка, вроде бы, аналогичной теоремы нет. Т.е. в теории второго порядка $T$ может существовать верная во всех её моделях, но недоказуемая в ней формула? Чем это так уж хуже существования недоказуемой и неопровержимой формулы в теории первого порядка?

(Пояснение к происхождению вопросов)

У меня эти вопросы возникают потому, что я не очень хорошо пониманию идеологической важности понятия "общезначимости" (в смысле "верности в любых моделях теории"). Алгоритмическая разрешимость - понимаю, важна. Доказуемость - тоже можно понять, важна. А общезначимость - это зачем? Модель - сама по себе очень мутное понятие, сначала нужно убедиться, что она существует, потом - ухитриться доказать, что нечто в ней истинно (что наверняка не проще прямого доказательства в теории)... А потом ещё и ухитриться доказать, что оно истинно вообще в любой модели?

Xaositect в сообщении #377512 писал(а):

Оно истинно в том смысле, что оно истинно в стандартной модели арифметики.

Понятно, я примерно так и предполагал. Понять бы ещё, что даёт нам основания именовать модель "стандартной"... Вот, скажем, есть у нас некая арифметическая формула $\varphi(x)$, такая, что предложение $\exists x \, \varphi(x)$ недоказуемо, но и неопровержимо. Как я понимаю, это значит, что нет такого числа $n$ (терма вида $S(\dots S(0)\dots)$), которое, будучи подставленным в формулу, даст доказуемое предложение. В определённом смысле это позволяет нам считать, что такого числа и не существует, т.е. истинно: $\nexists x \, \varphi(x)$. Однако в самой теории последнее предложение тоже недоказуемо... Поэтому мы можем добавить в теорию аксиому о существовании такового числа: $\exists x \, \varphi(x)$. Правильно ли я понимаю, что:
1) То число, существование которого мы сейчас утверждаем, является "нестандартным"? Т.е. это нечто, невыразимое конечным термом вида $S(\dots S(0)\dots)$?
2) Получившаяся теория с дополнительной аксиомой будет $\omega$-противоречивой?

-- Пн ноя 22, 2010 12:15:56 --

Кстати, а почему из $\models \varphi \; \Rightarrow \; \vdash \varphi$ (верное на всех моделях данной сигнатуры доказуемо в исчислении предикатов) выводится $T \models \varphi \; \Rightarrow \; T \vdash \varphi$ (верное на всех моделях теории доказуемо в ней)?

[mkot]

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

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

Общезначимость -- это аналог тавтологии из логики высказываний. Считаете ли вы тавтологии идеологически важными?

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

Кстати, а почему из $\models \varphi \; \Rightarrow \; \vdash \varphi$ (верное на всех моделях данной сигнатуры доказуемо в исчислении предикатов) выводится $T \models \varphi \; \Rightarrow \; T \vdash \varphi$ (верное на всех моделях теории доказуемо в ней)?

А выводится ли вообще? Не соображу. Эти утверждения получаются из такой теоремы, которую тоже иногда называют теоремой о полноте: любая непротиворечивая теория совместна.

[epros]

mkot в сообщении #379048 писал(а):

Общезначимость -- это аналог тавтологии из логики высказываний. Считаете ли вы тавтологии идеологически важными?

Тавтологии я считаю идеологически важными. Но это потому, что они доказуемы (без прикладных аксиом). А общезначимость, как я понял, изначально определяется независимо от доказуемости, и только теорема о полноте позволяет утверждать, что это одно и то же. Т.е. если теоремы о полноте нет (пример - логика второго порядка), то, вообще говоря, общезначимость $\ne$ доказуемости. И что это за общезначимость такая без доказуемости? Говорят, что общезначимость - это "про семантику", в то время как доказуемость - "про синтаксис". Что это за семантика такая, откуда мы её возьмём? Как я понимаю, если предложение общезначимо, но недоказуемо, то мы просто не узнаем о том, что оно общезначимо...

mkot в сообщении #379048 писал(а):

А выводится ли вообще? Не соображу. Эти утверждения получаются из такой теоремы, которую тоже иногда называют теоремой о полноте: любая непротиворечивая теория совместна.

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

[Xaositect]

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

mkot в сообщении #379048 писал(а):

Общезначимость -- это аналог тавтологии из логики высказываний. Считаете ли вы тавтологии идеологически важными?

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

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

Цитата:

mkot в сообщении #379048 писал(а):

А выводится ли вообще? Не соображу. Эти утверждения получаются из такой теоремы, которую тоже иногда называют теоремой о полноте: любая непротиворечивая теория совместна.

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

Как минимум, это сразу переносится на конечно-аксиоматизируемые теории, потому что $T\models P \Leftrightarrow \models (A_1\& A_2\&\dots \&A_n\to P)$

[epros]

Xaositect в сообщении #379447 писал(а):

Тавтология изначально определяется тоже независимо от доказуемости. Тавтология - это тождественно истинная формула

Хм, не могу я постичь смысл этого заявления. Что значит "тождественно истинная формула" (в "семантическом" смысле, т.е. без ссылок на доказуемость)? Вот $P \vee \neg P$ - это тождественно истинная формула? Если у нас есть соответствующая "логическая аксиома", то да. А если я, скажем, конструктивист и в моей версии исчисления высказываний такой "логической аксиомы" нет? Насколько я понимаю, ниоткуда свыше ("из семантики"?) она тогда и не возьмётся. А апелляция к "логической аксиоме" - это как раз ссылка на доказуемость.

Xaositect в сообщении #379447 писал(а):

Как минимум, это сразу переносится на конечно-аксиоматизируемые теории, потому что $T\models P \Leftrightarrow \models (A_1\& A_2\&\dots \&A_n\to P)$

Ага, точно. А для бесконечно-аксиоматизируемых, как я понял, можно применить теорему компактности?

[Xaositect]

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

Xaositect в сообщении #379447 писал(а):

Тавтология изначально определяется тоже независимо от доказуемости. Тавтология - это тождественно истинная формула

Хм, не могу я постичь смысл этого заявления. Что значит "тождественно истинная формула" (в "семантическом" смысле, т.е. без ссылок на доказуемость)? Вот $P \vee \neg P$ - это тождественно истинная формула? Если у нас есть соответствующая "логическая аксиома", то да. А если я, скажем, конструктивист и в моей версии исчисления высказываний такой "логической аксиомы" нет? Насколько я понимаю, ниоткуда свыше ("из семантики"?) она тогда и не возьмётся. А апелляция к "логической аксиоме" - это как раз ссылка на доказуемость.

Переменным приписываются истинностные значения, а формула интерпретируется как функция от этих значений. Если эта функция всегда принимает некоторое выделенное значение "истина", то формула - тавтология.

-- Вт ноя 23, 2010 12:34:42 --

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

Ага, точно. А для бесконечно-аксиоматизируемых, как я понял, можно применить теорему компактности?

Что-то мне кажется, что не все так просто.