Пренекс нормальная форма

Формула . находится исчисления предикатов в пренексе нормальная форма ( PNF ), если она записана как строка кванторов и связанных переменных , называемая префиксом , за которой следует часть без кванторов, называемая матрицей . Вместе с нормальными формами в логике высказываний (например, дизъюнктивной нормальной формой или конъюнктивной нормальной формой ) она обеспечивает каноническую нормальную форму , полезную при автоматизированном доказательстве теорем .

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

$\forall x\exists y\forall z(\phi (y)\lor (\psi (z)\rightarrow \rho (x)))$

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

$\forall x((\exists y\phi (y))\lor ((\exists z\psi (z))\rightarrow \rho (x)))$

логически эквивалентен, но не в пренексной нормальной форме.

Преобразование в предварительную форму

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

Соединение и дизъюнкция

Правила конъюнкции и дизъюнкции гласят, что

$(\forall x\phi )\land \psi$ эквивалентно $\forall x(\phi \land \psi )$ в (легком) дополнительном состоянии $\exists x\top$или, что то же самое, $\lnot \forall x\bot$ (это означает, что существует хотя бы один человек),

$(\forall x\phi )\lor \psi$ эквивалентно $\forall x(\phi \lor \psi )$;

и

$(\exists x\phi )\land \psi$ эквивалентно $\exists x(\phi \land \psi )$,

$(\exists x\phi )\lor \psi$ эквивалентно $\exists x(\phi \lor \psi )$ под дополнительным условием $\exists x\top$.

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

Например, на языке колец ,

$(\exists x(x^{2}=1))\land (0=y)$ эквивалентно $\exists x(x^{2}=1\land 0=y)$,

но

$(\exists x(x^{2}=1))\land (0=x)$ не эквивалентно $\exists x(x^{2}=1\land 0=x)$

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

Отрицание

Правила отрицания гласят, что

$\lnot \exists x\phi$ эквивалентно $\forall x\lnot \phi$

и

$\lnot \forall x\phi$ эквивалентно $\exists x\lnot \phi$.

Значение

Существует четыре правила импликации : два, которые удаляют кванторы из антецедента, и два, которые удаляют кванторы из консеквента. Эти правила можно получить, переписав импликацию $\phi \rightarrow \psi$ как $\lnot \phi \lor \psi$и применив вышеизложенные правила дизъюнкции и отрицания. Как и в случае с правилами дизъюнкции, эти правила требуют, чтобы переменная, выраженная количественно в одной подформуле, не появлялась свободной в другой подформуле.

Правила удаления кванторов из антецедента таковы (обратите внимание на изменение кванторов):

$(\forall x\phi )\rightarrow \psi$ эквивалентно $\exists x(\phi \rightarrow \psi )$ (при условии, что $\exists x\top$),

$(\exists x\phi )\rightarrow \psi$ эквивалентно $\forall x(\phi \rightarrow \psi )$.

Правила удаления кванторов из консеквента таковы:

$\phi \rightarrow (\exists x\psi )$ эквивалентно $\exists x(\phi \rightarrow \psi )$ (при условии, что $\exists x\top$),

$\phi \rightarrow (\forall x\psi )$ эквивалентно $\forall x(\phi \rightarrow \psi )$.

Например, когда диапазон количественной оценки представляет собой неотрицательное натуральное число (т. $n\in \mathbb {N}$), заявление

$[\forall n\in \mathbb {N} (x<n)]\rightarrow (x<0)$

эквивалентно логически утверждению

$\exists n\in \mathbb {N} [(x<n)\rightarrow (x<0)]$

Первое утверждение гласит, что если x меньше любого натурального числа, то x меньше нуля. Последнее утверждение гласит, что существует некоторое натуральное число n такое, что если x меньше n , то x меньше нуля. Оба утверждения верны. Первое утверждение верно, потому что, если x меньше любого натурального числа, оно должно быть меньше наименьшего натурального числа (ноля). Последнее утверждение верно, поскольку n=0 делает импликацию тавтологией .

Обратите внимание, что расстановка скобок подразумевает объем количественной оценки , что очень важно для смысла формулы. Рассмотрим следующие два утверждения:

$\forall n\in \mathbb {N} [(x<n)\rightarrow (x<0)]$

и его логически эквивалентное утверждение

$[\exists n\in \mathbb {N} (x<n)]\rightarrow (x<0)$

Первое утверждение гласит, что для любого натурального числа n , если x меньше n , то x меньше нуля. Последнее утверждение гласит, что если существует некоторое натуральное число n такое, что x меньше n , то x меньше нуля. Оба утверждения ложны. Первое утверждение не справедливо для n=2 , поскольку x=1 меньше n , но не меньше нуля. Последнее утверждение не выполняется для x=1 , поскольку натуральное число n=2 удовлетворяет условию x<n , но x=1 не меньше нуля.

Пример

Предположим, что $\phi$, $\psi$, и $\rho$являются формулами без кванторов, и никакие две из этих формул не имеют общих свободных переменных. Рассмотрим формулу

$(\phi \lor \exists x\psi )\rightarrow \forall z\rho$.

Рекурсивно применяя правила, начиная с самых внутренних подформул, можно получить следующую последовательность логически эквивалентных формул:

