Полнота исчисления предикатов

Выводимость из посылок

В исчислении высказываний важную роль играло понятие выводимости из посылок и связанная с ним лемма о дедукции. Для исчисления предикатов ситуация немного меняется. Если разрешить использовать посылки наравне с аксиомами безо всяких ограничений, то утверждение, аналогичное лемме о дедукции, будет неверным. Например, из формулы $$A(x)$$ можно вывести формулу $$\forall x\, A(x)$$ (как мы видели при обсуждении правила обобщения). Но импликация $$A(x)\to\forall x\,A(x)$$ не является выводимой (поскольку не общезначима).

Поэтому мы ограничимся случаем, когда все посылки являются замкнутыми формулами. Пусть $$\Gamma$$ — произвольное множество замкнутых формул рассматриваемой нами сигнатуры $$\sigma$$. (Такие множества называют теориями в сигнатуре $$\sigma$$.) Говорят, что формула $$A$$ выводима из $$\Gamma$$, если ее можно вывести, используя наравне с аксиомами формулы из $$\Gamma$$. Как и для исчисления высказываний, мы пишем $$\Gamma\vdash A$$. Выводимые из $$\Gamma$$ формулы называют также теоремами теории $$\Gamma$$.

Лемма о дедукции для исчисления предикатов. Пусть $$\Gamma$$ — множество замкнутых формул, а $$A$$ — замкнутая формула. Тогда $$\Gamma \vdash (A\to B)$$ тогда и только тогда, когда $$\Gamma\cup\{A\} \vdash B$$.

Доказательство проходит по той же схеме, что и для исчисления высказываний : к формулам $$C_1,\dots,C_n$$, образующим вывод $$C_n=B$$ из $$\Gamma\cup\{A\}$$, мы приписываем посылку $$A$$ и дополняем полученную последовательность$$(A\to C_1),\dots,(A\to C_n)$$ до вывода из $$\Gamma$$. Отличие от пропозиционального случая в том, что в выводе могут встречаться правила Бернайса. Например, от выводимости формулы$$A\to(\psi\to\varphi)$$ надо перейти к выводимости формулы$$A\to(\psi\to\forall\xi\,\varphi)$$ (в которой переменная $$\xi$$ не является параметром формулы $$\psi$$ ). Это несложно сделать, если заметить, что в силу пропозициональных тавтологий можно перейти от $$A\to(\psi\to\varphi)$$ к $$(A\land\psi)\to\varphi$$, затем применить правило Бернайса (это законно, так как переменная $$\xi$$ не является параметром формулы $$\psi$$, а формула $$A$$ замкнута по предположению). Получится выводимая из $$\Gamma$$ формула$$(A\land\psi)\to\forall\xi\,\varphi,$$ и остается вернуть $$A$$ из конъюнкции в посылку.

Сходным образом рассматривается и второе правило Бернайса. Если выводима формула $$A\to(\varphi\to\psi)$$, то в силу пропозициональных тавтологий выводима формула $$\varphi\to(A\to\psi)$$, к которой можно применить правило Бернайса и получить $$\exists\xi\,\varphi\to(A\to\psi)$$, после чего вернуть $$A$$ назад с помощью пропозициональной тавтологии. Лемма о дедукции доказана.

Отметим теперь несколько полезных свойств выводимости из посылок.

Понятие выводимости из посылок позволяет переформулировать теорему о корректности исчисления предикатов.

Говорят, что интерпретация $$M$$ сигнатуры $$\sigma$$ является моделью теории $$\Gamma$$, если все формулы из $$\Gamma$$ истинны в $$M$$.

Теорема 44 (о корректности; переформулировка). Все теоремы теории $$\Gamma$$ истинны в любой модели $$M$$ теории $$\Gamma$$.

Если формула $$A$$ является теоремой теории $$\Gamma$$ (т. е. $$\Gamma\vdash A$$ ), найдутся формулы $$\gamma_1,\dots,\gamma_n\in\Gamma$$, для которых$$\vdash \gamma_1\to(\gamma_2\to(\ldots(\gamma_n\to A)\ldots)).$$ По теореме о корректности (в уже известной нам форме) эта формула будет истинна во всех интерпретациях, в частности в $$M$$. Поскольку $$\gamma_1,\dots,\gamma_n$$ истинны в $$M$$, то и формула $$A$$ истинна в $$M$$ (на любой оценке).

В следующих задачах — и только в них — знак $$\vdash$$ понимается в описанном выше смысле (в посылках допускаются параметры).

