Введение
Формализм логики первого порядка. Формула исчисления предикатов находится в пренексной нормальной форме (PNF), если она записана как последовательность кванторов и связанных переменных, называемая префиксом, за которой следует часть, не содержащая кванторов, называемая матрицей. Вместе с нормальными формами в пропозициональной логике (например, дизъюнктивной нормальной формой или конъюнктивной нормальной формой), она предоставляет каноническую нормальную форму, полезную в автоматическом доказательстве теорем. Любая формула в классической логике логически эквивалентна формуле в пренексной нормальной форме. Например, если φ, ψ и θ – формулы, не содержащие кванторов, со свободными переменными, указанными в них, то
A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier free part, called the matrix. Together with the normal forms in propositional logic (e. g. disjunctive normal form or conjunctive normal form), it provides a canonical normal form useful in automated theorem proving. Every formula in classical logic is logically equivalent to a formula in prenex normal form. For example, if , , and are quantifier free formulas with the free variables shown then
находится в пренексной нормальной форме с матрицей φ, а
логически эквивалентна, но не находится в пренексной нормальной форме.
Переход на формат prenex
Любая формула первого порядка логически эквивалентна (в классической логике) некоторой формуле в пренексной нормальной форме. Существует несколько правил преобразования, которые можно рекурсивно применять для приведения формулы к пренексной нормальной форме. Эти правила зависят от логических связок, присутствующих в формуле.
Использование формы prenex
Некоторые доказательные исчисления работают только с теорией, формулы которой записаны в пренексной нормальной форме. Эта концепция важна для разработки арифметической и аналитической иерархий. Доказательство Гёделем теоремы о полноте для логики первого порядка предполагает, что все формулы были приведены к пренексной нормальной форме. Аксиомы Тарского для геометрии – это логическая система, предложения которой могут быть записаны в универсально-экзистенциальной форме, являющейся частным случаем пренексной нормальной формы, где каждый универсальный квантор предшествует любому экзистенциальному квантору, так что все предложения могут быть переписаны в виде , где – формула, не содержащая кванторов. Этот факт позволил Тарскому доказать, что евклидова геометрия разрешима.