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

Запрос «Исчисление предикатов»^[d] перенаправляется сюда. На эту тему нужно создать отдельную статью.

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

Помимо логики первого порядка существуют также логики высших порядков, в которых кванторы могут применяться не только к переменным, но и к предикатам. Термины логика предикатов и исчисление предикатов могут означать как логику первого порядка, так и логики первого и высшего порядка вместе; в первом случае иногда говорится о чистой логике предикатов или чистом исчислении предикатов.

Основные определенияПравить

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

• символы переменных (обычно $x$$x$ , $y$$y$ , $z$$z$ , $x_1$$x_{1}$ , $y_1$$y_1$ , $z_1$$z_{1}$ , $x_2$$x_{2}$ , $y_2$$y_2$ , $z_2$$z_{2}$  и т. д.);
• логические операции:

Символ	Значение
$\mathrm{\neg <!--\; \neg \; -->}$$\neg$	Отрицание («не»)
$\wedge <!--\; \wedge \; -->$$\land$	Конъюнкция («и»)
$\vee <!--\; \vee \; -->$$\lor$	Дизъюнкция («или»)
$\to <!--\; \to \; -->$$\to$	Импликация («если …, то …»)

• кванторы:

Символ	Значение
$\mathrm{\forall <!--\; \forall \; -->}$$\forall$	Квантор всеобщности
$\mathrm{\exists <!--\; \exists \; -->}$$\exists$	Квантор существования

• служебные символы: скобки и запятая.

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

• Терм есть символ переменной, либо имеет вид $f(t_1,\dots <!--\; \dots \; -->,t_n)$$f(t_{1},\ldots ,t_{n})$ , где $f$$f$  — функциональный символ арности $n$$n$ , а $t_1,\dots <!--\; \dots \; -->,t_n$$t_{1},\ldots ,t_{n}$  — термы.
• Атом (атомарная формула) имеет вид $p(t_1,\dots <!--\; \dots \; -->,t_n)$$p(t_{1},\ldots ,t_{n})$ , где $p$$p$  — предикатный символ арности $n$$n$ , а $t_1,\dots <!--\; \dots \; -->,t_n$$t_{1},\ldots ,t_{n}$  — термы.
  • Например, $(x+1)\times <!--\; \times \; -->(x+1)⩾<!--\; ⩾\; -->0$$(x+1)\times (x+1)\geqslant 0$  это атомарная формула, истинная для любого действительного числа $x$$x$ . Формула состоит из 2-арного предиката $⩾<!--\; ⩾\; -->$$\geqslant$ , аргументами которого являются термы $(x+1)\times <!--\; \times \; -->(x+1)$$(x+1)\times (x+1)$  и 0. При этом терм $(x+1)\times <!--\; \times \; -->(x+1)$$(x+1)\times (x+1)$  состоит из константы 1 (которую можно считать 0-арной функцией), переменной $x$$x$  и символов бинарных (2-арных) функций + и ×.
• Формула — это либо атом, либо одна из следующих конструкций: $\mathrm{\neg <!--\; \neg \; -->}F$$\neg F$ , $F_1\vee <!--\; \vee \; -->F_2$$F_{1}\lor F_{2}$ , $F_1\wedge <!--\; \wedge \; -->F_2$$F_{1}\land F_{2}$ , $F_1\to <!--\; \to \; -->F_2$$F_{1}\to F_{2}$ , $\mathrm{\forall <!--\; \forall \; -->}xF$$\forall xF$ , $\mathrm{\exists <!--\; \exists \; -->}xF$$\exists xF$ , где $F,F_1,F_2$$F,F_{1},F_{2}$  — формулы, а $x$$x$  — переменная.

