2. элементы логики предикатов формулы логики предикатов и их преобразование - страница №2/4
2.2. Приведение формул к предваренной
нормальной форме (ПНФ)
Сводка теории
Определение
Предваренной (или
пренексной) формулой называется формула вида , где
Qi суть кванторы, а формула
A (называемая
матрицей предваренной формулы) уже кванторов не содержит.
Если и B – предваренная формула, то B называют предваренной (нормальной) формой (ПНФ) формулы A.
В частности, не исключается и случай
n =
0, т.е. бескванторная формула также считается предваренной.
Теорема 2.1
Для всякой формулы существует ПНФ.
Доказательство. С помощью основных логических законов устраняем в формуле все знаки логических операций, кроме (если таковые имеются).
К полученной формуле последовательно применяем в произвольном возможном порядке преобразования двух типов: А и В.
Преобразование типа А. Находим в формуле некоторую часть (подформулу)
Ф, имеющую вид , или , или , или , где
F,
G(x) – какие-то формулы и
G(x) содержит свободную переменную
x. Пусть для определенности (в остальных случаях все делается точно так же).
Преобразуем Ф следующим образом: проверяем, содержит ли F переменную x, и если нет, то замещаем Ф на (соотношение (III.1)), если да, то заменяем все вхождения x в вхождениями какой-либо новой переменной, скажем, t, не встречающейся в нашей «боль-шой» формуле (соотношение (IV.1)), и затем заменяем на . Таким же образом поступаем с подформулами остальных трех видов (это возможно ввиду коммутативности конъюнкции и дизъюнкции).
Преобразование типа В. Находим в формуле некоторую подформулу, имеющую вид (или ), где
G(x) – формула со свободной переменной
x, и заменяем ее на (соответственно на ) по соотношениям (II.1), (II.2).
Применяя преобразования типов А и В, мы шаг за шагом «вытаскиваем наружу» все кванторы и, в конце концов, приходим к формуле, в которой ни один квантор не стоит внутри конъюнкции или дизъюнкции, или вслед за отрицанием. Но в такой формуле квантор может стоять только либо вслед за другим квантором, либо в самом начале формулы, т.е. получена ПНФ для исходной формулы.
Замечания
1) В доказательстве указан практический способ приведения формул к ПНФ. При фактическом приведении удобно «по пути» устранять двойные отрицания всякий раз, когда они возникают (а также производить любые другие упрощения, если они возможны).
2) В силу соотношений II. 1 – II 2 отрицание формулы равносильно формуле , где – квантор, «противоположный» Qi .
Помимо рассмотренных предваренных формул (и соответственно ПНФ), иногда вводят и более специальные виды нормальных форм, например,
нормальную форму Сколема, которая имеет предваренный вид (т.е. все кванторы вынесены в начало формулы), не содержит функциональных символов и все ее кванторы всеобщности предшествуют кванторам существования либо, наоборот, все кванторы существования предшествуют кванторам всеобщности (понятно, что к такой форме легко перейти от ПНФ, используя свойства кванторов группы II).
Примеры
Пример 2.5
Привести формулы к ПНФ:
а) ;
б) .
Решение
Преобразуем формулы, устраняя «лишние» логические связки и «опуская» отрицания на предикаты, а затем последовательно «вытаскива-ем» кванторы из-под логических связок с помощью преобразований типа А или типа В, при необходимости применяя переименование переменных.
а)
.
б)
.
Задачи
2.8. Привести к ПНФ:
а) ;
б) ;
в) ;
г) ;
д) ;
е) ;
ж) ;
з)
.
Контрольные вопросы
-
Дайте общее определение предиката. Что такое «местность» предиката? тождественно-истинный предикат? тождественно-ложный предикат?
-
Как определяются логические операции над предикатами?
-
Чем отличается формула логики высказываний от формулы логики предикатов?
-
Что такое интерпретация формулы логики предикатов? Параметр формулы? Замкнутая формула?
-
Что называют коллизией переменных?
-
Какие формулы логики предикатов называют равносильными? Конгруэнтными? Тождественно-истинными? Тождественно-ложными?
-
Дайте определение кванторов существования и всеобщности в случае одноместного и многоместного предиката.
-
Попробуйте доказать свойства кванторов.
-
Какие понятия формального языка выполняют роли, аналогичные тем, которые в естественном языке выполнятся: подлежащим? Сказуемым? Дополнениями? Местоимением? Союзами?
-
Что такое терм? Функциональная сложность терма?
-
Что такое формула? Логическая сложность формулы?
-
Что такое предваренная нормальная форма?
3. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ И ИСЧИСЛЕНИЕ
ПРЕДИКАТОВ
3.1. Общее представление об исчислении высказываний
Сводка теории
Таблицы истинности позволяют ответить на многие важные вопросы, касающиеся логических связок: является ли данная формула тавтологией, противоречием или ни тем и ни другим; влечет ли она логически другую данную формулу или являются ли две формулы логически равносильными.
Более сложные вопросы логики уже не могут быть решены с помощью истинностных таблиц или каких-либо других подобных эффективных процедур. Поэтому используется другой метод – аксиоматический.
При формализации математической теории полностью отвлекаются от ее содержания. Теоремы воспринимаются просто как формулы, которые могут быть выведены по определенным правилам. Поэтому формальные теории иначе называют исчислениями. О знаках и формулах исчисления приходится, однако, рассуждать содержательно: так, рядом с формальной теорией возникает «метатеория», которая тоже пользуется некоторыми обозначениями. Эти обозначения метатеории следует строго отличать от знаков и формул, относящихся к собственно формальной теории.
Существует много вариантов формализации логики высказываний. Опишем подробнее один из них; назовем его «теория L». Формальная (аксиоматическая) теория L считается определенной, если выполнены следующие условия:
1) Задано некоторое счетное множество символов теории L (языка теории). Основные символы теории L суть: пропозициональные буквы , ..., , ... ; логические связки , , , ; скобки (, ).
Конечные последовательности символов теории называются выражениями теории L.
2) Имеется подмножество выражений теории L, называемых формулами теории и определяемых индуктивно с помощью следующих двух пунктов:
-
пропозициональные буквы суть формулы L;
-
если A и B – формулы, то формулами являются и следующие выражения: , , , .
3) Выделено некоторое множество формул, называемых
аксиомами теории
L, в рассматриваемом варианте теории их десять:
, (ив1)
, (ив2)
, (ив3)
, (ив4)
, (ив5)
, (ив6)
, (ив7)
, (ив8)
, (ив9)
(ив10)
Здесь – конкретные пропозициональные переменные, так что (ив1) – (ив10) есть список из десяти конкретных формул языка L.
4) Принимаются правила вывода, по которым можно из уже установленных теорем получать новые. В теории L – два таких правила вывода.
Первое правило имеет вид (MP) .
Это правило, называемое modus ponens (правило заключения), утверждает, что если формулы и установлены как теоремы, то формула также является теоремой.
Второе правило имеет вид: (S) .
Здесь суть формулы, – попарно различные пропозициональные буквы. Через обозначен результат одновременного замещения всех вхождений букв в на формулы соответственно. Отметим, что это правило подстановки (S) можно применять и к пропозициональным буквам , которые вовсе не входят в . В этом случае соответствующее никуда не подставляется и просто не играет никакой роли.
Выводом назовем любую конечную последовательность формул , ,...,, такую, что каждая формула этой последовательности есть либо аксиома, либо совпадает с какой-либо предыдущей формулой этой последовательности, либо получается из каких-то предыдущих формул этой последовательности с помощью одного из правил вывода. Скажем, что вывод ,,..., является выводом своей последней формулы , и формулу назовем выводимой, или, что то же самое, теоремой теории. Будем записывать это в виде: L A или просто A.
В дальнейшем будем употреблять сокращенный вывод, когда в качестве могут стоять теоремы теории L, полученные раньше, имея в виду, что мы всегда можем дополнить вывод, вставляя недостающие его отрезки.
Примеры
Пример 3.1
Вывести в теории L теорему (AA).
Решение
Возьмем в качестве примера первой формулы вывода аксиому (ив2). Применим к ней правило подстановки в виде:
( A, (AA), A).
Получим
((
A((
AA)
A))((
A(
AA))(
AA))). (а)
Из аксиомы (ив1) подстановкой ( A, (AA)) получим:
(
A((
AA)
A)). (б)
Применим правило (MP) к (а) и (б):
((
A(
AA))(
AA)). (в)
Из аксиомы (ив1) подстановкой ( A, A) получим:
((
A(
AA))). (г)
Применяя (МР) к (в) и (г), окончательно получим:
(
AA). (д)
Пример 3.2
Построить вывод в ИП для формулы (AA).
Решение
Для удобства вывод запишем сначала в виде столбцов формул, а затем в виде дерева. Столбцы формул:
А((
А А)
А), (а)
это пример схемы аксиом (ип1);
(А(( А А) А))(( А( А А))( А А)), (б)
это пример схемы аксиом (ип2);
(А( А А))( А А), (в)
получается по (MP) из (а) и (б);
А(
А А), (г)
это пример схемы аксиом (ип1);
А А (д)
п
олучается из (в) и (г) по (MP).
Соответствующее дерево вывода имеет вид:
Задачи
3.1. Являются ли выводами в ИВ следующие последовательности формул:
а) ;
б) , , ;
в) , , В?
3.2. Вывести в ИВ формулы:
а) ;
б) .
следующая страница >>
2. элементы логики предикатов формулы логики предикатов и их преобразование - umotnas.ru o_O