Дискуссионный математический форумМатематический форум
Математический форум Math Help Planet

Обсуждение и решение задач по математике, физике, химии, экономике

Теоретический раздел
Часовой пояс: UTC + 3 часа [ Летнее время ]
новый онлайн-сервис
число, сумма и дата прописью

Часовой пояс: UTC + 3 часа [ Летнее время ]


Формализованное исчисление предикатов

Формализованное исчисление предикатов


Задача формализованного исчисления предикатов (ФИП) та же, что и формализованного исчисления высказываний (ФИВ), — дать аксиоматическую теорию совокупности всех общезначимых формул (тавтологий) логики предикатов, т. е. научиться выводить (доказывать) все такие формулы и только их, исходя из выбранной системы аксиом и с использованием выбранных правил вывода.


Язык формализованного исчисления предикатов


Алфавит исчисления предикатов состоит из предметных переменных x_1,x_2,\ldots, предметных констант (символы выделенных элементов) c_1,c_2,\ldots, предикатных букв P'_1,P'_2,\ldots,P'_k,\ldots, функциональных букв f''_1,f''_2, \ldots, f''_{\ell},\ldots, а также знаков логических связок \lnot и \land, кванторов \forall и \exists и скобок (,). При этом верхние индексы предикатных и функциональных букв указывают число аргументов соответственно предиката или функции, которые могут быть подставлены вместо этих букв.


Понятие формулы определяется в два этапа. Сначала определяются термы. Ими являются отдельно взятые предметные переменные и константы, а также выражения вида f^n(t_1,\ldots,t_n), где f^n — n-местный функциональный символ; t_1,\ldots,t_n — термы. Наконец, определяются формулы:


а) если P_n — предикатная буква, t_1,\ldots,t_n — термы, то P_n(t_1,\ldots,t_n) — формула; при этом все вхождения переменных в эту формулу называются свободными;


б) если F_1,\,F_2 — формулы, то формулами являются \lnot F_1,\,(F_1\to F_2); причем все вхождения переменных, свободные в F_1,\,F_2, являются свободными и в формулах указанных видов; кроме того, можно считать, что в F_1 и F_2 нет предметных переменных, которые связаны в одной формуле и свободны в другой;


в) если F_x — формула, содержащая свободные вхождения переменной x, то (\forall x)(F(x)) и (\exists x)(F(x)) — формулы; при этом вхождения переменной x в них называются связанными; вхождения же всех остальных предметных переменных в эти формулы остаются свободными (связанными), если они были свободными (связанными) в формуле F(x) (формула F(x) называется областью действия квантора);


г) никаких других формул, кроме тех, которые строятся по правилам а, б, в, нет.


Из этого определения ясно, что вхождения переменных в формулу обладают следующими свойствами: свободные и связанные переменные обозначены разными буквами (если это не так, то ясно, что, не нарушая смысла формулы, можно переобозначить в ней связанные переменные); если какой-либо квантор находится в области действия другого квантора, то переменные, связанные этими кванторами, обозначены разными буквами (если это не так, то ясно, что, не нарушая смысла формулы, можно переобозначить в ней соответствующие переменные). Нарушения этих свойств называются коллизией переменных. Определенные формулы называются формулами первой ступени, так как в них разрешается навешивать кванторы только по предметным переменным, а по функциональным и предикатным — не разрешается. Возникающее исчисление предикатов называют исчислением предикатов первой ступени или узким исчислением предикатов (в отличие от расширенного исчисления предикатов), сокращенно — УИП.


Совокупность G=\{c_1,c_2,\ldots;~ f_1,f_2,\ldots;~ P_1,P_2,\ldots\} называется сигнатурой рассматриваемого исчисления предикатов. Если в сигнатуре отсутствуют функциональные символы, (а значит, функциональные термы), то возникающее исчисление предикатов называется чистым исчислением предикатов. Оно строится для произвольной предметной области и не зависит от взаимосвязи между предметами в этой области. Это чисто логическая теория. Именно о таком чистом исчислении предикатов и пойдет речь. Если же такие связи имеются и они описываются функциями на этой предметной области, то логика проникает в эту область и в эти связи и возникает логическая теория соответствующей математической Дисциплины, или, как говорят, некая формальная математическая теория.




Система аксиом исчисления предикатов


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


\begin{aligned}&\mathsf{(A1)}\colon\quad F\to (G\to F);\\ &\mathsf{(A2)}\colon\quad \bigl(F\to (G\to F)\bigr)\to \bigl((F\to G)\to (F\to H)\bigr);\\ &\mathsf{(A3)}\colon\quad (\lnot G\to\lnot F)\to \bigl((\lnot G\to F)\to G\bigr);\end{aligned}


где под F,\,G,\,H понимаются уже любые формулы исчисления предикатов.


Вторая группа аксиом (схем аксиом) — это собственно предикатные аксиомы (схемы аксиом), т.е. аксиомы с кванторами. Выберем в качестве них следующие (называемые аксиомами Бернайса):


