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

Из равносильностей (2.33)-(2.36) и (2.38)-(2.41) очевидным об­ разом следует, что для любой формулы можно добиться, чтобы снача­ ла были записаны кванторы, а затем формула, не имеющая кванторов, т.е. "вынести" кванторы за скобки. Здесь применены кавычки, так как для получения равносильных формул кванторы выносятся за скобки, возможно, оставаясь неизмененными, либо меняясь на двойственные, либо выносятся за скобки только после переименования связанных переменных (в самом кванторе и области его действия). При этом пе­ реименование переменных осуществляется по правилам, описанным в предыдущем параграфе. Формула вида; QxQi - QnB, где QuQb---,Qn - любая совокуп ность кванторов, а формула В не содержит кванторов, называется формулой в предваренной нормальной форме или в пренексной нор­ мальной форме. Для формулы А ~ Q\Qi..QnB совокупность кванторов QhQb - .Qn называется префиксом формулы а формула В - матрицей формулы А. Будем дополнительно считать, что матрица приведена к конъюнктивной нормальной форме. Из доказанных теорем легко следует следующая теорема. Теорема 2,9. Для каждой формулы логики предикатов суодествует равносильная ей формула в предваренной нормальной форме. Усердие все превозмогает. Козьма Прутков § 11. Вопросы и т е мы для самопроверки 1. Понятие предиката. 2. Кванторы. Использование кванторов и предикатов для сим­ волизации языка. 3. Термы, элементарные формулы и формулы логики предикатов. 76