Упрощение формул

Приведение бескванторной формулы к ДНФ и КНФ. Предваренная нормальная форма. Теорема о приведении. Пример: X =∀x¬∃y p(x,y)→∀x(q(x)→¬∃y p(x,y)). Замечание о порядке вынесения кванторов.

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

Например, если в формуле отсутствуют кванторы (бескванторная формула), то ее можно привести к ДНФ или КНФ. Такое преобразование всегда можно проводить в рамках языка логики высказываний, рассматривая любую элементарную подформулу как пропозициональную переменную.

Теорема 4.6. Всякая бескванторная формула эквивалентна некоторой ДНФ и некоторой КНФ.

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

Кванторы не мешают преобразованиям, если они в формуле собраны вместе. Формулу вида ∇x₁∇x₂ ... ∇x_n X, где X — бескванторная формула, называют предваренной или пренексной. В частности, любая бескванторная формула является предваренной. Предваренной (пренексной) формой данной формулы X называют любую предваренную формулу Y , логически эквивалентную X. Часть формулы Y без кванторных приставок называют матрицей предваренной формы.

Теорема 4.7 (о предваренной форме). Любая форма имеет предваренную форму.

Для доказательства нужно исходную формулу X заменить формулой X' со свойством чистоты переменных, а затем, применяя логические законы одностороннего пронесения кванторов, ” вытащить“ все кванторы за пределы формулы. Аккуратно доказательство следует проводить методом индукции по построению формулы. В самом деле, утверждение очевидно для элементарных формул (они все бескванторные). Пусть X = V ◦W, где ◦ — одна из двуместных логических связок, и формулы V и W имеют предваренные формы: V ≡ ∇v₁ ...∇v_m V', W ≡ ∇w₁ ...∇w_k W', где V' и W' бескванторные. Полагая, что X обладает свойством чистоты переменных, заключаем, что все переменные vi и wj различны, V 0 не содержит переменных w_j, а W' — переменных v_i. Тогда с помощью законов одностороннего пронесения кванторов получаем

X ≡ (∇v₁...∇v_mV')◦(∇w₁ ...∇w_k W'5) ≡∇v₁ ...∇v_m∇w₁ ...∇w_k (V'◦W').

Здесь мы воспользовались также правилом замены подформулы эквивалентной. Если формула X имеет вид X = ¬V , рассуждения аналогичны. Наконец, в случае X = ∇z V достаточно заменить V предваренной формой, чтобы получить предваренную форму X.

Пример 4.4. Рассмотрим формулу X = ∀x¬∃y p(x,y) →∀x(q(x) →¬∃y p(x,y)). Она не обладает свойством чистоты. Используя переименование с помощью двух новых переменных u и v, получим конгруэнтную (а потому эквивалентную) формулу

X' = ∀x¬∃y p(x,y)→∀u(q(u)→¬∃v p(u,v)).

Применяя одностороннее пронесение кванторов, последовательно получаем:

∀ x ¬ ∃ y p (x,y) → ∀ u (q (u) → ¬ ∃ v p(u, v)) ≡
≡ ∀ x ∀ y ¬ p (x,y) → ∀ u (q (u ) → ∀ v ¬ p (u, v)) ≡
≡ ∀ x ∀ y ¬ p (x, y) → ∀ u ∀ v (q (u) → ¬ p (u, v)) ≡
≡ ∃ x ∃ y ¬ p (x, y) → ∀ u ∀ v (q (u) → ¬ p (u, v))
≡
≡ ∃ x ∃ y ∀ u ∀ v ¬ p (x, y) → (q (u) → ¬ p (u, v))
.

Замечание. Вынесение кванторов может проходить в разном порядке. Следовательно, и в предваренной форме кванторные приставки могут идти в разном порядке: предваренная форма определена неоднозначно. В матрице предваренной формы все связки идут в том же порядке и без изменений. Она получается из исходной формулы удалением всех кванторных приставок.