\begin{aligned}&\mathsf{(PA1)}\colon\quad (\forall x)(F(x)\to F(y);\\ &\mathsf{(PA2)}\colon\quad F(y)\to (\exists x)(F(x)); \end{aligned}


где F(x) — любая формула, содержащая свободные вхождения x, причем ни одно из них не находится в области действия квантора по y (если таковой имеется); формула F(y) получена из F(x) заменой всех свободных вхождений x на y.


Существенность последнего требования можно пояснить следующим примером. Рассмотрим в качестве формулы F(x) формулу (\exists x)(P(x,y)), где это требование нарушено: свободное вхождение x находится в области действия квантора \exists y. Подставив эту формулу в аксиому \mathsf{(PA1)}, получим формулу (\forall x)(\exists y)(P(x,y))\to (\exists y)(P(y,y)) которая не будет общезначимой. В самом деле, предикат A(x,y)\colon\, x<y на множестве вещественных чисел превращает ее в ложное высказывание:


(\forall x)(\exists y)(x<y)\to (\exists y)(y<y).



Правила вывода в формальном исчислении высказываний


К правилу вывода modus ponens из исчисления высказываний добавляются еще два правила вывода:


\forall-правило, или правило обобщения: \frac{F\to G(x)}{F\to (\forall x)(G(x))};
\exists-правило, или правило конкретизации: \frac{G(x)\to F}{(\exists x)(G(x))\to F}

при условии, что G(x) содержит свободное вхождение x, a F не содержит.


Последнее требование также весьма существенно. Его нарушение может привести по этим правилам к ложным выводам из истинных посылок. Так, например, взяв предикаты A(x)\colon\,6\mid x и B(x)\colon\,3\mid x над \mathbb{N}, получим тождественно истинный предикат A(x)\to B(x)\colon\, 6\mid x\to3\mid x. Но применив к нему правило обобщения, получим уже опровержимый предикат: 6\mid x\to (\forall x)(3\mid x) (он превращается в ложное высказывание при тех x, которые делятся на 6). Если к предикату 6\mid x\to3\mid x применить (в нарушение условия) \exists-правило, то получим также опровержимый предикат (\exists x)(6\mid x\to3\mid x). Применив же к последнему предикату уже на корректных основаниях \forall-правило, придем к ложному высказыванию (\exists x)(6\mid x)\to (\forall x)(3\mid x).




Теория формального вывода


Определения формального доказательства (формального вывода из аксиом и из гипотез) доказуемой формулы (теоремы) в формализованном исчислении предикатов даются так же, как и в формализованном исчислении высказываний (см. определение 15.1), с точностью до добавления двух новых аксиомных схем \mathsf{(PA1)} и \mathsf{(PA2)} и двух новых правил вывода: \forall-правила и \exists-правила.


Уточним все же понятие формальной выводимости формулы из гипотез в исчислении предикатов. Формула G называется выводимой из гипотез F_1,\ldots,F_m с фиксированными вхождениями (в гипотезы) свободных переменных, если существует такая конечная последовательность формул B_1,B_2,\ldots,B_k,\ldots,B_s\equiv G, каждая формула которой является либо аксиомой, либо гипотезой, либо получена из предыдущих формул последовательности по одному из правил вывода. (Сама эта последовательность называется выводом G из гипотез F_1,\ldots,F_m). При этом, если B_k есть первая гипотеза, встречающаяся в выводе, то дальше в этом выводе не могут быть использованы \forall- и \exists-правила вывода по любой переменной x, которая входит свободно хотя бы в одну из гипотез. Обозначение используется то же, что и в исчислении высказываний: F_1,\ldots,F_m\vdash G. Если гипотезы отсутствуют, то говорят, что G выводима из аксиом (или просто выводима), и называют G теоремой формализованного исчисления предикатов и пишут \vdash G.


Отметим сначала, что так как все формулы, выводимые в исчислении высказываний, являются также выводимыми в исчислении предикатов, то, совершая подстановки в выводимые формулы исчисления высказываний, мы будем получать выводимые формулы исчисления предикатов. (Тем не менее всякую выводимую формулу исчисления предикатов таким способом получить нельзя.) Следовательно, все производные правила вывода, установленные для исчисления высказываний, остаются справедливыми и для исчисления предикатов, и мы будем в логике предикатов широко пользоваться этим.


Дальнейшее изучение формализованного исчисления предикатов строится в форме систематизированной подборки задач на доказательство теорем ФИП. Подборка начинается с построения выводов из аксиом. Затем рассматривается построение выводов из гипотез. Наконец — теорема о дедукции и ее применение к доказательству теорем ФИП. Теорема о дедукции в ФИП формулируется так же, как и в ФИВ:


если F_1,\ldots,F_{m-1},F_m\vdash G, то F_1,\ldots,F_{m-1}\vdash F_m\to G

(в частности, если F\vdash G), то \vdash F\to G. Ничем особо не отличается и идея доказательства, с той лишь разницей, что появятся случаи, связанные с получением формулы в последовательности-выводе не только по правилу modus ponens, но и по \forall-правилу и по \exists-правилу.

Математический форум (помощь с решением задач, обсуждение вопросов по математике).
Кнопка "Поделиться"
Если заметили ошибку, опечатку или есть предложения, напишите в комментариях.

Часовой пояс: UTC + 3 часа [ Летнее время ]


Яндекс.Метрика

Copyright © 2010-2023 MathHelpPlanet.com. All rights reserved