95. Пусть $$\Gamma$$ — множество произвольных (не обязательно замкнутых) формул. (а) Пусть существует "вывод" некоторой формулы $$\varphi$$, в котором наравне с аксиомами используются формулы из $$\Gamma$$, при этом все применения правил Бернайса предшествуют появлению формул из $$\Gamma$$. Покажите, что $$\Gamma\vdash\varphi$$. Покажите, что верно и обратное утверждение. (б) Покажите, если в "выводе" формулы $$\varphi$$ наравне с аксиомами используются формулы из $$\Gamma$$, но правила Бернайса не применяются по переменным, свободным в $$\Gamma$$, то $${\Gamma\vdash\varphi}$$.

96. Покажите, что правила Бернайса можно переписать так:$$\frac{\Gamma, A\vdash B\mathstrut} {\Gamma, A \vdash \forall\xi\,B\mathstrut} \qquad \frac{\Gamma, B\vdash A\mathstrut} {\Gamma, \exists\xi\,\vdash A\mathstrut},$$ где переменная $$\xi$$ не является параметром формулы $$A$$, а также параметром формул из $$\Gamma$$. (В первом правиле мы для симметрии выделили формулу $$A$$, хотя она ничем не отличается от формул из $$\Gamma$$.)

Переменные и константы

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

Лемма о свежих константах. Пусть выводима формула $$\varphi(c/\xi)$$, где $$\varphi$$ — произвольная формула, $$\xi$$ — переменная, $$c$$ — константа, не входящая в формулу $$\varphi$$. Тогда выводима и формула $$\varphi$$.

Интуитивный смысл леммы: если мы доказали что-то про "свежую" константу $$c$$ (не запятнавшую себя участием в формуле $$\varphi$$ ), то фактически мы доказали формулу $$\varphi$$ для произвольных значений переменной.

Доказательство леммы. По условию существует вывод формулы $$\varphi(c/\xi)$$. Возьмем "свежую" переменную $$\eta$$, не встречающуюся в этом выводе, и всюду заменим в нем константу $$c$$ на эту переменную. При этом вывод останется выводом, так как правила обращения с переменными и константами ничем не отличаются (кванторов по новой переменной в нем нет, так что корректные подстановки останутся корректными и применения правил Бернайса останутся допустимыми). Таким образом, выводима формула $$\varphi(\eta/\xi)$$.

По правилу обобщения выводима формула $$\forall\eta\,\varphi(\eta/\xi)$$. Осталось применить аксиому $$\forall\eta\,\varphi(\eta/\xi)\hm\to \varphi(\eta/\xi)(\xi/\eta)$$ ; подстановка в правой части корректна и дает формулу $$\varphi$$, так как сначала мы заменили свободные вхождения $$\xi$$ на $$\eta$$, а затем обратно (так что в зону действия кванторов по $$\xi$$ они попасть не могли). Лемма доказана.

97. Сформулируйте и докажите аналогичную лемму для нескольких констант.

Аналогичное рассуждение позволяет доказать и другое утверждение, которое нам потребуется:

Лемма о добавлении констант. Пусть формула $$\varphi$$ некоторой сигнатуры $$\sigma$$ выводима в исчислении предикатов расширенной сигнатуры $$\sigma'$$, полученной из $$\sigma$$ добавлением новых констант. Тогда $$\varphi$$ выводима и в исчислении предикатов сигнатуры $$\sigma$$.

Доказательство. Пусть формула $$\varphi$$, не содержащая новых констант, имеет вывод, в котором новые константы встречаются. Как их оттуда удалить? Легко понять, что их можно заменить на свежие переменные, не входящие в вывод, и он останется выводом, но уже без новых констант. Лемма доказана.

На самом деле эта лемма верна для произвольного расширения сигнатуры (можно добавлять не только константы, но и функциональные символы любой валентности, а также предикатные символы). Чтобы удалить новые символы из вывода, поступаем так. Все термы вида $$f(\ldots)$$, где $$f$$ — добавленный функциональный символ, мы заменяем на новую переменную (можно взять одну и ту же переменную для всех новых символов и всех их вхождений). Все атомарные формулы с новыми предикатными символами заменяем на какую-либо замкнутую формулу (одну и ту же; какая именно формула, роли не играет).

98. Проведите это рассуждение подробно.

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

Если принять теорему о полноте, по которой выводимость равносильна общезначимости, независимость выводимости от сигнатуры становится очевидной: истинность формулы не зависит от интерпретации символов, которые в нее не входят. (Если интерпретировать отсутствующие в формуле символы как постоянные функции и предикаты, мы приходим к синтаксическому рассуждению, упомянутому выше.)

