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

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

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

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

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

  • символы переменных (обычно , , , , , , , , и т. д.);
  • логические операции:
Символ Значение
Отрицание («не»)
Конъюнкция («и»)
Дизъюнкция («или»)
Импликация («если ..., то ...»)
Символ Значение
Квантор всеобщности
Квантор существования

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

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

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

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

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

  • ,
  • ,

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

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

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

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

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

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

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

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

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

  • , тогда и только тогда, когда ,
  • , тогда и только тогда, когда  — ложно,
  • , тогда и только тогда, когда и истинны,
  • , тогда и только тогда, когда или истинно,
  • , тогда и только тогда, когда влечет ,
  • , тогда и только тогда, когда для некоторой подстановки , которая отличается от только значением на переменной ,
  • , тогда и только тогда, когда для всех подстановок , которые отличается от только значением на переменной .

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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