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

(перенаправлено с «Теория первого порядка»)

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

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

Основные определения править

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

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

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

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

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

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

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

  •  ,
  •  ,

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

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

  • Modus ponens (это правило используется также и в логике высказываний):
     
  • Правило обобщения[en]:
     

Интерпретация править

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

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

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

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

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

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

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

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

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

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

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

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

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

Логика первого порядка с равенством править

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

  •  
  •  

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

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

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

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

( x(ЧЕЛОВЕК(x) → СМЕРТЕН(x))   ЧЕЛОВЕК(Сократ)) → СМЕРТЕН(Сократ)

См. также править

Литература править