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

Теперь вновь используем это правил д), но с В результате получим: А,В^А Полученная секвенция является аксиомой и не имеет контрпримера, следовательно, исходная секвенция ^ А^(В^А) выводима. Отметим, что формула А^(В^А) является тавтологией и выводима в формальной аксиоматической системе - теории L. Описанный вывод секвенции представляют в виде следующего дерева вывода, которое читается снизу вверх (от корня к листьям, причем корень внизу): А,В^А А^(В^А) -^А^(В^А) Рассмотрим пример 3. Пусть имеем секвенцию: —> (C^D)^D Используя правило д) из (4.27) получим (здесь Г= {0} , А={0}): C^D^D Теперь используя правил е), но с zl = {D}, получим две секвенции: ^ С, D и D^D Вторая секвенция является аксиомой и не имеет контрпримера, но первая имеет контрпример: С= D=JI. Тогда секвенция -^(C^D)^D не выводима. Эти выкладки представляются следующим деревом вывода, которое читается снизу вверх: ^С,Р Р^Р С^Р^Р -^(С^Р)^Р) Легко видеть, что формула (С^Р) ^Р не является тавтологией и не выводима и в формальной аксиоматической системе - теории L. Рассмотрим пример 4. Пусть имеем секвенцию ^ ((А^В)^А)^А Поиск контрпримера (вывода) можно развернуть и в последовательность секвенций, которую запишем в обычном для исчисления секвенции виде, именно, в виде дерева, как в рассмотренных примерах 2 и 3: А^А,В — А^А А,А^ В (А^В)^А^А -^((А^В)^А)^А Здесь обе секвенции А А,В и А ^ А, находящиеся в листьях дерева, являются аксиомами и не имеют контрпримеров. Следовательно, формула 134