$(\phi \lor \exists x\psi )\rightarrow \forall z\rho$.

$(\exists x(\phi \lor \psi ))\rightarrow \forall z\rho$,

$\neg (\exists x(\phi \lor \psi ))\lor \forall z\rho$,

$(\forall x\neg (\phi \lor \psi ))\lor \forall z\rho$,

$\forall x(\neg (\phi \lor \psi )\lor \forall z\rho )$,

$\forall x((\phi \lor \psi )\rightarrow \forall z\rho )$,

$\forall x(\forall z((\phi \lor \psi )\rightarrow \rho ))$,

$\forall x\forall z((\phi \lor \psi )\rightarrow \rho )$.

Это не единственная форма пренекса, эквивалентная исходной формуле. Например, если в приведенном выше примере иметь дело с консеквентом перед антецедентом, пренексная форма

$\forall z\forall x((\phi \lor \psi )\rightarrow \rho )$

может быть получен:

$\forall z((\phi \lor \exists x\psi )\rightarrow \rho )$

$\forall z((\exists x(\phi \lor \psi ))\rightarrow \rho )$,

$\forall z(\forall x((\phi \lor \psi )\rightarrow \rho ))$,

$\forall z\forall x((\phi \lor \psi )\rightarrow \rho )$.

Расположение двух кванторов универсальности с одинаковой областью действия не меняет значения/истинного значения утверждения.

Интуиционистская логика

В правилах преобразования формулы в пренексную форму широко используется классическая логика. В интуиционистской логике неверно, что каждая формула логически эквивалентна предшествующей формуле. Связка отрицания — одно из препятствий, но не единственное. Оператор импликации также трактуется в интуиционистской логике иначе, чем в классической логике; в интуиционистской логике его невозможно определить с помощью дизъюнкции и отрицания.

Интерпретация BHK иллюстрирует, почему некоторые формулы не имеют интуиционистски эквивалентной пренексной формы. В этой интерпретации доказательство

$(\exists x\phi )\rightarrow \exists y\psi \qquad (1)$

— это функция, которая, учитывая конкретный x и доказательство $\phi (x)$, дает конкретное y и доказательство $\psi (y)$. В этом случае допускается значения y вычисление на основе заданного значения x . Доказательство

$\exists y(\exists x\phi \rightarrow \psi ),\qquad (2)$

с другой стороны, выдает одно конкретное значение y и функцию, которая преобразует любое доказательство $\exists x\phi$ в доказательство $\psi (y)$. Если каждый x удовлетворяет $\phi$ может быть использован для удовлетворяющего построения $\psi$ но такой y невозможно построить без знания такого x , то формула (1) не будет эквивалентна формуле (2).

Правила преобразования формулы в пренексную форму, которые не работают в интуиционистской логике:

(1) $\forall x(\phi \lor \psi )$ подразумевает $(\forall x\phi )\lor \psi$,

(2) $\forall x(\phi \lor \psi )$ подразумевает $\phi \lor (\forall x\psi )$,

(3) $(\forall x\phi )\rightarrow \psi$ подразумевает $\exists x(\phi \rightarrow \psi )$,

(4) $\phi \rightarrow (\exists x\psi )$ подразумевает $\exists x(\phi \rightarrow \psi )$,

(5) $\lnot \forall x\phi$ подразумевает $\exists x\lnot \phi$,

( x не появляется как свободная переменная $\,\psi$в (1) и (3); x не появляется как свободная переменная $\,\phi$ в (2) и (4)).

Использование предварительной формы

Некоторые исчисления доказательств будут иметь дело только с теорией, формулы которой записаны в пренексной нормальной форме. Эта концепция важна для разработки арифметической и аналитической иерархии .

Доказательство Гёделя его теоремы о полноте для логики первого порядка предполагает, что все формулы были преобразованы в предварительную нормальную форму.

Аксиомы Тарского для геометрии — это логическая система, все предложения которой могут быть записаны в универсально-экзистенциальной форме , особый случай пренексной нормальной формы, в которой каждый квантор универсальности предшествует любому квантору существования , так что все предложения могут быть переписаны в форме $\forall u$ $\forall v$ $\ldots$ $\exists a$ $\exists b$ $\phi$, где $\phi$это предложение, не содержащее квантора. Этот факт позволил Тарскому доказать разрешимость евклидовой геометрии .

См. также

• Арифметическая иерархия
• Гербрандизация
• Шолемизация

Ссылки

• Ричард Л. Эпштейн (18 декабря 2011 г.). Классическая математическая логика: семантические основы логики . Издательство Принстонского университета. стр. 108–. ISBN  978-1-4008-4155-4 .
• Питер Б. Эндрюс (17 апреля 2013 г.). Введение в математическую логику и теорию типов: к истине через доказательство . Springer Science & Business Media. стр. 111–. ISBN  978-94-015-9934-4 .
• Эллиот Мендельсон (1 июня 1997 г.). Введение в математическую логику, четвертое издание . ЦРК Пресс. стр. 109–. ISBN  978-0-412-80830-2 .
• Хинман, Питер (2005), Основы математической логики , AK Peters , ISBN  978-1-56881-262-5