Математическая логика и теория алгоритмов

Доказательство. Пусть формула (3.4) является противоречием, тогда ее отрицание является тавтологией: [^1 • &/4да&1 jB). (3.6) Очевидно, имеем 1 ( A i & A i & . . В У 1 iAi&A2&...&A^)vB ~(Ai<&A2&..• В. Следовательно, утверяодение (3.6) можно записать в виде: Теперь, используя утверждение (3.2) теоремы 3.3 и утверждение (3.8), получим требуемое утверждение (3.5). Теорема доказана. Используя утверждения (3.2) и (3.3) теоремы 3,3, можно полу­ чать следствия из заданного множества формул следующим образом. Для заданного множества формул Ai, Аг ,...Ат, >п>1, строим их конъюнкцию: C=Ai&A2&---&A „. Для С находим с.к.н.ф.: С= Di&Di&.-.&Dk, здесь Д, l<i<k, - элементарные суммы (дизъюнкты). Теперь по указанной теореме 3.3 получаем, что каждый дизъюнкт Df, 1< i<к, а такисе их конъюнкции являются следствиями из Ai,A2,-..'Am, т. е. имеем: Ai, Aii.-.^m }=A для любого /, 1< i<к; ^1,^ 2 vH » i 1= . для любого г, 1< Г< А: и любых 5/, s2,.:,sr,l^sb s2,...,sr<k. Заметим, что для формул логики предикатов понятие логическо­ го следствия из данной формулы (данных формул) введено в § 6 гл. 2. Нетрудно убедиться, что теоремы 3.1 - 3.4 остаются в силе и для формул логики предикатов, в частности, теорема 3.2 для формул логики предикатов уже доказана (см. теорему 2.1). 1= (Ai&A2&...&A, „}=:> В. (3.7) Из (3.7) по теореме 3.2 получаем, что (3.8) 91