ВУЗ: Не указан
Категория: Не указан
Дисциплина: Не указана
Добавлен: 22.07.2019
Просмотров: 135
Скачиваний: 1
6. Лемма о дедукции для ИВ.
Лемма 1. Если – выводимая формула ИВ , то результат S() применения к одновременной подстановки S также есть выводимая формула ИВ .
Доказательство. Пусть одновременная подстановка S заключается в том, что попарно различные буквы a1, a2, …, ak одновременно заменяются в формуле на формулы 1, 2, …, k.
Возьмём множество всех тех и только тех букв, которые входят в запись хотя бы одной из формул 1, 2, …, k. Их конечное число. Пусть это будут (попарно различные) буквы x1, x2, …,xn. Тогда можно записать: 1 = 1(x1, x2, …, xn), …, k = k(x1, x2, …, xn). Так как алфавит ИВ (точнее, множество символов переменных) бесконечен, то можно взять попарно различные буквыb1, b2, …, bn, каждая из которых не совпадает ни с одной из букв a1, a2, …, ak, x1, x2, …, xn и не входит в запись формулы . А теперь произведём последовательно серию обычных (однократных) подстановок: сначала в формулу вместо буквы a1 подставим формулу 1(b1, b2, …, bn), затем вместо a2 в новую формулу подставим 2(b1, b2, …, bn) и т. д.; вместо ak – k(b1, b2, …, bn). Затем вместо букв b1, b2, …, bn последовательно подставим буквы x1, x2, …, xn. Легко видеть, что в конце мы получим S().
Осталось сослаться на доказанное ранее утверждение, что при применении (обычной, однократной) подстановки к выводимой формуле получается выводимая формула (в ИВ ).
7.Теорема 17 (О корректности ИВ). Всякая теорема исчисления высказываний есть тавтология.
Несложно проверить, что все аксиомы — тавтологии. Для примера проделаем это для самой длинной аксиомы (точнее, схемы аксиом) — для второй. В каком случае формула
(где —
некоторые
формулы) могла бы быть ложной? Для этого
посылка должна
быть истинной, а заключение —
ложным.
Чтобы заключение было ложным,
формула должна
быть истинной, а формула —
ложной.
Последнее означает, что истинна,
а ложна.
Таким образом, мы знаем, что , и истинны.
Отсюда следует, что и истинны,
и потому истинна
— противоречие. Значит, наша формула
не бывает ложной.
Корректность
правила MP также
очевидна: если формулы и всегда
истинны, то по определению импликации формула также
всегда истинна. Таким образом, все
формулы, входящие в выводы (все теоремы)
являются тавтологиями.
8.Теорема 18 (О полноте ИВ). Всякая тавтология есть теорема исчисления высказываний.
Начнем
с такого определения: множество
формул называется
совместным,если существует набор
значений переменных, при которых все
формулы из истинны.
Заметим, что формула является тавтологией тогда
и только тогда, когда множество, состоящее
из единственной формулы ,
не является совместным. Для случая
одной формулы есть специальный термин:
формула выполнима,
если существуют значения переменных,
при которых она истинна, то есть если
множество совместно. Тавтологии —
это формулы, отрицания которых не
выполнимы.
Множество
формул называется
противоречивым, если из него одновременно
выводятся формулы и .
Мы знаем, что в этом случае из него
выводятся вообще все формулы. (В противном
случае называется
непротиворечивым.)
9.Метод Квайна.
Метод Квайна основывается на применении двух основных соотношений.
Суть
метода заключается в последовательном
выполнении всех возможных склеиваний
и затем всех поглощений, что приводит
к сокращенной ДНФ. Метод применим к
совершенной ДНФ. Из соотношения поглощения
следует, что произвольное элементарное
произведение поглощается любой его
частью.
При склеивании всех конституент из S получим импликанту р. Последнее очевидно, поскольку операция склеивания обратна операции развертывания. Множество S конституент обязательно присутствует в совершенной ДНФ функции f поскольку р - ее импликанта.
|
Таблица 4.1.1 |
|
|
x4x3x2x1 |
f |
|
0000 |
0 |
10.Метод
резолюций.
Метод резолюций можно применять к любому множеству дизъюнктов с целью проверки их невыполнимости (противоречивости). Рассмотрим сначала метод резолюций для логики высказываний.
Литеры A и ~A называются контрарными, а множество {A, ~A} – контрарной парой.
Допустим, что в дизъюнкте C1 существует литера L1 , контрарная литере L2 в дизъюнкте C2. Вычеркнем литеры L1и L2 из дизъюнктов C1 и C2 соответственно и построим дизъюнкцию оставшихся дизъюнктов. Построенный дизъюнкт называется резольвентой дизъюнктов C1 и C2. Резольвента двух дизъюнктов является их логическим следствием. Резольвента двух единичных дизъюнктов (если она существует) – пустой дизъюнкт.
Резолютивный вывод C из множества дизъюнктов S есть такая конечная последовательность C1, C2, ..., Ckдизъюнктов, в которой каждый Ci (i=1, ..., k) или принадлежит S, или является резольвентой дизъюнктов, предшествующих Ci и Ck=C.
Дизъюнкт C может быть выведен или получен из S, если существует вывод C из S. Для невыполнимого множества дизъюнктов в результате последовательного применения правила резолюций получается пустой дизъюнкт.
Вывод из множества S пустого дизъюнкта называется опровержением (доказательством невыполнимости) S.