Теорема Эрбрана

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

Говорят, что формула находится в предваренной нормальной форме, если все кванторы в ней вынесены налево, то есть если она имеет вид$$Q_1 \xi_1 \ldots Q_k \xi_k \varphi,$$ где $$Q_1,\dots,Q_k$$ — кванторы всеобщности или существования, $$\xi_1,\dots,\xi_k$$ — переменные, а $$\varphi$$ — бескванторная формула. Эта формула может иметь параметры (если формула $$\varphi$$ имеет параметры, отличные от $$\xi_1,\dots,\xi_k$$ ).

Основной результат этого раздела гласит, что всякая формула (доказуемо) эквивалентна некоторой формуле в предваренной нормальной форме (предваренной формуле). Мы докажем его, одновременно построив некоторую классификацию формул (в каком- то смысле отражающую их "логическую сложность"). В качестве меры сложности можно было бы взять число кванторов в предваренной нормальной форме. Но правильнее учитывать число групп кванторов (считая одноименные рядом стоящие кванторы за один).

Говорят, что предваренная формула является $$\Sigma_n$$ - формулой, если ее кванторная приставка содержит $$n$$ групп кванторов, причем первыми стоят кванторы существования. Если первыми стоят кванторы всеобщности, говорят о классе $$\Pi_n$$. (Аналогичные обозначения используются в теории алгоритмов для классификации арифметических множеств, см. [5]).

Пример: формула $${\forall x \exists y \exists z\forall u\, (A(x,u,z)\to B(z,u))}$$ принадлежит классу $$\Pi_3$$, формула $$\exists u\forall v\,C(u,v)$$ принадлежит классу $$\Sigma_2$$, а формула $${\forall x\, (A(x) \to \exists y B(x,y))}$$ вообще не находится в предваренной нормальной форме.

103. Указать формулу в предваренной нормальной форме, доказуемо эквивалентную последней из перечисленных формул.

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

105. Как сэкономить один квантор в этом преобразовании?

Теперь все готово для доказательства упомянутого в начале раздела результата.

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

Индукция по построению формулы. Для атомарных формул это очевидно. Отрицание переводит формулу класса $$\Sigma_n$$ в класс $$\Pi_n$$ и наоборот. Конъюнкция и дизъюнкция: приведем каждую формулу к предваренной нормальной форме, затем добавим фиктивные кванторы так, чтобы они попали в один класс, а затем воспользуемся доказанным утверждением. Импликация сводится к дизъюнкции и отрицанию ( $$\varphi\hm\to\psi$$ доказуемо эквивалентно $$\lnot\varphi\lor\psi$$ ).

Отметим, что ни формулировка, ни доказательство этой теоремы не предполагают замкнутости формулы.

106. Привести к предваренной нормальной форме формулу $$\forall x\,A(x)\hm\to\forall x\, B(x)$$.

107. Формулы $$\varphi$$ и $$\psi$$ принадлежат классу $$\Sigma_n$$. Найдем формулу в предваренной нормальной форме, выводимо эквивалентную формуле $$\varphi\hm\to\psi$$. В каком классе она окажется? (Указание: возможны разные варианты.)

108. Применим описанный метод к общезначимой формуле $$\exists x\forall y\, A(x,y)\hm\to\forall y\exists x A(x,y)$$. Какая предваренная формула получится? (Естественно, она будет общезначимой.)

Теорема Эрбрана

Естественно ожидать, что вопрос о выводимости (или общезначимости) формулы тем сложнее, чем сложнее сама формула. В этом разделе (а также в следующем) мы рассмотрим его для формул класса $$\Sigma_n$$ и $$\Pi_n$$.

Начнем с самого простого случая — бескванторных формул. Пусть $$\varphi$$ — бескванторная формула. Посмотрим, из каких атомарных формул она составлена, и заменим их на пропозициональные переменные (разные — на разные, одинаковые — на одинаковые). Получится формула логики высказываний, которую мы будем называть прототипом формулы $$\varphi$$. Имеет место следующее (почти очевидное) утверждение.

Теорема 54 (выводимость бескванторных формул). Бескванторная формула выводима (общезначима) тогда и только тогда, когда ее прототип является тавтологией.

Если прототип формулы $$\varphi$$ является тавтологией, то формула $$\varphi$$ является частным случаем пропозициональной тавтологии и потому выводима и общезначима.

