Кузнецов О.П., Адельсон-Вельский Г.М. - Дискретная математика для инженеров (1048837), страница 47
Текст из файла (страница 47)
и фУнкЦиональных бУкв 1гг, Ггг, ..., Ц, ..., а также знаков логических свЯзок чг, Й, ~, -э, квантоРов )г, В и скобок (,). Верхние индексы предикатных и функциональных букв указывают число аргументов, их нижние индексы служат для обычной нумерации букв. Переменные высказывания в'исчисление предикатов вводятся либо непосредственно как пропозициональные буквы АьАИ ..., либо как 0-местные предикаты Р",, Р,', ..., т.е. как предикаты без предметных переменных.
2. Фо р мул ы. Понятие формулы определяется в два этапа. 1) Термы; а) предметные переменные и константы являются термами; б) если )" — функциональная буква, а 1„,, 1„— термы, то ("(1г, ..., 1„) — терм. 2) Формулы: а) если Рь — предикатная буква, а гг, ..., 1 — термы, то Р" (1ь „,, 1„) — формула; все вхождения предметных переменных в формулу вида Р" ((ь..., 1 ) называются свободными; б) если Рг, Рг — формулы, то формулами являются )Рг, (Рг-'Рг), (Рг~ггРг), (РгйРг); все вхождения переменных, свободные в Рь Рм являются свободными и в указанных четырех видах формул; в) если Р(х) — формула, содержащая свободные вхождения переменной х, то ТгхР(х) и ВхР(х) — формулы; 228 в этих формулах все вхождения переменной х называются связанными; вхождения остальных переменных в г остаются свободными.
Фуикциональвые буквы и термы введены «впрок» для целей различных прикладных исчислений предикатов. Чистое исчисление предикатов строится для произвольной предметной области; структура этой области н связи между ее элементами не имеют значения, поэтому в нем функциональные буквы и термы не обязательны '. В прикладных исчислениях (например, в формальной арифметике) структура предметнов области оказывается существенной, поэтому в исчисленви необходимо иметь средства для описания связей между элементами, т.е.
функций и отношений, определенных на области. Отношениям соответствуют предикатные буквы, функциям — функциональные буквы. Термы — это имена элементов предметной области, построенные с помощью функций. Они могут быть постоянными (если они построены иэ предметных констант) и переменными. Формулы — это высказывания о термах.
Например, 4+5 ° 3 — постоянный терм любого нешслсния, содержащего функциональные буквы + и °, а х+7 — переменный терм этого жс исчисления, Выражение 4+5 ° 3=к+7 — это переменное высказывание, полученное подстановкой двух термов в двухместный предикат равенства; его истинность зависит от значения переменной х. 3. А к с и о м ы и с ч и с л е н и я п р е д и к а т о в делятся на две группы: 1) аксиомы исчисления высказываний (можно взять любую из систем 1 или П); 2) две следующие предикатные аксиомы: Р1, тгхР(х)- Р(у); Р2. Р(у)-» Вхр(х).
В этих аксиомах У(х) — любая формула, содержащая свободные вхождения х, причем ни одно из пих пе находится в области действия квантора по у; формула Р(у) получена из Р(х) заменой всех свободных вхождений х на у. Чтобы пояснить существенность требования к вхождениям х в Р, рассмотрим в качестве Г(х) формулу БУР(У, х), где это требование нарушено: свободное вхождение х находится в области действия чу. Подстановка этой формулы в аксиому Р1 дает формулу тухЧУР(У, х) — ЧУР(У, у).
Если ее проинтерпретировать на множестве Аг натуральных чисел с предикатом Р «быть больше», то получим высказывание: «еслн для всякого х найдется у больший, чем В частности, приводимые далее аксиомы Р! и Р2 не учитыва>от наличия термов в формулах. Для исчисления с термами и функциональными буквами эти аксиомы имеют вид Р!' и Р2', 229 х, то найдется у, больший самого себя».
Посылка этой импликации истинна на У, а ее заключение ложно, и, следовательно, само высказывание ложно. 4. Правила вывода: 1) правило заключения (Модна Ропепз) — то же, что и в исчислении высказываний; 2) правило обобщения (т( — введения): Р-~6 (х) Е-~.~хп (х) где О(х) содержит свободные вхождения х, а Р их не содержит; 3) правило В в введения: о (х)-+Р цхо (х)-~К при тех же требованиях к Р и 6, что и в предыдушем пра. виле. Нарушения этих требований могут привести к ложным выводам из истинных высказываний. Пусть, например, Р(х) — предикат «х делится на 6», (,)(х) — предикат «х делится на 3», Высказывание Р(х)-»Я(х), очевидно, истинно для любого х, однако применение к нему правила обобщения дает высказывание Р(х)- )7х()(х), не являющееся всегда истинным.
Если же к Р(х)- ()(х) применить правило В-введения, то получим ВхР(х)-»Я(х), нз которого путем (уже корректного!) применения правила обобщения получим высказывание ВхР(х)-». ((х(,)(х), ложное на множестве натуральных чисел. Приведенные здесь аксиомы и правила вывода содержатся в [36, 37[. Возможны и другие системы, аксиом и правил (см., например, [39, 43)).
В частности, в [43) последовательно проводится принцип минимизации числа логических операторов, который в исчислении высказываний оставляет лишь связки ~ и -» (что отражено в системе аксиом П). В исчислении предикатов он выражается в том, что квантор Вх не считается самостоятельным символом, а рассматривается как сокращение выражения ))ух ~: например, выражение ВхР(х) эквивалентно выражению ~~х )Р(х). Читатель, вероятно, уже заметил, что правило подстановки окончательно исчезло из изложения; тем самым из двух возможных истолкований системы аксиом (о чем шла речь в исчислении высказываний) выбрано второе, при ко- 230 тором правило подстановки отсутствует, а вместо аксиом рассматриваются схемы аксиом.
Фактически этот выбор произошел уже тогда, когда аксиомы Р1 и Р2 были сопровождены словесным описанием ограничений на вхожде. ния переменных. Тем самым аксиомы перестали быть выражениями исчисления, а вместе с этим словесным текстом превратились в метаописания множества формул, являющихся аксиомами, т.е. в схемы аксиом, Построение исчисления преднкатов с правилом подстановки существенно более громоздко нз-за необходимости различать свободные и связанные вхождения предметных переменных (см., например, (15)).
Поэтому в большинстве современных книг по логике используется подход со схемами аксиом. Предполагая, что после знакомства с исчислением высказываний разница между переменными и метаперемениымн уже усвоена, пе будем больше употреблять готические буквы; в качестве метапеременных, обозначающих формулы, в этом разделе будут использоваться буквы Р и 6. Приведем теперь примеры вывода в исчислении предикатов. Пример 6.3. а. Покажем, что в исчислении предикатов из выводи мости формулы Р(х), содержащей свободные вхождения х, ни одно из которых не находится в области действия квантора по у, следует выводимость Р(у).
Это утверждение представляет собой правило переименования свободных переменных. 1. '„— Р(х) (по условию). 2. Р(х)-+(6-ьР(х)) (аксиома П 1; в качестве 6 выбираем любую доказуемую формулу, не содержащую свободных вхождений х: ее доказуемость понадобится на шаге 5, а ограничение на х — на шаге 4). 3. 6-~-Р(х) (правнло заключения к шагам 1 и 2). 4, 6-+дахр(х) (правило обобщения к шагу 3).
5. тухР(х) (правило заключения к 6 и шагу 4). 5. Р(у) (правило заключения к шагу 5 и аксиоме Р!). б. В исчислении предикатов нз выводимости тухР(х) следует выводимость тгуР(у), а из выводимости ВхР(х)— выводимость дур(у) прн условии, что Р(х) не содержит свободных вхождений у и содержит свободные вхождения х, ни одно из которых не входпт в область действия кван- тора по у (правило переименования связанных переменнь!х) .
Докажем это правило для квантора общности. 1. ( — !гхР(х) (по предположению). 231 2. ьхР(х)-+Р(р) (аксиома Р!). 3. у(х)Р(х) — ~ууР(у) (правнло обобщения к шагу 2). 4. )~уР(у) (правило заключения к шагам 1 и 3). Доказательство для В совершенно аналогично, но использует аксиому Р2 и правило В-введения. Выводимость и истинность. Эквивалентные преобразования. Теорема 6.5.
Всякая доказуемая формула исчисления предикатов тождественно-истинна (общезначима — см. $3.4) . Эта теорема доказывается аналогично теореме 6.3: непосредственно проверяется общезначимость аксиом и показывается, что правила вывода сохраняют общезначн. мость, т. е.
их применение к общезначимым формулам снова дает общезначимые формулы. П Теорема 6.6. Всякая общезначимая предикатная формула доказуема в исчислении предикатов. Доказательство этой теоремы намного более сложно; здесь оно опускается. В конце раздела об исчислении высказываний вскользь было упомянуто о том, что всякому эквивалентному соотношению Р= б в булевой алгебре соответствует доказуемая эквивалентность ) — Р - 6 в исчислении высказываний. Из теорем 6.5 и 6.6 следует, что между соотношениями содержательной логики предикатов (см. 5 3.4) и формальными эквивалентностями в исчислении предикатов имеется аналогичное соответствие (напомним, что Р О рассматривается как сокращение (Р- 6)Ь(6-+Р) ).
На нем имеет смысл остановиться подробнее. Дело в том, что доказательства общезначимости в логике предикатов существенно сложнее, чем в логике высказываний (об этом уже говорилось в гл. 3), и поэтому формальный вывод эквивалентностей становится важным способом нх получения. Теорема 6.7. Пусть Р(А) — формула, в которой выделено вхождение формулы А; Р(В) — формула„полученная из Р(А) заменой этого вхождения А формулой В, Тогда если )-А В, то ) — Р(А) Р(В). Эта теорема формулирует для исчисления предикатов правило, аналогичное правилу замены эквивалентных подформул в алгебрах (см. гл, 3). Благодаря ему можно получать доказуемые эквивалентности в исчислении, не строя их непосредственного вывода.