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

let Ai,...,An be the label of node; let S be the one-node tree labeled with for i: — 1 to /и do if nonatomic(Ai) then S := the. new tree obtainedfrom S by applying to the descendant ofAi in every nonaxiom leaf of S the left rule applicable to Ai endif endfor; for i 1 —I to n do if nonatomic(Bi) then S := the new tree obtainedfrom S by applying to the descendant of Bi in every nonaxiom leaf of S the right rule applicable to Bi endif endfor; T : = do substitution(T,node S} end Отметим, что процесс построения дерева вывода может быть и иным, например, построение дерева вглубь. Имеет место следующая теорема. Теорема 4.11 (корректность и полнота исчисления секвенций). Секвенция выводима тогда и только тогда, когда она не имеет контрпримера. Доказательство. Конечность дерева вывода следует из конечности множеств формул входящих в секвенцию. Аксиомы не имеют контрпримера. Если все верхние секвенции какого-то правила вывода не имеют контрпримера, то и нижняя секвенция не имеет контрпримера. Именно так подбирались правила: контрпример к нижней секвенции будет контрпримером к одной из верхних. Следовательно, все выводимые секвенции не имеют контрпримера . Обратно, пусть секвенция не имеет контрпримера. Тогда описанный процесс поиска контрпримера обрывается на аксиомах и тем самым даёт её вывод. Если формула В является тавтологией, то секвенция ^ В выводима в исчислении секвенций. Обратно, если секвенция В имеет контрпримера, то секвенция выводима в G' и В является тавтологией. Положим, что мы начали строить контрпример к секвенции вида 136