Переменная $x$$x$  называется связанной в формуле $F$$F$ , если $F$$F$  имеет вид $\mathrm{\forall <!--\; \forall \; -->}xG$$\forall xG$  либо $\mathrm{\exists <!--\; \exists \; -->}xG$$\exists xG$ , или же представима в одной из форм $\mathrm{\neg <!--\; \neg \; -->}H$$\neg H$ , $F_1\vee <!--\; \vee \; -->F_2$$F_{1}\lor F_{2}$ , $F_1\wedge <!--\; \wedge \; -->F_2$$F_{1}\land F_{2}$ , $F_1\to <!--\; \to \; -->F_2$$F_{1}\to F_{2}$ , причём $x$$x$  уже связана в $H$$H$ , $F_1$$F_{1}$  и $F_2$$F_{2}$ . Если $x$$x$  не связана в $F$$F$ , её называют свободной в $F$$F$ . Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

Аксиоматика и доказательство формулПравить

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

• $\mathrm{\forall <!--\; \forall \; -->}xA\to <!--\; \to \; -->A[t/x]$$\forall xA\to A[t/x]$ ,
• $A[t/x]\to <!--\; \to \; -->\mathrm{\exists <!--\; \exists \; -->}xA$$A[t/x]\to \exists xA$ ,

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

В логике первого порядка используется два правила вывода:

• Modus ponens (это правило используется также и в логике высказываний):

  $\frac{A,A\to <!--\; \to \; -->B}{B}$${\frac {A,A\to B}{B}}$ 

• Правило обобщения^[en]:

  $\frac{A}{\mathrm{\forall <!--\; \forall \; -->}xA}$${\frac {A}{\forall xA}}$ 

ИнтерпретацияПравить

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

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

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

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

1. $[[x]{]}_s=s(x)$$[\![x]\!]_{s}=s(x)$ , если $x$$x$  — переменная,
2. $[[f(x_1,\dots <!--\; \dots \; -->,x_n)]{]}_s=\mathrm{\sigma <!--\; \sigma \; -->}(f)([[x_1]{]}_s,\dots <!--\; \dots \; -->,[[x_n]{]}_s)$$[\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)([\!\![\,x_1]\!]_s,\ldots,[\![x_n]\!]_s)$ 

В таком же духе определяется отношение истинности ${\models <!--\; \models \; -->}_s$$\models _{s}$  формул на $\mathcal{D}$$\mathcal{D}$  относительно $s$$s$ :

