Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 12
Текст из файла (страница 12)
Следовательно, и множество всех формул ϕi совместно,и выполняющий набор определяет бесконечную ветвь. (Конечно, мы «бьём из пушек по воробьям»: достаточно индук-[п. 3]Поиск контрпримера и исчисление секвенций53цией по i строить слово длины i, которое имеет бесконечное числопродолжений в дереве T .)Обычно утверждение леммы Кёнига формулируют так: если колония бактерий, возникшая из одной бактерии, никогда не вымирает полностью, то существует бесконечная последовательность бактерий, каждая следующая из которых получается при делении предыдущей.
[Аналогичная формулировка про людей осложняется возможностью клонирования, наличием двух полов и проблемами политкорректности.]2.3. Поиск контрпримера и исчисление секвенцийВ этом разделе мы построим другой вариант исчисления высказываний — так называемое исчисление секвенций. Такого рода исчисления изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов.
Ихназывают исчислениями генценовского типа (по имени Генцена, который начал их изучать). Ранее приведённый вариант исчислениявысказываний называют исчислением гильбертовского типа (по имени Гильберта, который использовал подобные исчисления в своейпрограмме формального построения математики).Для начала мы вообще не будем говорить ничего об аксиомах иправилах вывода, а рассмотрим задачу поиска контрпримера. Пустьдана некоторая формула A, про которую мы подозреваем, что она неявляется тавтологией, и хотим найти значения переменных, при которых она ложна. Как это делать? Естественно посмотреть на структуру формулы A.
Например, если A имеет вид B → C, то надо найтизначения переменных, при которых формула B истинна, а C ложна.Если A имеет вид B ∨ C, то надо найти значения переменных, прикоторых обе формулы B и C ложны. Если A имеет вид B ∧C, то надонайти либо значения переменных, при которых B ложна, либо значения переменных, при которых C ложна. Тем самым задача поискаконтрпримера для формулы A сводится к одной или нескольким задачам такого же или более общего вида (надо обеспечить истинностьили ложность одной или нескольких формул).Введём необходимую терминологию и обозначения. Будем называть секвенцией выражение Γ ` ∆, где Γ и ∆ — некоторые конечныемножества формул. (Пока что знак ` не имеет ничего общего с выводимостью, а только разделяет два множества формул.) С каждойсеквенцией Γ ` ∆ будем связывать задачу поиска таких значений54Исчисление высказываний[гл.
2]переменных, при которых все формулы из Γ истинны, а все формулы из ∆ ложны. Такой набор значений мы по некоторым причинамбудем называть контрпримером к секвенции Γ ` ∆. Легко проверить, что контрпримеры к секвенции Γ ` ∆ — это контрпримеры кформуле∧Γ → ∨∆,(∧Γ обозначает конъюнкцию формул из Γ, а ∨∆ — дизъюнкцию формул из ∆), то есть те наборы значений, при которых эта формулаложна. При этом конъюнкцию пустого множества формул мы считаем тождественно истинной, а дизъюнкцию — тождественно ложной.Наша исходная задача поиска контрпримера к формуле A может быть теперь сформулирована как задача поиска контрпримерак секвенции ` A. (Мы позволяем себе писать так для краткости;полностью следовало бы написать ∅ ` {A}.)Задачу поиска контрпримера к секвенции можно решать с помощью следующих правил. В каждом из приведенных правил нижнийзаказ на контрпример выполним, если и только если выполним одиниз верхних заказов, т. е. нижняя секвенция имеет контрпример тогда и только тогда, когда хотя бы одна из верхних секвенций имеетконтрпример.Γ ` A, ∆Γ ` B, ∆Γ ` A ∧ B, ∆A, B, Γ ` ∆A ∧ B, Γ ` ∆Γ ` A, B, ∆Γ ` A ∨ B, ∆A, Γ ` ∆B, Γ ` ∆A ∨ B, Γ ` ∆Γ, A ` B, ∆Γ ` A → B, ∆Γ ` A, ∆Γ, B ` ∆A → B, Γ ` ∆A, Γ ` ∆Γ ` ¬A, ∆Γ ` A, ∆¬A, Γ ` ∆Каждое из правил соответствует анализу одной из формул нижнейсеквенции.
Правила разделены на группы в зависимости от главнойсвязки анализируемой формулы, и согласованы с таблицами истинности для этой связки (что легко проверить). Запятая в правилахиспользуется как сокращение: Γ, A обозначает Γ ∪ {A} и т. д.Как пользоваться этими правилами? Возьмём секвенцию, к которой мы ищем контрпример. Выберем в ней одну из формул слеваили справа, посмотрим на главную связку и применим соответствующее правило (написав одну или две секвенции над исходной). Затем[п. 3]Поиск контрпримера и исчисление секвенций55к каждой из них снова применим одно из правил и т. д. Постепеннобудет расти «дерево поиска контрпримера», причём исходная секвенция будет иметь контрпример тогда и только тогда, когда одна изверхних секвенций (стоящих в «листьях») этого дерева имеет контрпример.Когда этот процесс обрывается? Это происходит в том случае,если все формулы в оставшихся секвенциях представляют собой переменные, тогда ни одно из наших правил поиска контрпримера неприменимо.
Но к этому моменту всё становится ясным: если в левой и правой части секвенции есть общая переменная, то к ней нетконтрпримера (одна и та же переменная не может быть одновременно истинной и ложной). Если же левая и правая часть такойсеквенции не пересекаются, то контрпример есть.Вот как это делается с секвенцией ` (p → q) → q:` p, qq`q(p → q) ` q` (p → q) → qКонтрпример найден: p и q ложны (он является контрпримером ксеквенции ` p, q).Напротив, поиск контрпримера к секвенции ` ((p → q) → p) → pне даёт результата:p ` p, qp`p` p, p → q(p → q) → p ` p` ((p → q) → p) → pЗдесь обе секвенции p ` p, q и p ` p не имеют контрпримеров. Следовательно, формула ((p → q) → p) → p является тавтологией.Построенный алгоритм можно одновременно рассматривать какдоказательство полноты некоторого «исчисления секвенций».Аксиомами исчисления секвенций будем называть секвенции, влевых и правых частях которых встречаются только переменные,причём некоторая переменная встречается в обеих частях.Правилами вывода в исчислении секвенций являются правила нашей таблицы.
Каждое из этих правил объявляет выводимой нижнюю секвенцию, если выводимы все верхние. (Процесс вывода естественно представлять в виде дерева, как в наших примерах, но можно развернуть и в последовательность секвенций.)56Исчисление высказываний[гл. 2]Теорема 23 (корректность и полнота исчисления секвенций). Секвенция выводима тогда и только тогда, когда она не имеет контрпримера. Аксиомы не имеют контрпримера. Если все верхние секвенции какого-то правила вывода не имеют контрпримера, то и нижняясеквенция не имеет контрпримера.
(Именно так мы подбирали правила: контрпример к нижней секвенции будет контрпримером к одной из верхних.) Следовательно, все выводимые секвенции не имеютконтрпримера.Обратно, пусть секвенция не имеет контрпримера. Тогда описанный процесс поиска контрпримера обрывается на аксиомах и темсамым даёт её вывод. В частности, если формула A является тавтологией, то секвенция` A выводима в исчислении секвенций. Это обстоятельство можноиспользовать для ещё одного доказательства полноты исчислениявысказываний (в стандартной, гильбертовской форме).
В самом деле, для каждой секвенции Γ ` ∆ рассмотрим представляющую еёформулу, то есть формулу ∧Γ → ∨∆ (в левой и правой частях стоят конъюнкция и дизъюнкция формул из Γ и ∆ соответственно).Теперь индукцией по построению вывода в исчислении секвенцийнадо доказать такой факт: если секвенция выводима в исчислениисеквенций, то представляющая её формула выводима в (обычном)исчислении высказываний.Это требует довольно хлопотной проверки, впрочем.
Сначала надо проверить, что конъюнкция и дизъюнкция доказуемо ассоциативны, и потому всё равно, как расставлять скобки в формуле, представляющей секвенцию. Затем полезно убедиться, что правила, связанные с отрицанием (два последних правила таблицы) можно применять в обе стороны, не меняя выводимости соответствующей формулы. Другими словами, надо проверить, что формулыΓ → (∆ ∨ A) и(Γ ∧ ¬A) → ∆,а также формулыΓ → (∆ ∨ ¬A) и(Γ ∧ A) → ∆выводимы одновременно (здесь Γ и ∆ можно считать формулами, ане множествами формул, расставив скобки надлежащим образом).После этого мы можем переносить формулы из одной части в другую (меняя их на противоположные), и потому можем считать одно[п.
3]Поиск контрпримера и исчисление секвенций57из множеств Γ и ∆ пустым, если это нам удобно. Теперь ссылка налемму о дедукции и уже известные нам свойства выводимости завершает рассуждение.30. Провести это рассуждение подробно.Естественно возникает вопрос — чем уж так интересно исчисление секвенций? Какая, собственно говоря, разница — иметь дело с секвенциями или с формулами, раз всякую секвенцию можно представить формулой? Принципиальное различие тут в следующем.
Правила вывода в исчислении секвенций таковы, что в их верхнюю частьвходят только подформулы формул, встречающихся в нижней части.Поэтому в выводе какой-то секвенции не может встретиться ничегопринципиально нового, чего не было в самой секвенции.
В гильбертовском исчислении это далеко не так: мы можем вывести формулуB из формул A → B и A, при этом формула A может быть совершенно произвольной. Это же различие объясняет, почему поисквывода снизу вверх (как можно теперь называть то, что раньше называлось поиском контрпримера — мы находим либо контрпример,либо вывод) для исчисления секвенций происходит сравнительно однозначно (мы можем по-разному выбирать расчленяемую формулу,но и только), в то время как искать вывод в обычном исчислениивысказываний, начав с интересующей нас формулы B и смотря, изчего бы она могла получиться, не удаётся (если только не перебиратьвсе формулы подряд).Заметим, что добавление к исчислению секвенций уже упоминавшегося правила сеченияΓ ` ∆, AΓ, A ` ∆Γ`∆нарушает свойство «подформульности», так как формула A можетбыть никак не связана с нижней секвенцией.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
