Логика первого порядка

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

Основные определения[править | править вики-текст]

Язык логики первого порядка строится на основе сигнатуры, состоящей из множества функциональных символов \mathcal{F} и множества предикатных символов \mathcal{P}. С каждым функциональным и предикатным символом связана арность, то есть число возможных аргументов. Допускаются как функциональные, так и предикатные символы арности 0. Первые иногда выделяют в отдельное множество констант. Кроме того, используются следующие дополнительные символы:

  • символы переменных (обычно \! x, \! y, \! z, \! x_1, \! y_1, \! z_1, \! x_2, \! y_2, \! z_2 и т. д.);
  • пропозициональные связки:
Символ Значение
\neg Отрицание («не»)
\land Коньюнкция («и»)
\lor Дизъюнкция («или»)
\to Импликация («если ..., то ...»)
Символ Значение
\forall Квантор всеобщности
\exists Квантор существования

Перечисленные символы вместе с символами из \mathcal{P} и \mathcal{F} образуют алфавит логики первого порядка. Более сложные конструкции определяются индуктивно.

  • Терм есть символ переменной, либо имеет вид f( t_1, \ldots, t_n ), где \! f — функциональный символ арности \! n, а t_1, \ldots, t_n — термы.
  • Атом имеет вид p( t_1, \ldots, t_n ), где \! p — предикатный символ арности \! n, а t_1, \ldots, t_n — термы.
  • Формула — это либо атом, либо одна из следующих конструкций: \neg F, F_1\lor F_2, F_1\land F_2, F_1\to F_2, \forall x F, \exists x F, где \! F, F_1, F_2 — формулы, а \! x — переменная.

Переменная \! x называется связанной в формуле \! F, если \! F имеет вид \forall x G либо \exists x G, или же представима в одной из форм \neg H, F_1\lor F_2, F_1\land F_2, F_1\to F_2, причём \! x уже связана в \! H, \! F_1 и \! F_2. Если \! x не связана в \! F, её называют свободной в \! F. Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

Аксиоматика и доказательство формул[править | править вики-текст]

Система логических аксиом логики первого порядка состоит из аксиом исчисления высказываний дополненной двумя новыми аксиомами:

  • \forall x A \to A[t/x],
  • A[t/x] \to \exists x A,

где \! A[t/x] — формула, полученная в результате подстановки терма \! t вместо каждой свободной переменной \! x, встречающейся в формуле \! A.

Правил вывода 2:

Интерпретация[править | править вики-текст]

В классическом случае интерпретация формул логики первого порядка задается на модели первого порядка, которая определяется следующими данными

  • Несущее множество \mathcal{D},
  • Семантическая функция \sigma, отображающая
    • каждый n-арный функциональный символ f из \mathcal{F} в n-арную функцию \sigma(f):\mathcal{D}\times\ldots\times\mathcal{D}\rightarrow\mathcal{D},
    • каждый n-арный предикатный символ p из \mathcal{P} в n-арное отношение \sigma(p)\subseteq\mathcal{D}\times\ldots\times\mathcal{D}.

Обычно принято, отождествлять несущее множество \mathcal{D} и саму модель, подразумевая неявно семантическую функцию, если это не ведет к неоднозначности.

Предположим s — функция, отображающая каждую переменную в некоторый элемент из \mathcal{D}, которую мы будем называть подстановкой. Интерпретация [\![t]\!]_s терма t на\mathcal{D} относительно подстановки s задается индуктивно

  • [\![x]\!]_s = s(x), если x — переменная,
  • [\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)([\!\![x_1]\!]_s,\ldots,[\![x_n]\!]_s)

В таком же духе определяется отношение истинности \models_s формул на \mathcal{D} относительно s

  • \mathcal{D}\models_s p(t_1,\ldots,t_n), тогда и только тогда, когда \sigma(p)([\!\![t_1]\!]_s,\ldots,[\![t_n]\!]_s),
  • \mathcal{D}\models_s \neg\phi, тогда и только тогда, когда \mathcal{D}\models_s \phi — ложно,
  • \mathcal{D}\models_s \phi\land\psi, тогда и только тогда, когда \mathcal{D}\models_s \phi и \mathcal{D}\models_s \psi истинны,
  • \mathcal{D}\models_s \phi\lor\psi, тогда и только тогда, когда \mathcal{D}\models_s \phi или \mathcal{D}\models_s \psi истинно,
  • \mathcal{D}\models_s \phi\to\psi, тогда и только тогда, когда \mathcal{D}\models_s \phi влечет \mathcal{D}\models_s \psi,
  • \mathcal{D}\models_s \exists x\, \phi, тогда и только тогда, когда \mathcal{D}\models_{s'} \phi для некоторой подстановки s', которая отличается от s только значением на переменной x,
  • \mathcal{D}\models_s \forall x\, \phi, тогда и только тогда, когда \mathcal{D}\models_{s'} \phi для всех подстановок s', которые отличается от s только значением на переменной x.

Формула \phi, истинна на \mathcal{D}, что обозначается как \mathcal{D}\models \phi, если \mathcal{D}\models_s \phi, для всех подстановок s. Формула \phi называется общезначимой, что обозначается как \models \phi, если \mathcal{D}\models \phi для всех моделей \mathcal{D}. Формула \phi называется выполнимой , если \mathcal{D}\models \phi хотя бы для одной \mathcal{D}.

Свойства и основные результаты[править | править вики-текст]

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

  • полнота (это означает, что для любой замкнутой формулы выводима либо она сама, либо её отрицание);
  • непротиворечивость (ни одна формула не может быть выведена одновременно со своим отрицанием).

При этом если непротиворечивость более или менее очевидна, то полнота — нетривиальный результат, полученный Гёделем в 1930 году (теорема Гёделя о полноте). По сути теорема Гёделя устанавливает фундаментальную эквивалентность понятий доказуемости и общезначимости.

Логика первого порядка обладает свойством компактности: если некоторое множество формул не выполнимо, то невыполнимо также некоторое его конечное подмножество.

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

Использование[править | править вики-текст]

Логика первого порядка как формальная модель рассуждений[править | править вики-текст]

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

Возьмем рассуждение «Каждый человек смертен. Конфуций — человек. Следовательно, Конфуций смертен». Обозначим «x есть человек» через ЧЕЛОВЕК(x) и «x смертен» через СМЕРТЕН(x). Тогда утверждение «каждый человек смертен» может быть представлено формулой:  \forallx(ЧЕЛОВЕК(x) → СМЕРТЕН(x)) утверждение «Конфуций — человек» формулой ЧЕЛОВЕК(Конфуций), и «Конфуций смертен» формулой СМЕРТЕН(Конфуций). Утверждение в целом теперь может быть записано формулой

( \forallx(ЧЕЛОВЕК(x) → СМЕРТЕН(x))  \and ЧЕЛОВЕК(Конфуций)) → СМЕРТЕН(Конфуций)

См. также[править | править вики-текст]

Литература[править | править вики-текст]

  • Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
  • Клини С. К. Введение в метаматематику. М., 1957
  • Мендельсон Э. Введение в математическую логику. М., 1976
  • Новиков П. С. Элементы математической логики. М., 1959
  • Черч А. Введение в математическую логику, т. I. М. 1960