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

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

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

 символы переменных (обычно , , , , , , , ,  и т. д.);
 логические операции:

 кванторы:

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

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

 Терм есть символ переменной, либо имеет вид , где  — функциональный символ арности , а  — термы.
 Атом (атомарная формула) имеет вид , где  — предикатный символ арности , а  — термы.
 Например,  это атомарная формула, истинная для любого действительного числа . Формула состоит из 2-арного предиката , аргументами которого являются термы  и 0. При этом терм  состоит из константы 1 (которую можно считать 0-арной функцией), переменной  и символов бинарных (2-арных) функций + и ×.
 Формула — это либо атом, либо одна из следующих конструкций: , , , , , , где  — формулы, а  — переменная.

Переменная  называется связанной в формуле , если  имеет вид  либо , или же представима в одной из форм , , , , причём  уже связана в ,  и . Если  не связана в , её называют свободной в . Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

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

 ,
 ,

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

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

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

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

 Несущее множество ,
 Семантическая функция , отображающая
 каждый -арный функциональный символ  из  в -арную функцию ,
 каждый -арный предикатный символ  из  в -арное отношение .
Обычно принято отождествлять несущее множество  и саму модель, подразумевая неявно семантическую функцию, если это не ведёт к неоднозначности.

Предположим,  — функция, отображающая каждую переменную в некоторый элемент из , которую мы будем называть подстановкой. Интерпретация  терма  на  относительно подстановки  задаётся индуктивно:

 , если  — переменная,
 

В таком же духе определяется отношение истинности  формул на  относительно :

 , тогда и только тогда, когда ,
 , тогда и только тогда, когда  — ложно,
 , тогда и только тогда, когда  и  истинны,
 , тогда и только тогда, когда  или  истинно,
 , тогда и только тогда, когда  влечёт ,
 , тогда и только тогда, когда  для некоторой подстановки , которая отличается от  только значением на переменной ,
 , тогда и только тогда, когда  для всех подстановок , которые отличается от  только значением на переменной .
Формула  истинна на  (что обозначается как ), если  для всех подстановок . Формула  называется общезначимой (что обозначается как ), если  для всех моделей . Формула  называется выполнимой, если  хотя бы для одной .

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

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

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

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

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

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

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

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

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

Математическая логика