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

Для формулы а ~ q\q2---qnb совокупность кванторов QuQb' -.Qii считаете? префиксом формулыЛ, а формула В — матрицей формулы а. Будем дополнительно считать, что матрица приведена к конъюнктивной нормальной форме. Очевидно, что формула а является противоречием тогда и только тогда, когда 1 а является логически общезначимой. Из свойств формул (см. § 5 гл. 2) следует, что формула Л является ло­ гически общезначимой тогда и только тогда, когда логически обще­ значимо замыкание В* формулы В. Как известно, замыкание В* фор­ мулы В получается приписыванием к В кванторов всеобщности по всем ее свободным переменным. Таким образом, при выяснении логически общезначимости либо противоречивости будем считать, что имеем дело только с замкнутыми формулами, ибо если это не так, то можно добиться этого, Осуществим следующие преобразования формул логики преди­ катов (формулы записаны с использованием связок 1, =>): 1) исключим знаки импликации, выразив их через 1, v ; 2) добьемся того, чтобы 1 относилась только к элементарным формулам; это можно сделать, используя правила перенесения отрицания через кванторы и законы де Моргана; 3) проведем стандартизацию (переименование) переменных для вынесения кванторов за скобки; 4) вынесем кванторы за скобки, т.е. получим предваренную нормальную форму: ^ ~ QiXi Q2X2-'QnxJS, здесь В ~ матрица формулы, а Q{XiQ2X2...QnX »- префикс (совокупность кванторов). Будем считать, что матрица приведена к конъюнктивной нормальной форме; 5) проведем исключение кванторов существования введением сколемовских функций (Skolem Т). Осуществим это следующим образом. Пусть Q\Xu Q2X2,:. , Q>^ „B, где Q^Xx, Q2X2,.-> Qrfin " кванторы всеобщно­ сти или существования. По]южим, что QiX,. - квантор существования 103