• $\mathcal{D}{\models <!--\; \models \; -->}_{s}p(t_1,\dots <!--\; \dots \; -->,t_n)$${\mathcal {D}}\models _{s}p(t_{1},\ldots ,t_{n})$ , тогда и только тогда, когда $\mathrm{\sigma <!--\; \sigma \; -->}(p)([[t_1]{]}_s,\dots <!--\; \dots \; -->,[[t_n]{]}_s)$$\sigma(p)([\!\![\,t_1]\!]_s,\ldots,[\![t_n]\!]_s)$ ,
• $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\neg <!--\; \neg \; -->}\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{s}\neg \phi$ , тогда и только тогда, когда $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{s}\phi$  — ложно,
• $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\varphi <!--\; \varphi \; -->}\wedge <!--\; \wedge \; -->\mathrm{\psi <!--\; \psi \; -->}$${\mathcal {D}}\models _{s}\phi \land \psi$ , тогда и только тогда, когда $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{s}\phi$  и $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\psi <!--\; \psi \; -->}$${\mathcal {D}}\models _{s}\psi$  истинны,
• $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\varphi <!--\; \varphi \; -->}\vee <!--\; \vee \; -->\mathrm{\psi <!--\; \psi \; -->}$${\mathcal {D}}\models _{s}\phi \lor \psi$ , тогда и только тогда, когда $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{s}\phi$  или $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\psi <!--\; \psi \; -->}$${\mathcal {D}}\models _{s}\psi$  истинно,
• $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\varphi <!--\; \varphi \; -->}\to <!--\; \to \; -->\mathrm{\psi <!--\; \psi \; -->}$${\mathcal {D}}\models _{s}\phi \to \psi$ , тогда и только тогда, когда $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{s}\phi$  влечёт $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\psi <!--\; \psi \; -->}$${\mathcal {D}}\models _{s}\psi$ ,
• $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\exists <!--\; \exists \; -->}x\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{s}\exists x\,\phi$ , тогда и только тогда, когда $\mathcal{D}{\models <!--\; \models \; -->}_{s^{\prime }}\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{{s'}}\phi$  для некоторой подстановки $s^{\prime }$$s'$ , которая отличается от $s$$s$  только значением на переменной $x$$x$ ,
• $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\forall <!--\; \forall \; -->}x\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{s}\forall x\,\phi$ , тогда и только тогда, когда $\mathcal{D}{\models <!--\; \models \; -->}_{s^{\prime }}\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{{s'}}\phi$  для всех подстановок $s^{\prime }$$s'$ , которые отличается от $s$$s$  только значением на переменной $x$$x$ .

Формула $\mathrm{\varphi <!--\; \varphi \; -->}$$\phi$  истинна на $\mathcal{D}$$\mathcal{D}$  (что обозначается как $\mathcal{D}\models <!--\; \models \; -->\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models \phi$ ), если $\mathcal{D}{\models <!--\; \models \; -->}_s\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models _{s}\phi$  для всех подстановок $s$$s$ . Формула $\mathrm{\varphi <!--\; \varphi \; -->}$$\phi$  называется общезначимой (что обозначается как $\models <!--\; \models \; -->\mathrm{\varphi <!--\; \varphi \; -->}$$\models \phi$ ), если $\mathcal{D}\models <!--\; \models \; -->\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models \phi$  для всех моделей $\mathcal{D}$$\mathcal{D}$ . Формула $\mathrm{\varphi <!--\; \varphi \; -->}$$\phi$  называется выполнимой, если $\mathcal{D}\models <!--\; \models \; -->\mathrm{\varphi <!--\; \varphi \; -->}$${\mathcal {D}}\models \phi$  хотя бы для одной $\mathcal{D}$$\mathcal{D}$ .

Свойства и основные результатыПравить

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

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

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

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

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

Логика первого порядка с равенствомПравить

Во многих теориях первого порядка участвует символ равенства. Его часто относят к символам логики и дополняют её соответствующими аксиомами, определяющими его. Такая логика называется логикой первого порядка с равенством, а соответствующие теории — теориями первого порядка с равенством. Символ равенства вводится как двуместный предикатный символ $=$$=$ . Вводимые для него дополнительные аксиомы следующие:

• $\mathrm{\forall <!--\; \forall \; -->}x(x=x)$$\forall x(x=x)$ 
• $\mathrm{\forall <!--\; \forall \; -->}x\mathrm{\forall <!--\; \forall \; -->}y(x=y)\to <!--\; \to \; -->(F(x)\to <!--\; \to \; -->F(y))$$\forall x\forall y(x=y)\to (F(x)\to F(y))$ 

ИспользованиеПравить

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

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

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

($\mathrm{\forall <!--\; \forall \; -->}$$\forall$ x(ЧЕЛОВЕК(x) → СМЕРТЕН(x)) $\wedge <!--\; \wedge \; -->$$\land$  ЧЕЛОВЕК(Сократ)) → СМЕРТЕН(Сократ)

См. такжеПравить

• Логика высказываний
• Логика второго порядка
• Алгоритм Тарского

ЛитератураПравить

• Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
• Клини С. К. Введение в метаматематику. М., 1957
• В. И. Маркин. Логика предикатов // Новая философская энциклопедия : в 4 т. / пред. науч.-ред. совета В. С. Стёпин. — 2-е изд., испр. и доп. — М. : Мысль, 2010. — 2816 с.
• Мендельсон Э.^ru_en Введение в математическую логику. М., 1976
• Новиков П. С. Элементы математической логики. М., 1959
• Черч А. Введение в математическую логику, т. I. М. 1960