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

2025-12-29T21:24:33Z

178.70.33.173: /* Аксиоматика и доказательство формул */ Без правила для удаления квантора существования аксиома введения, приведённая в данной статье неполна. Если у нас есть полная пара "удаление – введение" только для квантора всеобщности, то квантор существования – не примитивное, а производное понятие, которое в классической логике можно выразить через двойное отрицание. Как вариант, можно оставить старый вариант аксиомы, но тогда нужно добавить правило для удаления квантора существования, а это сложнее

{{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> и т. д.);
* логические операции:
{| class="wikitable" width="360px"
|-
!width="60px" |Символ || Значение
|-
| style="text-align:center;" | <math>\neg</math> || [[Отрицание]] («не»)
|-
| style="text-align:center;" | <math>\land</math>, <math>\&</math> || [[Конъюнкция]] («и»)
|-
| style="text-align:center;" | <math>\lor</math> || [[Дизъюнкция]] («или»)
|-
| style="text-align:center;" | <math>\to</math>, <math>\supset</math> || [[Импликация]] («если …, то …»)
|-
|}
* [[квантор]]ы:
{| class="wikitable" width="360px"
|-
!width="60px"|Символ || Значение
|-
| style="text-align:center;" | <math>\forall</math> || [[Квантор всеобщности]]
|-
| style="text-align:center;" | <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|Правило обобщения||en|Generalization (logic)}}:
*: <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))
утверждение «Сократ — человек» формулой
'''ЧЕЛОВЕК'''('''Сократ'''),
и «Сократ смертен» формулой
'''СМЕРТЕН'''('''Сократ''').
Утверждение в целом теперь может быть записано формулой
<center>(<math> \forall</math>x('''ЧЕЛОВЕК'''(x) → '''СМЕРТЕН'''(x)) <math> \land</math> '''ЧЕЛОВЕК'''('''Сократ''')) → '''СМЕРТЕН'''('''Сократ''')</center>

== См. также ==
* [[Логика высказываний]]
* [[Логика второго порядка]]
* [[Алгоритм Тарского]]

== Литература ==
* ''Гильберт Д., Аккерман В.'' Основы теоретической логики. М., 1947
* ''Клини С. К.'' Введение в метаматематику. М., 1957
* {{НФЭ||Логика предикатов|В. И. Маркин|ссылка= https://iphlib.ru/library/collection/newphilenc/document/HASHb46c37179b4005520488b4 }}
* ''{{нп4|Мендельсон, Эллиот|Мендельсон Э.||Elliott Mendelson}}'' Введение в математическую логику. М., 1976
* ''[[Новиков, Пётр Сергеевич|Новиков П. С.]]'' Элементы математической логики. М., 1959
* ''Черч А.'' Введение в математическую логику, т. I. М. 1960

{{вс}}
{{Логика}}
[[Категория:Математическая логика]]

wiki12 - Вклад [ru]

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