Предварительная нормальная форма

---

Формула исчисления предикатов находится в пренексной ^[1] нормальной форме ( PNF ), если она записана в виде строки кванторов и связанных переменных , называемой префиксом , за которой следует бескванторная часть, называемая матрицей . ^[2]

Каждая формула классической логики эквивалентна формуле в предваряемой нормальной форме. Например, если , и являются бескванторными формулами с показанными свободными переменными, то${\ Displaystyle \ фи (у)}$${\ Displaystyle \ фунтов на квадратный дюйм (г)}$${\ Displaystyle \ ро (х)}$

находится в предваренной нормальной форме с матрицей , а${\displaystyle \phi (y)\lor (\psi (z)\rightarrow \rho (x))}$

Каждая формула первого порядка логически эквивалентна (в классической логике) некоторой формуле в пренексной нормальной форме. ^[3] Существует несколько правил преобразования, которые можно рекурсивно применять для преобразования формулы в пренексную нормальную форму. Правила зависят от того, какие логические связки появляются в формуле.

Эквивалентности действительны, когда не появляется как свободная переменная ; если появляется свободный в , можно переименовать связанный в и получить эквивалент .${\displaystyle x}$${\displaystyle \psi }$${\displaystyle x}$${\displaystyle \psi }$${\displaystyle x}$${\displaystyle (\exists x\phi )}$${\displaystyle (\exists x'\phi [x/x'])}$

потому что формула слева верна в любом кольце, когда свободная переменная x равна 0, а формула справа не имеет свободных переменных и ложна в любом нетривиальном кольце. Поэтому сначала будет переписано как , а затем помещено в пренексную нормальную форму .${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$${\displaystyle (\exists x'(x'^{2}=1))\land (0=x)}$${\displaystyle \exists x'(x'^{2}=1\land 0=x)}$

---