Полнота исчисления предикатов

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

Фиксируем некоторую сигнатуру $$\sigma$$. Пусть $$\Gamma$$ — теория в сигнатуре $$\sigma$$, то есть произвольное множество замкнутых формул этой сигнатуры. Говорят, что теория $$\Gamma$$ противоречива, если в ней выводится некоторая формула $$\varphi$$ и ее отрицание $$\lnot\varphi$$. В этом случае из $$\Gamma$$ выводится любая формула, так как имеется аксиома $$\lnot A \to (A \to B)$$. Если теория $$\Gamma$$ не является противоречивой, то она называется непротиворечивой.

99. Докажите, что теория противоречива тогда и только тогда, когда в ней выводится формула $$\varphi\land\lnot\varphi$$ (здесь $$\varphi$$ — произвольная формула сигнатуры).

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

Синтаксическое понятие непротиворечивости мы будем сравнивать с семантическим понятием совместности. Пусть имеется некоторая интерпретация $$M$$ сигнатуры $$\sigma$$. Напомним, что она называется моделью теории $$\Gamma$$, если все формулы из $$\Gamma$$ истинны в $$M$$. Множество $$\Gamma$$ называется совместным, если оно имеет модель, то есть если все его формулы истинны в некоторой интерпретации.

Теорема 45 (о корректности; переформулировка). Любое совместное множество замкнутых формул непротиворечиво.

Пусть все формулы из $$\Gamma$$ истинны в некоторой интерпретации $$M$$. Может ли оказаться, что $$\Gamma\hm\vdash \varphi$$ и $$\Gamma\hm\vdash\lnot\varphi$$ для некоторой замкнутой формулы $$\varphi$$? Легко понять, что нет. В самом деле, в этом случае теорема 44 показывает, что формулы $$\varphi$$ и $$\lnot\varphi$$ должны быть одновременно истинны в $$M$$, что, очевидно, невозможно.

Для доказательства обратного утверждения (о совместности непротиворечивой теории) нам понадобится понятие полной теории.

Непротиворечивое множество $$\Gamma$$, состоящее из замкнутых формул сигнатуры $$\sigma$$, называется полным в этой сигнатуре, если для любой замкнутой формулы $$\varphi$$ этой сигнатуры либо формула $$\varphi$$, либо ее отрицание $$\lnot \varphi$$ выводятся из $$\Gamma$$.

Другими словами, теория полна, если из любых двух формул $$\varphi$$ и $$\lnot\varphi$$ (соответствующей сигнатуры) ровно одна является теоремой этой теории.

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

В определении полноты существенно, что мы ограничиваемся замкнутыми формулами той же сигнатуры. Например, если мы возьмем одноместный предикатный символ $$S$$, не входящий в $$\Gamma$$, то формулы из $$\Gamma$$ про него ничего не утверждают, и потому, скажем, ни формула $$\forall x\, S(x)$$, ни ее отрицание не выводимы из $$\Gamma$$. Замкнутость формулы $$\varphi$$ тоже важна. Например, множество всех истинных в натуральном ряду формул сигнатуры $$({=},{<})$$ полно, но ни формула $$x=y$$, ни формула $$x\ne y$$ из него не выводятся, иначе по правилу обобщения мы получили бы ложную в $$\mathbb{N}$$ формулу $${\forall x\forall y\, (x=y)}$$ или $${\forall x \forall y\, (x\ne y)}$$.

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

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

Теорема 46 (полнота исчисления предикатов, сильная форма). Любая непротиворечивая теория совместна.

Напомним, как мы доказывали аналогичное утверждение для высказываний. Мы расширяли наше непротиворечивое множество $$\Gamma$$ до полного множества $$\Gamma'$$, а потом полагали пропозициональную переменную $$p$$ истинной, если $$\Gamma'\vdash p$$. Здесь этого будет недостаточно, как мы увидим (например, непонятно, откуда брать носитель искомой модели). Но начало рассуждения будет таким же.

Лемма 1. Для всякого непротиворечивого множества $$\Gamma$$ замкнутых формул сигнатуры $$\sigma$$ существует полное непротиворечивое множество $$\Gamma'$$ замкнутых формул той же сигнатуры, содержащее $$\Gamma$$.

Доказательство повторяет рассуждение раздела "Второе доказательство теоремы о полноте": рассматривая по очереди замкнутые формулы, мы добавляем либо их, либо их отрицания в множество $$\Gamma$$.

