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

[epros]

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

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

Если так рассуждать, то, понятное дело, все аксиомы исчисления высказываний можно вывести (из таблиц значений логических функций $\neg$, $\rightarrow$, $\wedge$ и $\vee$). Но эти рассуждения основаны на априорном допущении, что мы знаем всё про "истинностные значения" и заведомо способны вычислить значение любой логической функции.

Наверное, конструктивисты с таким допущением не согласятся. Скажем, неочевидна вычислимость логической функции $\neg$: Допустим, $P$ соответствует недоказуемому и неопровержимому в арифметике предложению $\exists x \, \varphi(x)$. В стандартной модели арифметики мы можем считать $P$ ложным (не существует такого стандартного $x$, что...). Однако $\neg P$ недоказуемо в арифметике, т.е. мы не располагаем средствами вычислить правильное значение данного выражения (если считать, что все наши средства ограничены арифметикой), т.е. логическая функция отрицания оказывается "невычислимой".

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

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

Может быть. Но если теорема компактности формулируется таким образом, что из $T \models P$ следует, что существует конечное множество $\{A_1, \dots , A_n\}$ аксиом теории $T$ такое, что $\models A_1 \wedge \dots \wedge A_n \rightarrow P$, то, вроде бы, из $T \models P$ следует $\vdash A_1 \wedge \dots \wedge A_n \rightarrow P$, а значит и $T \vdash P$.

[AlexDem]

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

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

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

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

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

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

То есть мы всегда по умолчанию принимаем логику высказываний для определения истинности? Потому как если подходить формально, то характеристическую функцию истинности на множестве всех формул теории можно попытаться задать совершенно произвольно, положив, например $P \vee \neg P \equiv false$. А логика высказываний здесь - единственный возможный вариант?

[Xaositect]

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

[AlexDem]

Это не было замечание - просто вопрос, тема попалась подходящая. Я хотел уточнить, что такое "истинность формулы в модели", в принципе Вы ответили, спасибо...

[molokowoz]

Читая "Вычислимость и Логика"столкнулся с двумя понятиями:
1) Полнота теории - Теория наз-ся полной, если для любого предложения(в языке этой теории) А, либо А либо неА - теорема данной теории(т.е.выводима)
2) Полнота формализации логики первого порядка - существует процедура, устанавливающая общезначимость общезначимых предложений и если предложение общезначимо, то процедура непременно установит это.
Если рассматривать логику первого порядка как теория без собств аксиом - то связаны ли как нибудь эти понятия?

[epros]

molokowoz в сообщении #483041 писал(а):

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

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

[molokowoz]

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

-- 16.09.2011, 18:38 --

Я например связи не вижу, но меня очень смущает слово "полнота" и в одном случае и в другом.

[epros]

molokowoz в сообщении #483532 писал(а):

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

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

molokowoz в сообщении #483532 писал(а):

Я например связи не вижу, но меня очень смущает слово "полнота" и в одном случае и в другом.

Вроде бы полнота исчисления также означает существование в нём полной теории.

[molokowoz]

"Вроде бы полнота исчисления также означает существование в нём полной теории."

Можно здесь поподробнее. И опять же смущает слово "ВРОДЕ".


Прошу прощения, что цитировать не умею здесь.

[epros]

molokowoz в сообщении #483685 писал(а):

Можно здесь поподробнее. И опять же смущает слово "ВРОДЕ"

Это скорее не утверждение, а вопрос к общественности, так что подробнее не могу. "Вроде" по этой же причине.

[molokowoz]

Выяснил!) Это 2 разных понятия никак не связанных. По моему мнению, как минимум странно называть 2 разных понятия из одной области математики одним словом...Вызывает путанницу в еще не окрепших и во всём сомневающихся (таких как моя) головах студентов...

[epros]

molokowoz в сообщении #488470 писал(а):

Выяснил!) Это 2 разных понятия никак не связанных. По моему мнению, как минимум странно называть 2 разных понятия из одной области математики одним словом...Вызывает путанницу в еще не окрепших и во всём сомневающихся (таких как моя) головах студентов...

Неужели совсем никак? По-моему, это странно ... Насколько я знаю, существует "семантическое" понимание полноты теории, кое заключается в том, что всё "истинное" доказуемо в ней ("истинность", разумеется, определяется построением моделей). Это очень похоже на понимание полноты исчисления: всё "общезначимое" доказуемо в нём.

[molokowoz]

Действительно, семантическая полнота теории является следствием семантической полноты исчисления(по крайней мере в логике первого порядка - про другие логики ничего сказать не могу), а я говорил: "Полнота теории - Теория наз-ся полной, если для любого предложения(в языке этой теории) А, либо А либо неА - теорема данной теории." И пытался найти связь между этими понятиями.