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

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

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

Содержание

1 Основные определения
2 Аксиоматика и доказательство формул
3 Интерпретация
4 Свойства и основные результаты
5 Использование
- 5.1 Логика первого порядка как формальная модель рассуждений
6 Обобщения
7 Литература

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

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

Символы переменных (обычно $x, y, z, x 1, y 1, z 1, x 2, y 2, z 2,$ и т. д.),
Пропозициональные связки: $\lor,\land,\neg,\to$ ,
Кванторы: всеобщности $\forall$ и существования $\exists$ ,
Служебные символы: скобки и запятая.

Перечисленные символы вместе с символами из $\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$ .

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

Modus ponens:

$\frac{A, A \to B}{B}$
Правило обобщения (GEN):

$\frac{A}{\forall x A}$

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

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

Несущее множество $\mathcal{D}$ ,
Семантическая функция σ, отображающая
- каждый $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$ .

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

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

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

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

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

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

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

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

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

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

[править] Обобщения

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

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

Это незавершённая статья по логике. Вы можете помочь проекту, исправив и дополнив её.

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

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

Содержание

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

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

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

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

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

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

[править] Обобщения

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

Просмотры

Личные инструменты

Навигация

Поиск

Участие

Инструменты

На других языках