Это можно сделать без труда для конечной или счетной сигнатуры (тогда множество всех замкнутых формул этой сигнатуры счетно); для общего случая надо воспользоваться трансфинитной индукцией или леммой Цорна, как объяснялось в разделе "Второе доказательство теоремы о полноте". Лемма 1 доказана.

Как же нам теперь построить модель полного множества $$\Gamma$$? Прежде всего надо решить, что будет носителем этой модели. Заметим, что в сигнатуре могут быть некоторые константы (функциональные символы валентности $$0$$ ). Им должны соответствовать некоторые элементы носителя. Кроме того, замкнутым термам (которые не содержат никаких переменных, только константы) также должны соответствовать элементы носителя. Попробуем взять в качестве носителя как раз множество $$T$$ всех замкнутых термов нашей сигнатуры. При этом понятно, как надо определять сигнатурные функции на этом множестве: функция, соответствующая символу $$f$$ валентности $$k$$, отображает замкнутые термы $$t_1,\ldots,t_k$$ в терм $$f(t_1,\dots,t_k)$$. (Это определение никак не зависит от $$\Gamma$$.)

Предикаты на этом множестве определяем так: если $$A$$ — предикатный символ, а $$t_1,\dots,t_n$$ — замкнутые термы, то предикат, соответствующий символу $$A$$, истинен на термах $$t_1,\dots,t_n$$, если формула $$A(t_1,\dots,t_n)$$ выводима из $$\Gamma$$.

Тем самым интерпретация полностью описана, и мы хотели бы доказать, что все формулы из $$\Gamma$$ в ней истинны. Мы будем доказывать по индукции такой факт: если $$\Gamma\hm\vdash\varphi$$, то формула $$\varphi$$ истинна в построенной интерпретации, а если $$\Gamma\hm\vdash\lnot\varphi$$, то формула $$\varphi$$ ложна.

Однако без дополнительных предположений о множестве $$\Gamma$$ этот план обречен на неудачу, поскольку замкнутых термов может быть совсем мало (или даже вовсе не быть), в то время как соответствующая теория не имеет конечных моделей. Если начать индуктивное рассуждение, то выяснится, что трудность возникает в случае, когда формула $$\varphi$$ начинается с квантора. Например, может оказаться, что формула $$\exists x\,A(x)$$ выводима из множества $$\Gamma$$, в то время как ни для какого замкнутого терма $$t$$ формула $$A(t)$$ не выводима из $$\Gamma$$. Тогда формула $$\exists x\, A(x)$$ будет ложной в описанной нами модели (хотя выводимой). Чтобы преодолеть эту трудность, мы наложим дополнительные требования на множество $$\Gamma$$.

Назовем теорию (множество замкнутых формул сигнатуры $$\sigma$$ ) экзистенциально полной в сигнатуре $$\sigma$$, если для всякой замкнутой формулы $$\exists\xi\,\varphi$$ сигнатуры $$\sigma$$, выводимой из $$\Gamma$$, найдется замкнутый терм $$t$$ этой сигнатуры, для которого $$\Gamma\vdash \varphi(t/\xi)$$.

Если множество $$\Gamma$$ полно и экзистенциально полно, то описанная выше конструкция с замкнутыми термами дает его модель. Прежде чем проверять это, покажем, как расширить $$\Gamma$$ до полного и экзистенциально полного множества. Ключевую роль здесь играет такая лемма:

Лемма 2. Пусть $$\Gamma$$ — непротиворечивое множество замкнутых формул, из которого выводится замкнутая формула $$\exists \xi\,\varphi$$. Пусть $$c$$ — константа, не встречающаяся ни в $$\Gamma$$, ни в $$\varphi$$. Тогда множество $$\Gamma$$ останется непротиворечивым после добавления формулы $$\varphi(c/\xi)$$.

(Замечание. Здесь и далее, говоря о непротиворечивости и выводимости, мы не уточняем, в какой сигнатуре строятся выводы: все наши сигнатуры будут отличаться лишь набором констант, и лемма о добавлении констант.)

Доказательство леммы 2. Пусть $$\Gamma$$ становится противоречивым после добавления формулы $$\varphi(c/\xi)$$. Отсюда следует (используем подходящую пропозициональную тавтологию), что отрицание этой формулы выводится из $$\Gamma$$, то есть выводима формула $$\gamma\hm\to\lnot\varphi(c/\xi)$$, где $$\gamma$$ — конъюнкция конечного числа формул из $$\Gamma$$. По лемме о свежих константах выводима формула $$\gamma\hm\to\lnot\varphi$$ (напомним, что $$c$$ не входит ни в $$\varphi$$, ни в $$\gamma$$ ). Контрапозиция дает формулу $$\varphi\hm\to\lnot\gamma$$, а правило Бернайса — формулу $$\exists\xi\,\varphi\hm\to\lnot\gamma$$. По предположению формула $$\exists\xi\,\varphi$$ выводима из $$\Gamma$$, и множество $$\Gamma$$ оказывается противоречивым. Лемма 2 доказана.

