Полнота логики первого порядка

olish

Логика предикатов:
1) Логика первого порядка (исчисление предикатов) — формальное исчисление, ...
2) Логика первого порядка обладает рядом полезных свойств, которые делают ее очень привлекательной в качестве основного инструмента формализации математики. Главными из них являются полнота (это означает, что для любой формулы выводима либо она сама, либо ее отрицание) и непротиворечивость (ни одна формула не может быть выведена одновременно со своим отрицанием).
Формальное исчисление:
Теория называется полной, если в ней для любой формулы F выводима либо сама F, либо ее отрицание !F.
То есть в логике первого порядка для любой формулы F выводима либо сама F, либо ее отрицание !F ?
Как же быть, например, с такой формулой: \any x P(x на мой взгляд ни она, ни её отрицание не выводимы. Её отрицанием будет \exists x !P(x).
И вообще, кажется, что из полноты, как она тут описана, будет следовать то, что любая формула является либо общезначимой, либо противоречивой, что очевидно не верно.
Что я делаю не так?

vsjshnikova

Есть два понятия полноты - дедуктивная и семантическая. Дедуктивная - это когда для любой замкнутой формулы выводимо либо F, либо ¬F. Семантическая - это когда выводима любая формула, истинная в некотором классе интерпретаций.
Теорема о полноте утверждает как раз семантическую полноту: В логике первого порядка выводима любая общезначимая формула, т.е. формула, истинная в любой модели этой самой логики первого порядка.

vsjshnikova

Что я делаю не так?
Читаешь википедию, чтобы изучить какую-то область. Энциклопедии вообще для этого не предназначены.

pilaf4

Как же быть, например, с такой формулой: \any x P(x на мой взгляд ни она, ни её отрицание не выводимы. Её отрицанием будет \exists x !P(x).
не выводимы откуда? какие аксиомы у нас есть?

olish

> не выводимы откуда? какие аксиомы у нас есть?
Ниоткуда. Есть только законы логики предикатов.
А не выводимы, прежде всего, потому, что не общезначимы, для каждой из них можно привести пример интерпретации, в которой они не верны.
Для \any x P(x) таким примером будет "P - тождественно ложный предикат"
Для отрицания примером будет "P - тождественно истинный предикат"

Lokomotiv59

То есть в логике первого порядка для любой формулы F выводима либо сама F, либо ее отрицание !F ?
Нет. В логике первого порядка выводимы те и только те замкнутые формулы, которые являются общезначимыми, то есть истинными в любой интерпретации. Очевидно, что формула (\forall x P(x не общезначима, а значит, не выводима. То же самое верно и для ее отрицания.
PS. Мне кажется, что из приведенного следует лишь, что логика первого порядка (полная в определенном выше смысле будучи рассмотренная как формальная теория с пустым множеством аксиом, не является полной теорией.
Оставить комментарий
Имя или ник:
Комментарий: