Математика
Регистрация
Advertisement

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

Основные определения[]

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

  • Символы переменных (обычно и т. д.),
  • Пропозициональные связки: ,
  • Кванторы: всеобщности и существования ,
  • Cлужебные символы: скобки и запятая.

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

  • Терм — есть символ переменной, либо имеет вид , где — функциональный символ арности , а — термы.
  • Атом — имеет вид , где — предикатный символ арности , а — термы.
  • Формула — это либо атом, либо одна из следующих конструкций: , где — формулы, а — переменная.

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

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

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

  • ,
  • ,

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

Правило вывода только одно — Modus ponens:

Интерпретация[]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Обобщения[]

Литература[]

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


cs:Predikátová logika el:Κατηγορηματική λογική fa:منطق محمولات hu:Elsőrendű logika mk:Предикатна логика nl:Predicatenlogica pl:Rachunek predykatów pierwszego rzędu sk:Predikátová logika sv:Predikatlogik uk:Числення висловлень

Advertisement