100. Докажите такое усиление леммы 2: при добавлении в $$\Gamma$$ формулы $$\varphi(c/\xi)$$ (в предположениях леммы) множество выводимых из $$\Gamma$$ формул исходной сигнатуры (без константы $$c$$ ) не меняется.

Лемма 3. Пусть $$\Gamma$$ — непротиворечивое множество замкнутых формул сигнатуры $$\sigma$$. Тогда существует расширение сигнатуры $$\sigma$$ новыми константами и непротиворечивое, полное и экзистенциально полное (в расширенной сигнатуре) множество $$\Gamma'$$ замкнутых формул, содержащее $$\Gamma$$.

Доказательство. Пусть сигнатура конечна или счетна. Тогда замкнутых формул вида $$\exists\xi\,\varphi$$, выводимых из $$\Gamma$$, не более чем счетное число. К каждой из них по очереди будем применять лемму 2, вводя новую константу. Согласно этой лемме, на каждом шаге множество $$\Gamma$$ остается непротиворечивым, поэтому оно будет непротиворечивым и после добавления счетного числа формул (вывод противоречия затрагивает лишь конечное число формул).

Однако нельзя утверждать, что полученное множество будет экзистенциально полным в новой сигнатуре, поскольку про формулы вида $$\exists\xi\,\varphi$$ с добавленными константами мы ничего не знаем. Пополним это множество, применив лемму 1, и повторим рассуждение: для каждой замкнутой выводимой формулы, начинающейся с квантора существования, введем новую константу и т. д.

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

Что меняется, если сигнатура несчетна? Тогда мы уже не можем рассматривать все экзистенциальные формулы по очереди, и надо обрабатывать их все сразу. При этом противоречие не появится: в самом деле, оно использовало бы лишь конечное число добавленных формул, а для конечного числа все уже доказано.

После этого доказательство проходит как раньше (мы по-прежнему делаем счетное число чередующихся пополнений множества и расширений сигнатуры).

Лемма 3 доказана.

Последним шагом в доказательстве теоремы о полноте (всякое непротиворечивое множество замкнутых формул совместно) является такая лемма:

Лемма 4. Пусть $$\Gamma$$ — полное и экзистенциально полное множество замкнутых формул некоторой сигнатуры $$\sigma$$. Тогда существует интерпретация $$M$$ сигнатуры $$\sigma$$, в которой истинны все формулы из $$\Gamma$$.

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

Как интерпретировать функциональные символы, понятно (это не зависит от множества $$\Gamma$$ ): если символ $$f$$ имеет валентность $$n$$, то ему соответствует функция, которая отображает $$n$$ замкнутых термов $$t_1,\dots,t_n$$ в замкнутый терм $$f(t_1,\dots,t_n)$$. Константы (функциональные символы валентности $$0$$ ) интерпретируются сами собой.

Интерпретация предикатных символов такова. Пусть $$A$$ — предикатный символ валентности $$n$$. Чтобы узнать, истинен ли соответствующий ему предикат на замкнутых термах $$t_1,\dots,t_n$$, надо составить атомарную формулу $$A(t_1,\dots,t_n)$$ и выяснить, что выводится из $$\Gamma$$ — сама эта формула или ее отрицание. (Здесь мы используем полноту.) В первом случае предикат будет истинным, во втором — ложным.

Индукцией по числу логических связок и кванторов в замкнутой формуле $$\varphi$$ сигнатуры $$\sigma$$ докажем такое утверждение:$$\Gamma\vdash\varphi\Leftrightarrow \varphi \text{ истинна в }M.$$ Для атомарных формул это верно по построению интерпретации $$M$$.

