Предваренная формула

- формула узкого исчисления предикатов (УИП), имеющая вид [img: http://localhost:8080/file/041739-62.jpg] где Qi обозначает квантор всеобщности [img: http://localhost:8080/file/041739-63.jpg] или квантор существования $, переменные х i, xj различны при [img: http://localhost:8080/file/041739-64.jpg] и Y - формула, не содержащая кванторов. П. ф. наз. также предваренными нормальными формами или пренексными формами. Для всякой формулы ф языка УИП можно найти П. ф., логически эквивалентную в классич. исчислении предикатов формуле ф. Процесс нахождения П. ф. основан на следующих эквивалентностях, выводимых в классич. УИП: [img: http://localhost:8080/file/041739-65.jpg] где х' - любая переменная, не входящая свободно в формулы j(x), Y, и j(x') получается из j(х). заменой всех свободных вхождений хна х';переменная у не входит свободно в [img: http://localhost:8080/file/041739-66.jpg]. Чтобы применять приведенные эквивалентности, надо предварительно выразить логич. связки через [img: http://localhost:8080/file/041739-67.jpg] и [img: http://localhost:8080/file/041739-68.jpg]; затем, применяя эти эквивалентности, постепенно передвигать все кванторы влево. Получающаяся в результате П. ф. наз. предваренной формой данной формулы.