Пусть прототип формулы $$\varphi$$ не является тавтологией. Можно считать, что формула $$\varphi$$ замкнута, поскольку свободные переменные с точки зрения общезначимости и выводимости ничем не отличаются от констант (мы уже отмечали это при доказательстве теоремы о полноте). Построим интерпретацию, где формула $$\varphi$$ будет ложной. Носителем ее будут замкнутые термы. Значения предикатов мы подберем так, чтобы атомарные формулы принимали те самые значения, которые делают прототип формулы $$\varphi$$ ложным. Это возможно, так как значения разных атомарных формул можно выбирать независимо (это значения либо разных предикатов, либо одного и того же предиката, но на разных термах).

Что можно сказать про общезначимость формул классов $$\Pi_1$$ и $$\Sigma_1$$? Для класса $$\Pi_1$$ все просто: общезначимость формулы со свободными переменными равносильна общезначимости ее замыкания (которое получается, если навесить кванторы всеобщности по всем переменным), поэтому формулы класса $$\Pi_1$$ по существу ничем не отличаются от бескванторных.

Вопрос для класса $$\Sigma_1$$ решается следующей теоремой:

Теорема 55 (Эрбрана). Формула $$\exists \xi_1\ldots\exists\xi_k\,\varphi$$ (где формула $$\varphi$$ — бескванторная) общезначима тогда и только тогда, когда найдется конечный список подстановок$$\begin{align*} \varphi(t_1/\xi_1,\dots, t_k/\xi_k),\\ \varphi(u_1/\xi_1,\dots, u_k/\xi_k),\\ \dots\dots\dots\dots\dots\dots\dots\\ \varphi(w_1/\xi_1,\dots, w_k/\xi_k) \end{align*}$$ (вместо переменных подставляются термы нашей сигнатуры), дизъюнкция которых общезначима.

Заметим, что дизъюнкция, о которой идет речь в теореме, является бескванторной формулой. По теореме 54 она общезначима тогда и только тогда, когда является частным случае пропозициональной тавтологии.

Прежде чем доказывать эту теорему, приведем пример. Рассмотрим формулу$$\exists x \,( A(c,x)\to A(x,d) )$$ (в которой $$c$$ и $$d$$ — константы). Она общезначима; соответствующий набор состоит из подстановок $$c/x$$ и $$d/x$$. В самом деле, формула$$(A(c,c)\to A(c,d))\lor (A(c,d)\to A(d,d))$$ истинна как при истинном $$A(c,d)$$, так и при ложном. Заметим, что в этом примере нам понадобились две подстановки.

Доказательство теоремы Эрбрана. В одну сторону утверждение очевидно: если общезначима дизъюнкция подстановок, то общезначима формула с квантором. (Мы уже использовали это при элиминации кванторов в разделе "Элиминация кванторов" при доказательстве теоремы 28.)

Докажем обратное утверждение. Будем считать, что формула $$\varphi$$ не содержит переменных, кроме $$\xi_1,\dots,\xi_k$$ (как мы уже замечали, остальные переменные можно заменить константами). Рассмотрим (бесконечное) множество формул$$\lnot\varphi(t_1/\xi_1,\dots,t_k/\xi_k)$$ для всевозможных наборов замкнутых термов $$t_1,\dots,t_k$$. Если это множество противоречиво, все доказано (тогда выводима дизъюнкция подстановок, отрицания которых используются при выводе противоречия). Если оно непротиворечиво, то существует интерпретация, в которой все эти формулы истинны. Мы не можем утверждать, что в этой интерпретации ложна формула$$\exists\xi_1\dots\exists\xi_k\,\varphi$$ (носитель интерпретации может содержать элементы, не являющиеся значениями замкнутых термов). Однако если мы выбросим лишние элементы и оставим только значения термов, то эта формула станет ложной, так что она не общезначима.

Заметим, что теорему Эрбрана можно сформулировать чисто синтаксически: если выводима $$\Sigma_1$$ -формула $$\exists \xi_1\ldots\exists \xi_k \varphi$$, то можно найти конечное число подстановок, дизъюнкция которых выводима. Можно предложить и доказательство, не использующее понятия общезначимости. Такое доказательство приведено, например, в книге Клини [16] (для генценовского варианта исчисления предикатов) и в книге Шенфилда [31] (для гильбертовского варианта). Синтаксическое доказательство (в отличие от нашего) конструктивно: по выводу $$\Sigma_1$$ -формулы можно алгоритмически указать соответствующие термы.

Если сигнатура не содержит функциональных символов, то теорема Эрбрана позволяет алгоритмически проверить выводимость формул класса $$\Sigma_1$$, поскольку число возможных подстановок конечно. Это же можно сказать и про формулы класса $$\Pi_2$$, так как внешние кванторы всеобщности можно отбросить, не меняя выводимости.

Естественный вопрос: можно ли построить аналогичные алгоритмы для следующих классов? Отрицательный ответ дается в следующем разделе.