Для пропозициональных связок рассуждение ничем не отличается от приведенного в разделе "Второе доказательства теоремы о полноте". Нам нужно проверить, что выводимость из $$\Gamma$$ подчиняется тем же правилам, что и истинность:$$\begin{align*} \Gamma\vdash \lnot A \Leftrightarrow \Gamma\not\vdash A ,\\ \Gamma\vdash A\land B \Leftrightarrow \Gamma\vdash A \text{ и } \Gamma\vdash B, \\ \Gamma\vdash A\lor B \Leftrightarrow \Gamma\vdash A \text{ или } \Gamma\vdash B, \\ \Gamma\vdash A\to B \Leftrightarrow \Gamma\not\vdash A \text{ или } \Gamma\vdash B. \end{align*}$$ Все эти свойства несложно доказать. Первое из них выражает полноту (и непротиворечивость — напомним, что по определению полная теория всегда непротиворечива) множества $$\Gamma$$. Остальные свойства легко проверить, если иметь в виду, что все частные случаи пропозициональных тавтологий выводимы.

Пусть теперь формула $$\varphi$$ имеет вид $$\exists \xi\,\psi$$, где $$\psi$$ — формула с единственным параметром $$\xi$$ (или без параметров). Предположим, что она выводима из $$\Gamma$$. Тогда в силу экзистенциальной полноты найдется константа $$c$$, для которой $$\Gamma\hm\vdash \psi(c/\xi)$$. Формула $$\psi(c/\xi)$$ имеет меньшее число логических связок, поэтому к ней можно применить предположение индукции и заключить, что она истинна в $$M$$. Тогда формула $$\psi$$ истинна на оценке $$\xi\mapsto c $$, поэтому формула $$\exists\xi\,\psi$$ истинна в $$M$$.

Напротив, пусть формула $$\exists\xi\,\psi$$ истинна в $$M$$. Тогда (по определению истинности) найдется элемент (замкнутый терм) $$t$$, для которого $$\psi$$ истинна на оценке $$\xi\mapsto t$$ и потому формула $$\psi(t/\xi)$$ истинна в $$M$$. По предположению индукции формула $$\psi(t/\xi)$$ выводима из $$\Gamma$$. Осталось воспользоваться тем, что формула $$\psi(t/\xi)\to\exists\xi\,\psi$$ является аксиомой (напомним, подстановка замкнутого терма всегда корректна).

Наконец, рассмотрим случай, когда формула $$\varphi$$ имеет вид $$\forall\xi\,\psi$$. Пусть она выводима из $$\Gamma$$. Формула $$\forall \xi\, \psi \hm\to \psi(t/\xi)$$ является аксиомой для любого замкнутого терма $$t$$. Поэтому и формула $$\psi(t/\xi)$$ выводима из $$\Gamma$$. В ней меньше логических связок, чем в $$\varphi$$, поэтому по предположению индукции она истинна в $$M$$. Значит, формула $$\psi$$ истинна на любой оценке $$\xi\hm\mapsto t$$, и потому формула $$\forall\xi\,\psi$$ истинна в $$M$$.

Если формула $$\forall\xi\,\psi$$ не выводима из $$\Gamma$$, то из $$\Gamma$$ выводится ее отрицание. Оно, как мы видели, доказуемо эквивалентно формуле $$\exists\xi\,\lnot\psi$$. Поэтому в силу экзистенциальной полноты выводима формула $$\lnot\psi(c/\xi)$$ для некоторой константы $$c$$. Эта формула истинна, поэтому $$\psi$$ ложна при некотором значении переменной $$\xi$$, так что формула $$\forall\xi\,\psi$$ ложна в $$M$$.

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

Анализ доказательства позволяет сделать такое наблюдение:

Теорема 47. Непротиворечивое множество замкнутых формул конечной или счетной сигнатуры имеет счетную модель.

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

Аналогичное рассуждение с использованием свойств операций с мощностями (о которых можно прочесть в [6]) устанавливает такой факт:

Теорема 48. Всякое непротиворечивое множество формул сигнатуры $$\sigma$$ имеет модель мощности $$\max(\aleph_0,|\sigma|)$$ (где $$\aleph_0$$ обозначает счетную мощность, а $$|\sigma|$$ — мощность сигнатуры).

Кстати, при доказательстве теорем 47 и 48 можно было бы сослаться на теорему Левенгейма-Сколема об элементарной подмодели (построить модель произвольной мощности, а потом уменьшить, если надо).

Возвратимся теперь к исходной формулировке теоремы о полноте.

Теорема 49 (полнота исчисления предикатов, слабая форма) Всякая общезначимая формула выводима в исчислении предикатов.

Пусть формула $$\varphi$$ замкнута. Если она невыводима, то множество $$\{\lnot \varphi\}$$ непротиворечиво и потому совместно. В его модели формула $$\varphi$$ будет ложной, что противоречит предположению.

Что касается незамкнутых формул, то их общезначимость и выводимость равносильна общезначимости и выводимости их замыкания.

