Викия

Математика

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

1457статей на
этой вики
Добавить новую страницу
Обсуждение0 Поделиться

Обнаружено использование расширения AdBlock.


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

Викия не будет доступна для последующих модификаций. Если вы желаете продолжать работать со страницей, то, пожалуйста, отключите расширение для блокировки рекламы.

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

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

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

  • Символы переменных (обычно x, y, z, x_1, y_1, z_1, x_2, y_2, z_2, и т. д.),
  • Пропозициональные связки: \lor,\land,\neg,\to,
  • Кванторы: всеобщности \forall и существования \exists,
  • Cлужебные символы: скобки и запятая.

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

  • Терм — есть символ переменной, либо имеет вид f(t_1,\ldots,t_n), где f — функциональный символ арности n, а t_1,\ldots,t_n — термы.
  • Атом — имеет вид p(t_1,\ldots,t_n), где p — предикатный символ арности n, а t_1,\ldots,t_n — термы.
  • Формула — это либо атом, либо одна из следующих конструкций: \neg F, F_1\lor F_2, F_1\land F_2, F_1\to F_2, \forall x F, \exists x F, где F, F_1, F_2 — формулы, а x — переменная.

Переменная x называется связанной в формуле F, если F имеет вид \forall x G либо \exists x G, или же представима в одной из форм \neg H, F_1\lor F_2, F_1\land F_2, F_1\to F_2, причем x уже связанна в H, F_1 и F_2. Если x не связанна в F, ее называют свободной в F. Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

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

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

  • \forall x A \to A[t/x],
  • A[t/x] \to \exists x A,

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

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

{A, A \to B}\over B

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

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

  • Несущее множество \mathcal{D},
  • Семантическая функция \sigma, отображающая
    • каждый n-арный функциональный символ f из \mathcal{F} в n-арную функцию \sigma(f):\mathcal{D}\times\ldots\times\mathcal{D}\rightarrow\mathcal{D},
    • каждый n-арный предикатный символ p из \mathcal{P} в n-арное отношение \sigma(p)\subseteq\mathcal{D}\times\ldots\times\mathcal{D}.

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

Предположим s — функция, отображающая каждую переменную в некоторый элемент из \mathcal{D}, которую мы будем называть подстановкой. Интерпретация [\![t]\!]_s терма t на\mathcal{D} относительно подстановки s задается индуктивно

  • [\![x]\!]_s = s(x), если x — переменная,
  • [\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)(\![x_1]\!]_s,\ldots,\![x_n]\!]_s)

В таком же духе определяется отношение истинности \models_s формул на \mathcal{D} относительно s

  • \mathcal{D}\models_s p(t_1,\ldots,t_n), тогда и только тогда, когда \sigma(p)( \![x_1]\!]_s,\ldots,\![x_n]\!]_s),
  • \mathcal{D}\models_s \neg\phi, тогда и только тогда, когда \mathcal{D}\models_s \phi — ложно,
  • \mathcal{D}\models_s \phi\land\psi, тогда и только тогда, когда \mathcal{D}\models_s \phi и \mathcal{D}\models_s \psi истинны,'
  • \mathcal{D}\models_s \phi\lor\psi, тогда и только тогда, когда \mathcal{D}\models_s \phi или \mathcal{D}\models_s \psi истинно,
  • \mathcal{D}\models_s \phi\to\psi, тогда и только тогда, когда \mathcal{D}\models_s \phi влечет \mathcal{D}\models_s \psi,
  • \mathcal{D}\models_s \exists x\, \phi, тогда и только тогда, когда \mathcal{D}\models_{s'} \phi для некоторой подстановки s', котрая отличается от s только на переменной x,
  • \mathcal{D}\models_s \forall x\, \phi, тогда и только тогда, когда \mathcal{D}\models_{s'} \phi для всех подстановок s', котрые отличается от s только на переменной x.

Формула \phi, истинна на \mathcal{D}, что обозначается как \mathcal{D}\models \phi, если \mathcal{D}\models_s \phi, для всех подстановок s. Формула \phi называется общезначимой, что обозначается как \models \phi, если \mathcal{D}\models \phi для всех моделей \mathcal{D}. Формула \phi называется выполнимой , если \mathcal{D}\models \phi хотябы для одной \mathcal{D}.

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

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

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

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

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

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

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

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

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

Обобщения Править

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

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


cs:Predikátová logikael:Κατηγορηματική λογικήfa:منطق محمولاتhu:Elsőrendű logikamk:Предикатна логика

nl:Predicatenlogica pl:Rachunek predykatów pierwszego rzędusk:Predikátová logika sv:Predikatlogik uk:Числення висловлень

Викия-сеть

Случайная вики