Логика первого порядка
Шаблон:Falseredirect Логика первого порядка — формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций и предикатов. Расширяет логику высказываний.
Помимо логики первого порядка существуют также логики высших порядков, в которых кванторы могут применяться не только к переменным, но и к предикатам. Термины логика предикатов и исчисление предикатов могут означать как логику первого порядка, так и логики первого и высшего порядка вместе; в первом случае иногда говорится о чистой логике предикатов или чистом исчислении предикатов.
Основные определения
Язык логики первого порядка строится на основе сигнатуры, состоящей из множества функциональных символов <math>\mathcal{F}</math> и множества предикатных символов <math>\mathcal{P}</math>. С каждым функциональным и предикатным символом связана арность, то есть число возможных аргументов. Допускаются как функциональные, так и предикатные символы арности 0. Первые иногда выделяют в отдельное множество констант. Кроме того, используются следующие дополнительные символы:
- символы переменных (обычно <math>x</math>, <math>y</math>, <math>z</math>, <math>x_1</math>, <math>y_1</math>, <math>z_1</math>, <math>x_2</math>, <math>y_2</math>, <math>z_2</math> и т. д.);
- логические операции:
| Символ | Значение |
|---|---|
| <math>\neg</math> | Отрицание («не») |
| <math>\land</math>, <math>\&</math> | Конъюнкция («и») |
| <math>\lor</math> | Дизъюнкция («или») |
| <math>\to</math>, <math>\supset</math> | Импликация («если …, то …») |
| Символ | Значение |
|---|---|
| <math>\forall</math> | Квантор всеобщности |
| <math>\exists</math> | Квантор существования |
Перечисленные символы вместе с символами из <math>\mathcal{P}</math> и <math>\mathcal{F}</math> образуют алфавит логики первого порядка. Более сложные конструкции определяются индуктивно.
- Терм есть символ переменной, либо имеет вид <math>f( t_1, \ldots, t_n )</math>, где <math>f</math> — функциональный символ арности <math>n</math>, а <math>t_1, \ldots, t_n</math> — термы.
- Атом (атомарная формула) имеет вид <math>p( t_1, \ldots, t_n )</math>, где <math>p</math> — предикатный символ арности <math>n</math>, а <math>t_1, \ldots, t_n</math> — термы.
- Например, <math>(x+1)\times(x+1) \geqslant 0</math> это атомарная формула, истинная для любого действительного числа <math>x</math>. Формула состоит из 2-арного предиката <math>\geqslant</math>, аргументами которого являются термы <math>(x+1)\times(x+1)</math> и 0. При этом терм <math>(x+1)\times(x+1)</math> состоит из константы 1 (которую можно считать 0-арной функцией), переменной <math>x</math> и символов бинарных (2-арных) функций + и ×.
- Формула — это либо атом, либо одна из следующих конструкций: <math>\neg F</math>, <math>F_1\lor F_2</math>, <math>F_1\land F_2</math>, <math>F_1\to F_2</math>, <math>\forall x F</math>, <math>\exists x F</math>, где <math>F, F_1, F_2</math> — формулы, а <math>x</math> — переменная.
Переменная <math>x</math> называется связанной в формуле <math>F</math>, если <math>F</math> имеет вид <math>\forall x G</math> либо <math>\exists x G</math>, или же представима в одной из форм <math>\neg H</math>, <math>F_1\lor F_2</math>, <math>F_1\land F_2</math>, <math>F_1\to F_2</math>, причём <math>x</math> уже связана в <math>H</math>, <math>F_1</math> и <math>F_2</math>. Если <math>x</math> не связана в <math>F</math>, её называют свободной в <math>F</math>. Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.
Аксиоматика и доказательство формул
Система логических аксиом логики первого порядка состоит из аксиом исчисления высказываний дополненной двумя новыми аксиомами:
- <math>\forall x A \to A[t/x]</math>,
- <math>\exists x A \leftrightarrow \neg \forall x \neg A</math>,
где <math>A[t/x]</math> — формула, полученная в результате подстановки терма <math>t</math> вместо каждой свободной переменной <math>x</math>, встречающейся в формуле <math>A</math>.
В логике первого порядка используется два правила вывода:
- Modus ponens (это правило используется также и в логике высказываний):
- <math>\frac{A, A \to B}{B}</math>
- Шаблон:Нп1:
- <math>\frac{A}{\forall x A}</math>
Интерпретация
В классическом случае интерпретация формул логики первого порядка задаётся на модели первого порядка, которая определяется следующими данными:
- Несущее множество <math>\mathcal{D}</math>,
- Семантическая функция <math>\sigma</math>, отображающая
- каждый <math>n</math>-арный функциональный символ <math>f</math> из <math>\mathcal{F}</math> в <math>n</math>-арную функцию <math>\sigma(f)\colon\,\mathcal{D}\times\ldots\times\mathcal{D}\rightarrow\mathcal{D}</math>,
- каждый <math>n</math>-арный предикатный символ <math>p</math> из <math>\mathcal{P}</math> в <math>n</math>-арное отношение <math>\sigma(p)\subseteq\mathcal{D}\times\ldots\times\mathcal{D}</math>.
Обычно принято отождествлять несущее множество <math>\mathcal{D}</math> и саму модель, подразумевая неявно семантическую функцию, если это не ведёт к неоднозначности.
Предположим, <math>s</math> — функция, отображающая каждую переменную в некоторый элемент из <math>\mathcal{D}</math>, которую мы будем называть подстановкой. Интерпретация <math>[\![t]\!]_s</math> терма <math>t</math> на <math>\mathcal{D}</math> относительно подстановки <math>s</math> задаётся индуктивно:
- <math>[\![x]\!]_s = s(x)</math>, если <math>x</math> — переменная,
- <math>[\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)([\!\![\,x_1]\!]_s,\ldots,[\![x_n]\!]_s)</math>
В таком же духе определяется отношение истинности <math>\models_s</math> формул на <math>\mathcal{D}</math> относительно <math>s</math>:
- <math>\mathcal{D}\models_s p(t_1,\ldots,t_n)</math>, тогда и только тогда, когда <math>\sigma(p)([\!\![\,t_1]\!]_s,\ldots,[\![t_n]\!]_s)</math>,
- <math>\mathcal{D}\models_s \neg\phi</math>, тогда и только тогда, когда <math>\mathcal{D}\models_s \phi</math> — ложно,
- <math>\mathcal{D}\models_s \phi\land\psi</math>, тогда и только тогда, когда <math>\mathcal{D}\models_s \phi</math> и <math>\mathcal{D}\models_s \psi</math> истинны,
- <math>\mathcal{D}\models_s \phi\lor\psi</math>, тогда и только тогда, когда <math>\mathcal{D}\models_s \phi</math> или <math>\mathcal{D}\models_s \psi</math> истинно,
- <math>\mathcal{D}\models_s \phi\to\psi</math>, тогда и только тогда, когда <math>\mathcal{D}\models_s \phi</math> влечёт <math>\mathcal{D}\models_s \psi</math>,
- <math>\mathcal{D}\models_s \exists x\, \phi</math>, тогда и только тогда, когда <math>\mathcal{D}\models_{s'} \phi</math> для некоторой подстановки <math>s'</math>, которая отличается от <math>s</math> только значением на переменной <math>x</math>,
- <math>\mathcal{D}\models_s \forall x\, \phi</math>, тогда и только тогда, когда <math>\mathcal{D}\models_{s'} \phi</math> для всех подстановок <math>s'</math>, которые отличается от <math>s</math> только значением на переменной <math>x</math>.
Формула <math>\phi</math> истинна на <math>\mathcal{D}</math> (что обозначается как <math>\mathcal{D}\models \phi</math>), если <math>\mathcal{D}\models_s \phi</math> для всех подстановок <math>s</math>. Формула <math>\phi</math> называется общезначимой (что обозначается как <math>\models \phi</math>), если <math>\mathcal{D}\models \phi</math> для всех моделей <math>\mathcal{D}</math>. Формула <math>\phi</math> называется выполнимой, если <math>\mathcal{D}\models \phi</math> хотя бы для одной <math>\mathcal{D}</math>.
Свойства и основные результаты
Логика первого порядка обладает рядом полезных свойств, которые делают её очень привлекательной в качестве основного инструмента формализации математики. Главными из них являются:
- полнота (это означает, что любая общезначимая формула выводима);
- непротиворечивость (ни одна формула не может быть выведена одновременно со своим отрицанием).
При этом если непротиворечивость более или менее очевидна, то полнота — нетривиальный результат, полученный Гёделем в 1930 году (теорема Гёделя о полноте). По сути теорема Гёделя устанавливает фундаментальную эквивалентность понятий доказуемости и общезначимости.
Логика первого порядка обладает свойством компактности, доказанным Мальцевым: если некоторое множество формул не выполнимо, то невыполнимо также некоторое его конечное подмножество.
Согласно теореме Лёвенгейма — Скулема если множество формул имеет модель, то оно также имеет модель не более чем счётной мощности. С этой теоремой связан парадокс Скулема, который, однако, является лишь мнимым парадоксом.
Логика первого порядка с равенством
Во многих теориях первого порядка участвует символ равенства. Его часто относят к символам логики и дополняют её соответствующими аксиомами, определяющими его. Такая логика называется логикой первого порядка с равенством, а соответствующие теории — теориями первого порядка с равенством. Символ равенства вводится как двуместный предикатный символ <math>=</math>. Вводимые для него дополнительные аксиомы следующие:
- <math>\forall x( x = x)</math>
- <math>\forall x \forall y (x = y \to (F(x) \to F(y)))</math>
Использование
Логика первого порядка как формальная модель рассуждений
Являясь формализованным аналогом обычной логики, логика первого порядка даёт возможность строго рассуждать об истинности и ложности утверждений и об их взаимосвязи, в частности, о логическом следовании одного утверждения из другого, или, например, об их эквивалентности. Рассмотрим классический пример формализации утверждений естественного языка в логике первого порядка.
Возьмём рассуждение «Каждый человек смертен. Сократ — человек. Следовательно, Сократ смертен». Обозначим «x есть человек» через ЧЕЛОВЕК(x) и «x смертен» через СМЕРТЕН(x). Тогда утверждение «каждый человек смертен» может быть представлено формулой: <math> \forall</math>x(ЧЕЛОВЕК(x) → СМЕРТЕН(x)) утверждение «Сократ — человек» формулой ЧЕЛОВЕК(Сократ), и «Сократ смертен» формулой СМЕРТЕН(Сократ). Утверждение в целом теперь может быть записано формулой
См. также
Литература
- Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
- Клини С. К. Введение в метаматематику. М., 1957
- Шаблон:НФЭ
- Шаблон:Нп4 Введение в математическую логику. М., 1976
- Новиков П. С. Элементы математической логики. М., 1959
- Черч А. Введение в математическую логику, т. I. М. 1960