Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

, Г,А^В,Л , Г ^ А,Л Г,В->Л д) е) Г^А^В,Л А^В,Г^Л А,Г^Л Г^А,Л т; : : V Г —^—А, л —А, Г —у Л Запятая в правилах используется как сокращение: Г, А обозначает Г vj{А}. Каждое правило применяется для анализа одной из формул нижней секвенции. Отметим, что правила выводов в исчислении гильбертовского типа применялись к формулам. Правила преобразования (вывода) в исчислении секвенций применяются не к формулам, а к секвенциям. Для построения доказательства строится дерево вывода, называемое также деревом поиска контрпримера. Как пользоваться этими правилами? Возьмём секвенцию, к которой мы ищем контрпример. Выбираем в ней последовательно (лексографически) формулу сначала слева затем справа секвенции, посмотрим на главную связку и применим соответствующее правило, написав одну или две секвенции над исходной. Затем к каждой из них снова применим одно из правил и т. д. Постепенно будет расти «дерево поиска контрпримера», причём исходная секвенция будет иметь контрпример тогда и только тогда, когда одна из верхних секвенций (стоящих в «листьях») этого дерева имеет контрпример. Когда этот процесс обрывается? Это происходит в том случае, если все формулы в оставшихся секвенциях представляют собой атомы (переменные), тогда ни одно из наших правил поиска контрпримера не применимо. По к этому моменту всё становится ясным: если в левой и правой части секвенции есть общая переменная, то к ней нет контрпримера (одна и та же переменная не может быть одновременно истинной и ложной). Если же левая и правая часть такой секвенции не пересекаются, то контрпример есть. Рассмотрим пример 1. В гильбертовском исчислении высказываний (теории L) было доказано, что для любой формулы А формула А^А является теоремой. Выясним будет ли секвенция -^А^А доказуемой в G'. Используя правило (д) из (4.27) дляГ= { 0 } и zl={0} получим, что А^А, а эта секвенция является аксиомой и контрпримера не имеет. Следовательно, секвенция -^А^А доказуема в G'. Рассмотрим пример 2. Пусть имеем секвенцию -^А^(В^А) Тогда, используя правило д) из (4.27) получим (здесь Г= {0} , zl={0}): А (В^А) 133