Игошин Математическая логика и теория алгоритмов (1019110), страница 54
Текст из файла (страница 54)
й 25. Формализованное исчисление преднкатов Задача формализованного исчисления предикатов (ФИП) та же, что и формализованного исчисления высказываний (ФИВ), — дать аксиоматическую теорию совокупности всех обшезначимых формул (тавтологий) логики предикатов, т.е. научиться выводить (доказывать) все такие формулы и только их, исходя из выбранной системы аксиом и с использованием выбранных правил вывода. Первоначальные понятия (язык формализованного исчисления предикатов). Алфавит исчисления предикатов состоит из предметных переменных хь хь ..., предметных констант (символы вьщеленных элементов) сь св ..., предикатных букв Р'ь Р'и ..., Р'„, ..., функциональных букв 1';, 1';, ..., Д, ..., а также знаков логических связок и л, кванторов и' и 3 и скобок (, ).
При этом верхние индексы предикатных и функциональных букв указывают число аргументов соответственно предиката или функции, которые могут быть подставлены вместо этих букв. Понятие формулы определяется в два этапа. Сначала определяются термы. Ими являются отдельно взятые предметные переменные и константы, а также выРажениЯ вида 1'"(гь ..., г„), где1""— и-местный функциональный символ; гп ..., г„— термы.
Наконец, определяются формулы: а) если Є— предикатная буква, гн ..., г„— термы, то Р„(гь ..., г„) — формула; при этом все вхождения переменных в эту формулу называются свободньиии; 222 б) если Гп Гг — формулы, то формулами являются — Рп Ж вЂ” ь > Рг); причем все вхождения переменных, свободные в Гп Рп являются свободными и в формулах указанных видов; кроме того, можно считать, что в Г, и Г, нет предметных переменных, которые связаны в одной формуле и свободны в другой; в) если Г(х) — формула, содержащая свободные вхождения переменной х, то (Ъх)(Г(х)) и (Зх)(Г(х)) — формулы; при этом вхождения переменной х в них называются связанными; вхождения же всех остальных предметных переменных в зти формулы остаются свободными (связанными), если они были свободными (связанными) в формуле Г(х) (формула Г(х) называется областью действия квантора); г) никаких других формул, кроме тех, которые строятся по правилам а, б, в, нет.
Из этого определения ясно, что вхождения переменных в формулу обладают следующими свойствами: свободные и связанные переменные обозначены разными буквами (если зто не так, то ясно, что, не нарушая смысла формулы, можно переобозначить в ней связанные переменные); если какой-либо квантор находится в области действия другого квантора, то переменные, связанные этими кванторами, обозначены разными буквами (если это не так, то ясно, что, не нарушая смысла формулы, можно переобозначить в ней соответствующие переменные).
Нарушения этих свойств называются коллизией переменных. Определенные формулы называются формулами первой ступени, так как в них разрешается навешивать кванторы только по предметным переменным, а по функциональным и предикатным — не разрешается. Возникающее исчисление предикатов называют исчислением предикатов первой ступени или узким исчислением предикатов (в отличие от расширенного исчисления предикатов), сокращенно — УИП. Совокупность 6 = (сп с,, ...; Я,, Я~, ...; Р„Рн ...) называется сигнатурой рассматриваемого исчисления предикатов. Если в сигнатуре отсутствуют функциональные символы, (а значит, функциональные термы), то возникающее исчисление предикатов называется чистым исчислением предикатов.
Оно строится для произвольной предметной области и не зависит от взаимосвязи между предметами в этой области. Это чисто логическая теория. Именно о таком чистом исчислении предикатов и пойдет речь. Если же такие связи имеются и они описываются функциями на этой предметной области, то логика проникает в эту область и в зти связи и возникает логическая теория соответствующей математической дисциплины, или, как говорят, некая формальная математическая теория.
О таких теориях речь пойдет в З 30. Система аксиом исчисления предикатов. Указанная система состоит из двух групп из которых п е р в а я — зто аксиомы формализованного исчисления высказываний: 223 (А1): à — > (6-~ Г); (А2): (Г-+ (6-+ Н)) — э ((Г-+ 6) — > (Г-+ Н)); (АЗ): ( 6 — ~ -Г) -э ((- 6 -+ Г) -~ 6), где под Г, 6, Н понимаются уже любые формулы исчисления предикатов. Вторая группа аксиом (схем аксиом) — зто собственно преди- катные аксиомы (схемы аксиом), т.е. аксиомы с кванторами.
Выбе- рем в качестве них следующие (называемые аксиомами Бернайса): (РА1): (чх)(Г(х)) -+ Г(у); (РА2): Г(у) -+ (Эх)(Г(х)), где Г(х) — любая формула, содержащая свободные вхождения х, причем ни одно из них не находится в области действия квантора по у (если таковой имеется); формула Г(у) получена из Г(х) за- меной всех свободных вхождений х на у. Существенность последнего требования можно пояснить сле- дующим примером. Рассмотрим в качестве формулы Г(х) форму- лу (Зу)(Р(х, у)), где зто требование нарушено: свободное вхожде- ние х находится в области действия квантора Зу. Подставив зту формулу в аксиому (РА1), получим формулу (~Гх)(ЗУ)(Р(х, у)) — > — > (Ву)(Р(у, у)), которая не будет обшезначимой.
В самом деле, предикат А(х, у): х < у на множестве вещественных чисел пре- вращает ее в ложное высказывание: (~х)(ЗУ)(х < у) -+ (ЗУ)(У < У). Правила вывода. К правилу вывода МР из исчисления выска- зываний добавляются еше два правила вывода: Г -+ 6(х) 'Ф-правило, или правило обобщения: 6(х) -+ Г Л-правило, или правило конкретизации: при условии, что 6(х) содержит свободное вхождение х, а Г не содержит. Последнее требование также весьма существенно.
Его нарушение может привести по зтим правилам к ложным выводам из истинных посылок. Так, например, взяв предикаты А(х): 61х и В(х): З~с над Лг, получим тождественно истинный предикат А(х) -+ В(х): 61х — > 31х. Но применив к нему правило обобщения, получим уже опровержимый предикат: б~х — > (чх)(З~с) (он превращается в ложное высказывание при тех х, которые делятся на б). Если к предикату б~х -+ З~х применить (в нарушение условия) З-правило, то получим также опровержимый предикат (Зх)(б(х — ~ З~х).
Применив же к последнему предикату уже на корректных основаниях Ч-правило, придем к ложному высказыванию (Лх)(б~х) -+ (чх)(З~х). Теория формального вывода. Определения формального доказательства (формального вывода из аксиом и из гипотез) доказуемой формулы (теоремы) в формализованном исчислении пре- 224 дикатов даются так же, как и в формализованном исчислении высказываний (см. определение 15.1), с точностью до добавления двух новых аксиомных схем (РА1) и (РА2) и двух новых правил вывода: ч'-правила и З-правила.
Уточним все же понятие формальной выводимости формулы из гипотез в исчислении предикатов. Формула б называется выводимой из гилатез Гь ..., Г с фиксированными вхождениями (в гипотезы) свободных переменных, если существует такая конечная последовательность формул Вь Вп ..., В», .„, В, и б, каждая формула которой является либо аксиомой, либо гипотезой, либо получена из предыдущих формул последовательности по одному из правил вывода. (Сама эта последовательность называется выводам 6 из гипотез Гн ..., Г ). При этом, если В» есть первая гипотеза, встречающаяся в выводе, то дальше в этом выводе не могут быть использованы 'Ф- и 3-правила вывода по любой переменной х, которая входит свободно хотя бы в одну из гипотез. Обозначение используется то же, что и в исчислении высказываний: Г„..., Г„»- 6.
Если гипотезы отсутствуют, то говорят, что 6 выводима из аксиом (или просто выводима), и называют 6 теоремой формализованного исчисления предикатов и пишут ~- 6. Отметим сначала, что так как все формулы, выводимые в исчислении высказываний, являются также выводимыми в исчислении предикатов, то, совершая подстановки в выводимые формулы исчисления высказываний, мы будем получать выводимые формулы исчисления предикатов. (Тем не менее всякую выводимую формулу исчисления предикатов таким способом получить нельзя.) Следовательно, все производные правила вывода, установленные для исчисления высказываний, остаются справедливыми и для исчисления предикатов, и мы будем в логике предикатов широко пользоваться этим.
Дальнейшее изучение формализованного исчисления предикатов происходит по Задачнику, Э 11. Это исчисление строится там в форме систематизированной подборки задач на доказательство теорем ФИП. Подборка начинается с построения выводов из аксиом. Затем рассматривается построение выводов из гипотез. Наконец— теорема о дедукции и ее применение к доказательству теорем ФИП. Теорема о дедукции в ФИП формулируется так же, как и в ФИВ: если Гь ..., Г ь Г„~- 6, то Г„..., Г, ~- Г -» 6 (в частности, если Г» — 6), то»- à — > 6. Ничем особо не отличается и идея доказательства, с той лишь разницей, что появятся случаи, связанные с получением формулы в последовательности-выводе не только по правилу МР, но и по У-правилу и по Л-правилу.
Исчисление предикатов будет развито настолько, что все рассмотренные в Э 2! тавтологии логики предикатов окажутся теоремами построенного формализованного исчисления предикатов. Что же касается свойств этого исчисления, то они будут рассмотрены в гл. 6 (э 29). Июшин Глава у' НЕФОРМАЛЬНЫЕ АКСИОМАТИЧЕСКИЕ ТЕОРИИ Мы подошли к тому разделу курса математической логики, который должен убедительно продемонстрировать всю мощь воздействия методов этой науки на прочие математические науки, показать особую (цементирующую) роль математической логики в системе математических наук. Здесь необходимо увидеть отчетливую связь изученных понятий и методов со школьной математикой, с педагогической деятельностью учителя математики. Должна быть осознана всеобъемлющая, универсальная роль математической логики в вопросах обоснования математики вообще и школьного курса математики в особенности.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