Как и в разделе "Второе доказательство теоремы о полноте", из теоремы о полноте можно вывести такое следствие:

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

В самом деле, по теореме о полноте (и корректности, если быть точным) наличие модели (совместность) равносильно непротиворечивости. А по определению противоречивость затрагивает лишь конечное число формул из $$\Gamma$$.

101. Покажите, что теорема о полноте в сильной форме является следствием теоремы компактности и теоремы о полноте в слабой форме. (Указание: если множество $$\Gamma$$ не имеет модели, то его конечная часть не имеет модели, поэтому формула $$\langle\dots\rangle$$ общезначима, поэтому $$\dots$$ )

Прямое доказательство теоремы компактности (без использования понятия выводимости) мы дадим в следующей лекции.

Еще один важный результат, вытекающий из теоремы о полноте — совпадение синтаксического понятия выводимости и семантического понятия следования. Пусть дана некоторая сигнатура $$\sigma$$. Рассмотрим множество $$\Gamma$$ замкнутых формул этой сигнатуры (такие множества мы называем теориями в сигнатуре $$\sigma$$ ) и еще одну замкнутую формулу $$\varphi$$. Говорят, что $$\varphi$$ семантически следует из $$\Gamma$$, если $$\varphi$$ истинна во всякой модели теории $$\Gamma$$, то есть во всякой интерпретации сигнатуры $$\sigma$$, где истинны все формулы из $$\Gamma$$. (Обозначение: $$\Gamma\vDash\varphi$$.)

Теорема 51.$$\Gamma\vdash \varphi \Leftrightarrow \Gamma\vDash \varphi.$$

Если $$\Gamma\vdash\varphi$$, то $$\Gamma\vDash\varphi$$.

Напротив, пусть $$\varphi$$ не выводима из $$\Gamma$$. Тогда теория $$\Gamma\hm\cup\{\lnot\varphi\}$$ непротиворечива и (в силу теоремы о полноте) имеет модель. Значит $$\varphi$$ не следует из $$\Gamma$$.

102. Какими нужно взять $$\varphi$$ и $$\Gamma$$ в этой теореме, чтобы получить приведенные ранее формулировки теоремы о полноте? (Ответ: при $$\varphi\hm=\perp$$ (тождественно ложная формула) получаем сильную форму теоремы о полноте, при $$\Gamma\hm=\varnothing$$ — слабую.)

Переименование переменных

В этом разделе мы попытаемся аккуратно разобраться с простым вопросом о том, почему и как можно переименовывать связанные переменные, не меняя смысла формул. Мы уже видели, что формулы $$\forall x\,A(x)$$ и $$\forall y\,A(y)$$ доказуемо эквивалентны , то есть их эквивалентность доказуема в исчислении предикатов. Сейчас мы хотим доказать общее утверждение об этом.

Корректная формулировка утверждения о переименовании переменных требует осторожности. Например, нельзя сказать, что формула $$\forall\xi\, \varphi$$ всегда эквивалентна $$\forall\eta\,\varphi(\eta/\xi)$$. Прежде всего, подстановка может быть некорректной, как в случае формул$$\forall \xi \forall\eta\, B(\xi,\eta) \quad\text{и}\quad \forall \eta \forall\eta\, B(\eta,\eta)$$ (легко понять, что эти формулы не эквивалентны). Но даже если подстановка корректна, формулы могут не быть эквивалентными, как в случае формул$$\forall \xi\, B(\xi,\eta) \quad\text{и}\quad \forall \eta\, B(\eta,\eta).$$ Как же сформулировать утверждение правильно?

Нагляднее всего, видимо, сделать так. Давайте заключим в рамку все связанные вхождения всех переменных (в том числе вхождения после кванторов). После этого соединим линиями переменную после квантора и все ее вхождения, связанные именно этим вхождением квантора. Свободные вхождения переменных остаются при этом без рамок. Получится что-то вроде(рис 10.1) Если после этого стереть переменные внутри рамок, получится схема формулы, которая содержит всю существенную информацию о ней. Будем называть две формулы подобными (отличающимися лишь именами связанных переменных), если они имеют одну и ту же схему.

Теорема 52. (переименование связанных переменных) Подобные формулы доказуемо эквивалентны.

Докажем две простые леммы.

Лемма 1. Если формула $$\varphi$$ не содержит переменной $$\eta$$ (ни связанно, ни свободно), то формулы$$\forall\xi\,\varphi \quad \text{и}\quad \forall\eta\,\varphi(\eta/\xi)$$ доказуемо эквивалентны.

