2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 Полнота и неразрешимость исчисления предикатов
Сообщение18.07.2016, 22:49 
Заслуженный участник


08/04/08
8556
Как одновременно возможно, что исчисление предикатов полно, но неразрешимо?

С одной стороны, мы знаем, что исчисление предикатов (ИП) полно - любая общезначимая формула выводима из аксиом ИП.
С другой стороны, не ИП неразрешимо - не существует алгоритма, проверяющего истинность произвольной формулы ИП (даже предъявляется конкретная неразрешимая формула).
Возьмем теперь некоторую формулу $F$.
Если $F$ общезначима, то она выводима из аксиом ИП - можно устроить перебор всех выводов формул из аксиом ИП (упорядочить их по суммарной длине вывода, подстановки тоже перебирать).
Если же $F$ не общезначима, значит общезначимо ее отрицание $\neg F$, и значит $\neg F$ можно вывести перебором всех выводов из аксиом ИП.
Теперь мы можем взять и построить алгоритм вывода $F$ и $\neg F$ параллельно. Поскольку либо $F$, либо $\neg F$ общезначима, то для одной из этих формул алгоритм перебора выводов найдет доказательство, а значит он всегда завершается на любой $F$ и, таким образом, дает алгоритм разрешимости $F$, которого не существует по теореме Черча :shock:

Где я ошибаюсь?
Я не смогу перебрать счетное число переменных в правилах постановки?

 Профиль  
                  
 
 Re: Полнота и неразрешимость исчисления предикатов
Сообщение18.07.2016, 22:56 
Заслуженный участник
Аватара пользователя


16/07/14
8336
Цюрих
Sonic86 в сообщении #1138723 писал(а):
Если же $F$ не общезначима, значит общезначимо ее отрицание $\neg F$

Почему? Ни $\forall x P(x)$, ни $\neg \forall x P(x)$ не являются общезначимыми.

 Профиль  
                  
 
 Re: Полнота и неразрешимость исчисления предикатов
Сообщение18.07.2016, 23:04 
Заслуженный участник


08/04/08
8556
mihaild в сообщении #1138725 писал(а):
Sonic86 в сообщении #1138723 писал(а):
Если же $F$ не общезначима, значит общезначимо ее отрицание $\neg F$

Почему? Ни $\forall x P(x)$, ни $\neg \forall x P(x)$ не являются общезначимыми.
Да, действительно, мог бы сам догадаться, спасибо :-)

А если я возьму в качестве $F$ ту самую неразрешимую формулу? Она же общезначима? Или нет?
Или вообще буду брать только такие $F$, для которых либо $F$, либо $\neg F$ общезначимы? Тогда рассуждение сохраняется?

 Профиль  
                  
 
 Re: Полнота и неразрешимость исчисления предикатов
Сообщение19.07.2016, 00:12 
Заслуженный участник
Аватара пользователя


16/07/14
8336
Цюрих
Sonic86 в сообщении #1138728 писал(а):
А если я возьму в качестве $F$ ту самую неразрешимую формулу? Она же общезначима?

Нет, иначе она была бы выводима.

Sonic86 в сообщении #1138728 писал(а):
Или вообще буду брать только такие $F$, для которых либо $F$, либо $\neg F$ общезначимы? Тогда рассуждение сохраняется?

Вы получите, что множества общезначимых и тождественно ложных утверждений перечеслимы. Что вы хотите из этого получить?

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 4 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group