Сколемовские функции

В этом разделе мы в разных формах используем ровно одну идею: утверждение$$\forall x \exists y \, A(x,y)$$ равносильно существованию функции, которая по любому $$x$$ дает такой $$y$$, что $$A(x,y)$$. Это утверждение нельзя записать в виде эквивалентности$$\forall x\exists y \, A(x,y) \Leftrightarrow \exists f \forall x\, A(x,f(x)),$$ поскольку в нашем языке нет квантора по функциям и $$\exists f$$ мы писать не имеем права. (Языки, содержащие кванторы по множествам и функциям, называются языками второго порядка и мы их не рассматриваем.)

Тем не менее это утверждение можно сформулировать и в наших терминах. Пусть, например, имеется формула $$\varphi$$ с двумя параметрами $$x$$ и $$y$$. Тогда замкнутая формула $$\forall x \exists y\,\varphi$$ выполнима тогда и только тогда, когда выполнима формула $$\forall x \varphi(f(x)/y)$$, где $$f$$ — новый одноместный функциональный символ. (Аккуратный читатель поправит: надо еще требовать, чтобы подстановка $$f(x)$$ вместо $$y$$ была корректна. Мы уже знаем, что переменные можно переименовывать, поэтому будем легкомысленно считать, что все необходимые переименования уже сделаны.)

Аналогичное преобразование выполнимо и для произвольных предваренных формул. Например, формула$$\forall x \forall y \exists z \forall u \exists v\,\varphi (x,y,z,u,v)$$ выполнима тогда и только тогда, когда выполнима формула$$\forall x \forall y \forall u\,\varphi (x,y,f(x,y),u,g(x,y,u))$$ (здесь $$\varphi(x,y,z,u,v)$$ — формула, не имеющая параметров, кроме $$x,y,z,u,v$$, запись $$\varphi(x,y,f(x,y),u,g(x,y,u))$$ обозначает результат соответствующих подстановок, которые мы предполагаем корректными, а $$f$$ и $$g$$ — функциональные символы, не встречающиеся в формуле $$\varphi$$ ).

Сходное преобразование имеют в виду преподаватели математического анализа, которые иногда записывают определение предела ( $$\forall \varepsilon \exists\delta\ldots$$ ) в несколько странной для логика форме $$\forall \varepsilon \exists \delta=\delta(\varepsilon)\ldots$$ — имеется в виду, что если для каждого $$\varepsilon$$ найдется $$\delta$$, то это самое $$\delta$$ представляет собой функцию от $$\varepsilon$$.

Отметим, что это рассуждение использует аксиому выбора, когда из различных возможных (для данного $$\varepsilon$$ ) значений $$\delta$$ мы выбираем какое-то одно и объявляем его значением функции $$\varepsilon(\delta)$$.

109. Казалось бы, выбор $$v$$ в приведенном выше примере зависит от $$x,y,z,u$$, так что следовало бы написать $$\varphi(x,y,f(x,y),u,g(x,y,f(x,y),u))$$ — но мы так не делаем. Почему это допустимо?

Используя описанное преобразование, мы приходим к такой теореме:

Теорема 56. Для всякой замкнутой формулы $$\tau$$ сигнатуры $$\sigma$$ можно указать формулу $$\tau'$$ класса $$\Pi_1$$ сигнатуры $$\sigma$$ с добавленными функциональными символами, которая выполнима или невыполнима одновременно с формулой $$\tau$$. При этом преобразование $$\tau\mapsto\tau'$$ эффективно (выполняется некоторым алгоритмом).

Приведя $$\tau$$ к предваренной нормальной форме, получим доказуемо эквивалентную формулу (выполнимую или невыполнимую одновременно с $$\tau$$ ). После этого применяем описанное выше преобразование.

Формула $$\tau$$ невыполнима тогда и только тогда, когда ее отрицание общезначимо. Поэтому наши рассуждения показывают, что, скажем, формула $$\lnot \forall x \exists y\,\psi(x,y)$$ общезначима одновременно с формулой $$\lnot \forall x \,\psi(x,f(x))$$. Внося отрицание внутрь и заменяя $$\lnot\psi$$ на $$\varphi$$, получаем такое утверждение: формулы$$\exists x \forall y\,\varphi(x,y) \quad \text{и}\quad \exists x \,\varphi(x,f(x))$$ одновременно общезначимы. (Это утверждение чуть менее наглядно, чем двойственное ему утверждение о выполнимости.) В общем виде двойственное к теореме 56 утверждение выглядит так:

Теорема 57. Для всякой замкнутой формулы $$\tau$$ сигнатуры $$\sigma$$ можно указать формулу $$\tau'$$ класса $$\Sigma_1$$ сигнатуры $$\sigma$$ с добавленными функциональными символами, которая общезначима или необщезначима одновременно с формулой $$\tau$$. При этом преобразование $$\tau\mapsto\tau'$$ эффективно (выполняется некоторым алгоритмом).

Заметим, что к формуле $$\tau'$$ можно применить теорему Эрбрана: она общезначима тогда и только тогда, когда дизъюнкция нескольких подстановок является тавтологией.

Теорема о полноте позволяет заменить в этой формулировке общезначимость на выводимость: формулы $$\tau$$ и $$\tau'$$ одновременно выводимы. После этого естественно искать явный метод, который преобразует вывод формулы $$\tau$$ в вывод формулы $$\tau'$$ и обратно. Такой метод действительно существует, но для этого требуется более детальный анализ структуры выводов, при котором удобно пользоваться исчислениями генценовского типа.

Идея использования функций вместо групп кванторов $$\forall\exists$$ восходит к Эрбрану и Сколему. Такие функции иногда называют "эрбрановскими" или "сколемовскими", а их добавление — "сколемизацией". Есть также термин "сколемовская нормальная форма", но здесь добавляются не функциональные символы, а предикатные, и получается формула не класса $$\Sigma_1$$, как в теореме 57, а класса $$\Sigma_2$$.

Теорема 57 (о сколемовской нормальной форме). Для всякой замкнутой формулы $$\tau$$ сигнатуры $$\sigma$$ можно указать формулу $$\tau'$$ класса $$\Sigma_2$$ сигнатуры $$\sigma$$ с добавленными предикатными символами, которая общезначима или необщезначима одновременно с формулой $$\tau$$. При этом преобразование $$\tau\mapsto\tau'$$ эффективно (выполняется некоторым алгоритмом).

Как и раньше, нам будет удобнее говорить о выполнимости и доказывать, что для всякой формулы $$\tau$$ найдется одновременно с ней выполнимая формула $$\tau'$$ из класса $$\Pi_2$$. Построение такой формулы мы объясним на примере. Пусть исходная формула имеет вид$$\forall x \forall y \exists z \forall u \exists v\,\varphi(x,y,z,u,v).$$ Мы теперь не можем ввести функции $$f$$ и $$g$$, как это делалось выше. Поэтому мы введем предикаты $$F$$ и $$G$$, заменяющие графики этих функций, и напишем формулу$$\begin{align*} \forall x\forall y \exists z\,\, F(x,y,z) \land \\ \forall x \forall y \forall u \exists v\,\, G(x,y,u,v) \land\\ \forall x \forall y \forall z \forall u \forall v\, (F(x,y,z)\land G(x,y,u,v) \to \varphi(x,y,z,u,v)) \end{align*}$$ Если исходная формула выполнима, то новая тоже выполнима: достаточно взять в качестве $$F$$ и $$G$$ графики сколемовских функций. Напротив, если новая формула выполнима, то выполнима и старая (более того, из новой формулы следует старая): надо взять $$z$$ и $$v$$ согласно первым двум строкам и заметить, что согласно третьей строке они подойдут.

Такая конструкция применима к любой предваренной форме и дает конъюнкцию $$\Pi_2$$ -формул (последняя из которых будет даже и $$\Pi_1$$ -формулой). А мы знаем, что такая конъюнкция эквивалентна $$\Pi_2$$ -формуле.

110. Дайте синтаксическое доказательство теоремы о сколемовской нормальной форме (показав, что из выводимости формулы следует выводимость ее сколемовской нормальной формы и наоборот). (Указание: это проще, чем для формул с функциональными символами, и не требуется использовать генценовское исчисление.)

Утверждения этого раздела сводят вопрос о выводимости произвольной формулы исчисления предикатов к выводимости $$\Sigma_1$$ -формулы (с функциональными символами). Если мы запрещаем функциональные символы, то вопрос о выводимости произвольной формулы сводится к выводимости $$\Sigma_2$$ - формулы.

Известно (теорема Черча, доказательство можно прочесть в [5]), что вопрос о выводимости произвольных формул языка первого порядка неразрешим: не существует алгоритма, который бы по произвольной замкнутой формуле определял бы, выводима она или нет. Результаты этого раздела показывают, что уже для формул класса $$\Sigma_1$$ (с функциональными символами) или $$\Sigma_2$$ (без них) такого алгоритма не существует, поскольку из него можно было бы получить и общий алгоритм. (В предыдущем разделе мы видели, что для формул класса $$\Sigma_1$$ без функциональных символов такой алгоритм существует.)