Доказательство. В самом деле, подстановка корректна, так как в $$\varphi$$ нет кванторов по $$\eta$$. Поэтому выводима формула$$\forall\xi\,\varphi \to \varphi(\eta/\xi).$$ Левая часть ее не содержит переменной $$\eta$$, поэтому по правилу Бернайса можно вывести$$\forall\xi\, \varphi \to \forall\eta\,\varphi(\eta/\xi).$$

В обратную сторону: подстановка $$\xi$$ вместо $$\eta$$ в формулу $$\varphi(\eta/\xi)$$ корректна (поскольку $$\eta$$ была подставлена вместо свободных вхождений $$\xi$$, при обратной подстановке переменная $$\xi$$ не попадет в область действия кванторов по ней) и дает формулу $$\varphi$$. Поэтому формула$$\forall\eta\,\varphi(\eta/\xi)\to \varphi(\eta/\xi)(\xi/\eta)$$ или, что то же самое,$$\forall\eta\,\varphi(\eta/\xi)\to \varphi$$ является аксиомой. Осталось применить правило Бернайса, заметив, что в левую часть переменная $$\xi$$ свободно не входит (все свободные вхождения были заменены на $$\eta$$ ). Лемма 1 доказана.

Аналогичное утверждение для квантора существования доказывается точно так же.

Лемма 2. Замена подформулы на доказуемо эквивалентную дает доказуемо эквивалентную формулу.

Доказательство. Как мы видели, доказуемая эквивалентность сохраняется после навешивания квантора: если $$\alpha\hm\simeq\alpha'$$, то $$\forall\xi\,\alpha\hm\simeq\forall\xi\,\alpha'$$ и $$\exists\xi\,\alpha\hm\simeq\exists\xi\,\alpha'$$ (символ $$\simeq$$ здесь обозначает доказуемую эквивалентность). Кроме того, из $$\alpha\hm\simeq\alpha'$$ и $$\beta\hm\simeq\beta'$$ следует, что $${(\alpha\land\beta)}\hm\simeq{(\alpha'\land\beta')}$$, $${(\alpha\lor\beta)}\hm\simeq{(\alpha'\lor\beta')}$$, $${(\alpha\to\beta)}\hm\simeq{(\alpha'\to\beta')}$$ и $$\lnot\alpha\hm\simeq\lnot\alpha'$$. (В этом легко убедиться, написав подходящие пропозициональные тавтологии.)

Теперь утверждение леммы легко доказать индукцией (начав с замененной подформулы и рассматривая все более длинные части формулы). Лемма 2 доказана.

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

(Использование третьей формулы существенно: мы не можем преобразовать первую формулу сразу во вторую, так как при замене переменных в рамках может не выполняться условие леммы 1.)

Аккуратное обращение со связанными и свободными переменными — традиционная головная боль авторов учебников по логике. Наиболее радикальный подход — вообще изгнать связанные переменные, заменив их квадратиками со связями между ними. Тогда при подстановке можно ни о чем не заботиться. Зато формулы перестают быть последовательностями символов, а становятся объектами со сложной структурой. (Этот подход использован в книге Бурбаки Теория множеств [3].)

Менее радикальный вариант состоит в том, чтобы разделить переменные на два типа — свободные и связанные. Так делается, например, в классической книге Гильберта и Бернайса Основания математики [8]. Тогда можно смело подставлять терм вместо свободной переменной, зато при навешивании квантора надо заменять свободную переменную на связанную.

Еще один вариант — договориться, что при подстановке терма вместо свободной переменных автоматически происходит переименование связанных переменных, создающих коллизии.

Все это, конечно, мелочи — но досадные, особенно если стремиться к краткости, ясности и наглядности. Следы мучительных раздумий на подобные темы видны в примечании книги Клини Математическая логика [16]: " Гильберт и Бернайс $$\langle\dots\rangle$$ и другие авторы используют для обозначения свободных и связанных переменных разные буквы $$\langle\dots\rangle$$ Мы следовали этому правилу в течение десятилетия $$\langle\dots\rangle$$ Сейчас же мы твердо убеждены, что использование единого списка переменных для свободных и замкнутых вхождений дает небольшое, но чувствительное преимущество".

С этим связан и другой выбор: как определять истинность формул. Тут есть две возможности: можно определять истинность формулы на оценке (при данных значениях параметров), а можно говорить только о замкнутых формулах, вводя константы для всех элементов интерпретации. И тот, и другой способы имеют недостатки, а выбор нами первого подхода — результат не единодушия авторов, а волевого решения.