Дискуссионный математический форумМатематический форум

Математический форум Math Help Planet

Обсуждение и решение задач по математике, физике, химии, экономике

Теоретический раздел
Часовой пояс: UTC + 4 часа [ Летнее время ]
MathHelpPlanet.com RSS-лента Математического форума

Часовой пояс: UTC + 4 часа [ Летнее время ]


Свойства формализованного исчисления предикатов

Свойства формализованного исчисления предикатов


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


Оправданность аксиоматизации


Теорема оправданности аксиоматизации утверждает, что если [math]\Phi\vdash F[/math], то [math]\Phi\vDash F[/math], т.е. из синтаксической выводимости следует семантическая выводимость. Ее очевидным следствием будет утверждение о том, что всякая теорема ФИП является общезначимой формулой (тавтологией) логики предикатов. Смысл этой теоремы состоит в утверждении фактически того, что мы не были "излишне щедры" в выборе аксиом и правил вывода для нашего формального исчисления и не включили в их число ничего лишнего, ибо доказуемыми в этом исчислении оказываются лишь общезначимые формулы логики предикатов. Доказательство этой теоремы не очень сложное, и мы получим ее в качестве следствия несколько более общей теоремы. Обратное же утверждение "если [math]\Phi\vDash F[/math], то [math]\Phi\vdash F[/math] (т.е. при выборе аксиом и правил вывода мы не проявили и "излишней скромности", и для всякой общезначимой формулы логики предикатов в нашем ФИП вполне достаточно формальных средств, чтобы доказать ее), уже не столь очевидно, и доказательство его, приводимое дальше, потребует от нас значительно больших усилий.


Теорема оправданности имеет глубокий смысл: она оправдывает наши занятия математикой, убеждая в том, что наши логические рассуждения и умопостроения не уводят нас от смысла и от практики.


Теорема 29.1. Если в алгебраической системе [math]\mathbf{M}[/math] выполняются все формулы из множества [math]\Phi[/math] и из [math]\Phi[/math] синтаксически выводима формула [math]F[/math], то [math]F[/math] также выполняется в [math]\mathbf{M}\colon \mathbf{M}\vDash \Phi[/math] и [math]\Phi\vdash F \Rightarrow \mathbf{M}\vDash F[/math].


Доказательство разделим на три этапа. На первом этапе отметим, что каждая аксиома ФИП есть тождественно истинная формула. Что касается аксиом [math]A1,\,A2,\,A3[/math] исчисления высказываний, то их тождественная истинность установлена нами в алгебре высказываний (см. теоремы 3.1 з, 3.3, а, л). Общезначимость аксиом [math]\mathsf{PA1}[/math] и [math]\mathsf{PA2}[/math] установлена в теореме 21.13.


На втором этапе покажем, что все три правила вывода, используемые в ФИП, обладают следующим семантическим свойством. Если алгебраическая система [math]\mathbf{M}[/math] служит моделью для всех посылок правила вывода, то [math]\mathbf{M}[/math] будет моделью и для формулы, получаемой из данных формул с помощью данного правила вывода. Докажем это утверждение для трех из правил вывода.


Правило MP. Допустим, что [math]\mathbf{M}\vDash F\to G[/math] и [math]\mathbf{M}\vDash F[/math]. Докажем, что тогда [math]\mathbf{M}\vDash G[/math]. Возьмем любую подстановку [math]\alpha[/math] констант из [math]\mathbf{M}[/math]. Тогда, по условию, каждое из высказываний [math]F(\alpha)\to G(\alpha)[/math] и [math]F(\alpha)[/math], получаемых соответственно из формул [math]F\to G[/math] и [math]F[/math] в результате подстановки предметных констант [math]\alpha[/math], будет истинным. Тогда истинным будет и высказывание [math]F(\alpha)[/math], то есть [math]\mathbf{M}\vDash_{\alpha}G[/math]. Это и означает, что [math]\mathbf{M}\vDash G[/math].


∀-правило. Допустим, что [math]\mathbf{M}\vDash G(y)\to F(x,y)[/math], где [math]x[/math] не входит свободно в формулу [math]G[/math], а [math]y[/math] обозначает все свободные предметные переменные в формулах [math]F[/math] и [math]G[/math][math]F[/math] — кроме [math]x[/math]). Тогда сделанное допущение означает, что для любых элементов [math]a,b\in M[/math] (где [math]M[/math] — носитель алгебраической системы [math]\mathbf{M}[/math]) высказывание [math]G(b)\to F(a,b)[/math] истинно в [math]\mathbf{M}[/math]. Рассмотрим теперь высказывание [math]G(b)\to (\forall x)(F(x,b))[/math] и покажем, что оно истинно в [math]\mathbf{M}[/math] при любом [math]b\in M[/math]. В самом деле, если [math]G(b)[/math] ложно, то рассматриваемое высказывание истинно. Если же [math]G(b)[/math] истинно, то, по отмеченному выше, истинным будет и высказывание [math]F(a,b)[/math]. Поскольку оно будет истинным при любом [math]a\in M[/math], то отсюда вытекает истинность для таких [math]b\in M[/math] высказывания [math](\forall x)(F(x,b))[/math]. Это, в свою очередь, влечет истинность высказывания [math]G(b)\to (\forall x)(F(x,b))[/math] для тех [math]b\in M[/math], для которых [math]G(b)[/math] истинно. Итак, высказывание [math]G(b)\to (\forall x)(F(x,b))[/math] истинно для любых [math]b\in M[/math]. Это и означает, что [math]\mathbf{M}\vDash G(y)\to (\forall x)(F(x,y))[/math].


∃-правило. Подобно предыдущему правилу, доказывается, что если [math]\mathbf{M}\vDash F(x)\to G[/math], то [math]\mathbf{M}\vDash (\exists x)(F(x))\to G[/math].


Наконец, на третьем этапе докажем утверждение самой теоремы. Пусть [math]\mathbf{M}\vDash \Phi[/math] и [math]\Phi\vdash F[/math]. Последнее означает, что имеется вывод [math]B_1,B_2,\ldots,B_m[/math] формулы [math]F[/math] из множества формул [math]\Phi[/math] (в частности, [math]B_m\equiv F[/math]). Покажем, что каждый элемент этой последовательности является формулой, выполняющейся в [math]\mathbf{M}[/math]. Доказательство проведем индукцией по номеру [math]k[/math] формулы в рассматриваемом выводе. При [math]k=1[/math], если [math]B_1\in\Phi[/math], то, по условию, [math]\mathbf{M}\vDash B_1[/math]. Если [math]B_1[/math] — аксиома, то она общезначима и, в частности, [math]\mathbf{M}\vDash B_1[/math]. Предположим теперь, что при всех [math]k<n~(n\geqslant2)[/math] все формулы [math]B_k[/math] выполняются в [math]\mathbf{M}[/math], то есть [math]\mathbf{M}\vDash B_k[/math]. Рассмотрим формулу [math]B_n[/math]. Если [math]B_n\in\Phi[/math] или [math]B_n[/math] — аксиома, то, как отмечено выше, [math]\mathbf{M}\vDash B_n[/math]. Если же [math]B_n[/math] получена из предыдущих формул последовательности по одному из трех правил вывода, то (на основании выполнимости всех предыдущих формул в [math]\mathbf{M}[/math]) в силу утверждений (см. второй этап) заключаем, что и [math]B_n[/math] выполняется в [math]\mathbf{M}[/math], то есть [math]\mathbf{M}\vDash B_n[/math]. Окончательно заключаем, что все формулы последовательности [math]B_1,B_2,\ldots,B_m[/math] истинны в [math]\mathbf{M}[/math], в частности [math]\mathbf{M}\vDash F[/math]. Теорема полностью доказана.


Следствие 29.2 (теорема оправданности). Из синтаксической выводимости следует семантическая выводимость, т. е. если [math]\Phi\vdash F[/math], то [math]\Phi\vDash F[/math].


Доказательство. Пусть [math]\Phi\vdash F[/math] и пусть [math]\mathbf{M}[/math] — любая алгебраическая система, в которой выполняются все формулы из [math]\Phu[/math], то есть [math]\mathbf{M}\vDash\Phi[/math]. Тогда по доказанной теореме [math]\mathbf{M}\vDash F[/math]. По определению семантического следствия это и означает, что [math]\Phi\vDash F[/math].


Следствие 29.3. Всякая доказуемая формула является общезначимой (т.е. любая теорема истинна): если [math]\vdash F[/math], то [math]\vDash F[/math].


Доказательство получается из предыдущего следствия при [math]\Phi=\varnothing[/math].




Непротиворечивость формализованного исчисления предикатов


Важнейшим компонентом критерия оправданности всякой математической теории является ее непротиворечивость, т.е. невозможность доказательства в ней некоторого утверждения и его отрицания одновременно. Трудности, связанные с доказательством этого свойства математических теорий (а одной из причин этих трудностей, несомненно, было отсутствие в содержательных математических теориях точного понятия доказательства), привели к тому, что в математике более естественным стал другой признак непротиворечивости теории, основанный на возможностях реализации этой теории, ее моделируемости. Но в то же время этот подход и привел к возникновению парадоксов в математике, которые, в свою очередь, привели к возникновению науки об основаниях математики и к концепциям формального подхода к понятиям доказательства и математической (аксиоматической) теории. Одной из задач этого подхода была выработка такого формального понятия доказательства, при котором для конкретной математической теории понятие ее формальной непротиворечивости совпало бы с понятием ее содержательной непротиворечивости. Факт такого совпадения, в силу точности определения доказательства, становится математической теоремой (точнее, метатеоремой). Отметим, что привыкание в математике к эквивалентности этих двух понятий непротиворечивости было непростым. В частности, неприятие современниками неевклидовых геометрий Лобачевского–Бояи объясняется также и тем, что законность этих теорий обосновывалась отсутствием в них противоречий — аргументом, совпадающим по существу с современным понятием формальной непротиворечивости. Геометрические модели для этих теорий, доказывающие их содержательную непротиворечивость, были найдены позднее.


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


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


Определение 29.4. Формальная теория называется семантически непротиворечивой, если ни одна из ее теорем (формул) не является противоречивой, т. е. ложной при любой ее интерпретации. Аналогично, множество [math]\Phi[/math] формул называется семантически непротиворечивым, если ни одна формула, выводимая из [math]\Phi[/math], не является противоречивой.


В теореме 16.1 доказано, что всякая теорема формализованного исчисления высказываний общезначима (тождественно истинна), а потому не является противоречивой. Это означает, что формализованное исчисление высказываний семантически непротиворечиво. Аналогичная теорема доказана и для формализованного исчисления предикатов (см. следствие 29.3 из теоремы 29.1 выше). Значит, и ФИП семантически непротиворечиво. Семантическая непротиворечивость ФИВ и ФИП означает, что эти формальные теории пригодны для описания любых классов алгебраических систем, т.е. они войдут в теории этих классов составными частями, что вполне соответствует общенаучному принципу универсальности законов логики (Лейбниц формулировал его как выполнимость логических законов "во всех мыслимых мирах").


Произвольная формальная теория [math]T[/math] есть теория множества [math]M(T)[/math] всех своих моделей, а значит, теория [math]T[/math] семантически непротиворечива, если и только если [math]\mathbf{M}(T)\ne \varnothing[/math], т.е. для теории [math]T[/math] существует модель. Если отождествить пригодность математической теории, ее целесообразность с ее семантической непротиворечивостью, то можно сказать, что сформулированный критерий пригодности теории известен уже давно. Отыскание модели для теории до возникновения оснований математики было единственным общепризнанным методом доказательства "законности" теории. Математическая логика выработала аналог этого критерия, не опирающийся на наличие модели теории — внешний фактор по отношению к теории, а опирающийся на внутренние свойства самой теории, — понятие синтаксической непротиворечивости теории.


Определение 29.5. Формальная теория [math]T[/math] называется синтаксически (или дедуктивно, или формально) непротиворечивой, если не существует такой формулы [math]F[/math], что [math]F[/math] и [math]\lnot F[/math] являются теоремами теории [math]T[/math], т.е. в [math]T[/math] невыводимыми являются одновременно формула и ее отрицание. Аналогичное определение можно сформулировать и для произвольного множества [math]\Phi[/math] формул: [math]\Phi[/math] называется синтаксически непротиворечивым, если из [math]\Phi[/math] невыводимы одновременно формула и ее отрицание.


В теореме 16.9 доказана синтаксическая непротиворечивость формализованного исчисления высказываний. Аналогично доказывается следующая теорема.


Теорема 29.6. Формализованное исчисление предикатов синтаксически непротиворечиво.


Доказательство. Допустим противное, т.е. предположим, что ФИП синтаксически противоречиво. Значит, найдется такая формула [math]F[/math], что [math]F[/math] и [math]\lnot F[/math] будут теоремами ФИП. Тогда по следствию 29.3 из теоремы 29.1 формулы Fa -,Fбудут общезначимыми, что невозможно на основании определения общезначимости.


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


Лемма 29.7. Если множество формул имеет модель, то это множество семантически непротиворечиво.


Доказательство. Если множество [math]\Phi[/math] формул имеет модель [math]\mathbf{M}[/math], то ни одна формула, выводимая из [math]\Phi[/math], не является противоречивой, т.е. ложной во всякой интерпретации, ибо в противном случае она была бы ложна и в [math]\mathbf{M}[/math] (что невозможно в силу теоремы 29.1). Это и означает, что [math]\Phi[/math] семантически непротиворечиво.


Теорема 29.8. Если множество формул семантически непротиворечиво, то оно синтаксически непротиворечиво.


Доказательство. Допустим, что некоторое множество [math]\Phi[/math] формул узкого исчисления предикатов семантически непротиворечиво, но противоречиво синтаксически. Следовательно, из него выводима некоторая формула [math]F[/math] и ее отрицание [math]\lnot F[/math]. Но тогда из [math]\Phi[/math] выводима и их конъюнкция (по правилу введения конъюнкции) [math]F\land\lnot F[/math]. Но эта формула ложна в любой интерпретации, что означает, что множество [math]\Phi[/math] семантически противоречиво. Получаем противоречие, доказывающее, что [math]\Phi[/math] синтаксически непротиворечиво.


Непосредственно из предыдущих леммы и теоремы вытекает такое следствие.


Следствие 29.9. Если множество формул имеет модель, то оно синтаксически непротиворечиво.




Теорема Гёделя о существовании модели


Утверждение, обратное следствию, также оказывается справедливым. Но с конструктивной точки зрения оно оказывается более глубоким. Смысл его состоит в том, что всякое множество формул не только имеет модель, но эту модель можно конструктивно построить. Доказательство этого факта как раз и заключается в изложении метода такого построения. Это еще одна из замечательных теорем Гёделя (теорема о существовании модели), относящаяся к важнейшим теоремам математической логики. Она доказана Гёделем в 1930 г.


Теорема 29.10 (теорема Гёделя о существовании модели). Любое синтаксически непротиворечивое множество [math]\Sigma[/math] замкнутых формул узкого исчисления предикатов сигнатуры [math]\sigma[/math] имеет модель.


▼ Доказательство

Пусть сигнатура [math]\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots\bigr\}[/math]. Требуется построить модель [math]\mathbf{M}= <M;\, a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots>[/math], такую, что [math]\mathbf{M}\vDash\Sigma[/math] (т.е. в алгебраической системе [math]\mathbf{M}[/math] выполняются все формулы из [math]\Sigma[/math]). Эта модель будет строиться из слов некоторого алфавита. Под непротиворечивостью всюду в этом доказательстве будем понимать синтаксическую непротиворечивость.


Прежде всего расширим данную сигнатуру [math]\sigma[/math] до [math]\sigma'[/math] введением новых индивидных констант: [math]\sigma'= \sigma\cup\{c_0,c_1,\ldots,c_n,\ldots\}[/math], где все [math]c_i[/math] отличны от всех символов из [math]\sigma[/math]. Далее будем работать с формулами расширенной сигнатуры [math]\sigma'[/math]. Поскольку все такие (замкнутые) формулы являются конечными словами некоторого счетного алфавита, то множество всех таких формул имеет счетную мощность и мы можем все их расположить в последовательность (т.е. занумеровать натуральными числами). Итак, пусть [math]A_0,A_1,\ldots,A_n,\ldots[/math] — множество всех предложений (замкнутых формул) сигнатуры [math]\sigma'[/math].


Построим далее последовательность (цепочку)


[math]\Sigma_0\subseteq \Sigma_1\subseteq \ldots\subseteq \Sigma_n\subseteq\ldots[/math]
(1)

множеств замкнутых формул следующим образом:


а) [math]\Sigma_0=\Sigma[/math];


б) если [math]\Sigma_n\cup\{A_n\}[/math] противоречиво, то [math]\Sigma_{n+1}= \Sigma_n\cup \{\lnot A_n\}[/math];


в) если [math]\Sigma_n\cup\{A_n\}[/math] непротиворечиво и [math]A_n[/math] не начинается с квантора существования, то [math]\Sigma_{n+1}= \Sigma_n\cup\{A_n\}[/math];


г) если [math]\Sigma_n\cup\{A_n\}[/math] непротиворечиво и [math]A_n\equiv (\exists x)(B(x))[/math], то [math]\Sigma_{n+1}= \Sigma_n\cup\{A_n, B(c_k)\}[/math], где [math]c_k\in \sigma'\setminus \sigma[/math] — новая константа с наименьшим номером [math]k[/math], не встречающаяся в формуле [math]A_n[/math] и во всех формулах множества [math]\Sigma_n[/math].


1) Докажем сначала, что каждое множество [math]\Sigma_n[/math] построенной последовательности будет непротиворечивым множеством формул исчисления предикатов сигнатуры [math]\sigma'[/math]. Доказательство будем вести индукцией по [math]n[/math].


с) База индукции: [math]n=0[/math]. Так как [math]\Sigma_0=\Sigma[/math], то по условию [math]\Sigma_0[/math] непротиворечиво в исчислении предикатов сигнатуры [math]\sigma[/math]. Докажем, что оно непротиворечиво и в исчислении сигнатуры [math]\sigma'[/math]. Допустим противное, т.е. [math]\Sigma_0\vdash F[/math] и [math]\Sigma_0\vdash\lnot F[/math], где [math]F[/math] — формула сигнатуры [math]\sigma'[/math]. Следовательно, [math]\Sigma\vdash F[/math] и [math]\Sigma\vdash\lnot F[/math]. Это означает, что в [math]\Sigma[/math] имеется такое конечное подмножество формул [math]G_1,G_2,\ldots,G_m[/math], что [math]G_1,G_2,\ldots,G_m\vdashF,\lnot F[/math]. Пусть [math]B_1,B_2,\ldots,B_s\equiv F[/math]— вывод формулы [math]F[/math] из гипотез [math]G_1,G_2,\ldots,G_m[/math] в исчислении предикатов сигнатуры [math]\sigma'[/math]. Допустим, что [math]c_{i_1},c_{i_2},\ldots,c_{i_p}[/math] — все те новые константы, которые входят в формулы этого вывода.


Поскольку ∀- и ∃-правила вывода к константам не применяются, то, заменив все новые константы [math]c_{i_1},c_{i_2},\ldots,c_{i_p}[/math] предметными переменными, не входящими в формулы [math]B_1,B_2,\ldots,B_s[/math], получим новую последовательность формул [math]\widetilde{B}_1, \widetilde{B}_2,\ldots, \widetilde{B}_s[/math] исчисления предикатов уже сигнатуры [math]\sigma[/math], представляющую собой вывод в этом исчислении ее последней формулы [math]\widetilde{B}_s\equiv \widetilde{F}[/math]. Аналогично доказывается, что в исчислении сигнатуры [math]\sigma[/math] из множества [math]\Sigma[/math] выводима формула [math]\lnot \widetilde{F}[/math]. Получается противоречие с условием, согласно которому [math]\Sigma[/math] — непротиворечиво в исчислении сигнатуры [math]\sigma[/math].


Таким образом, [math]\Sigma_0[/math] непротиворечиво в исчислении сигнатуры [math]\sigma[/math].


Шаг индукции. Предположим, что [math]\Sigma_n[/math] непротиворечиво в исчислении предикатов сигнатуры [math]\sigma'[/math]. Покажем, что тогда таким же свойством обладает и множество [math]\Sigma_{n+1}[/math]. Согласно определению для него возможны следующие случаи:


б) [math]\Sigma_{n}\cup\{A_n\}[/math] противоречиво. В этом случае [math]\Sigma_{n+1}= \Sigma_{n}\cup\{\lnot A_n\}[/math]. Допустим, что последнее множество противоречиво. Тогда [math]\Sigma_{n},\lnot A_n\vdash F[/math] и [math]\Sigma_{n},\lnot A_n\vdash\lnot F[/math] для некоторой формулы [math]F[/math]. Тогда для некоторого конечного подмножества [math]\Gamma\subset \Sigma_{n}\colon \Gamma,\lnot A_n\vdash F[/math] и [math]\Gamma,\lnot A_n\vdash\lnot F[/math]. Отсюда по производному правилу вывода [math]\lnot[/math]–вв получим [math]\Gamma\vdash\lnot\lnot A_n[/math], то есть [math]\Gamma\vdash A_n[/math], а значит, [math]\Sigma_n\vdash A_n[/math].


В то же время из условия противоречивости множества [math]\Sigma_n\cup\{A_n\}[/math] аналогичные рассуждения приведут к заключению: [math]\Sigma_n\vdash\lnot A_n[/math].


Эти два заключения говорят о противоречивости множества [math]\Sigma_n[/math], что противоречит предположению индукции;


в) [math]\Sigma_n\cup\{A_n\}[/math] непротиворечиво и [math]A_n[/math] не начинаются с квантора существования. В этом случае по определению [math]\Sigma_{n+1}= \Sigma_n\cup \{A_n\}[/math], а значит, [math]\Sigma_{n+1}[/math] — непротиворечиво;


г) [math]\Sigma_n\cup\{A_n\}[/math] непротиворечиво и [math]A_n[/math] начинается с квантора существования: [math]A_n\equiv (\exists x)(B(x))[/math]. В этом случае [math]\Sigma_{n+1}[/math] получается добавлением к [math]\Sigma_n[/math] двух формул [math]A_n[/math] и [math]B(c_k)[/math], где [math]B(c_k)[/math] получена из [math]B(x)[/math] подстановкой константы [math]c_k[/math] (первой из [math]c_0,c_1,\ldots[/math], не входящей в [math]A_n[/math] и все формулы из [math]\Sigma_{n}[/math]) вместо предметной переменной [math]x\colon\, \Sigma_{n+1}= \Sigma_{n}\cup\{A_n,B(c_k)\}[/math]. Допустим, что [math]\Sigma_{n+1}[/math] противоречиво, т.е. [math]\Sigma_{n+1}\vdash F,\lnot F[/math]. Тогда найдется такое конечное подмножество [math]\Gamma\subset\Sigma_{n}[/math], что [math]\Gamma, (\exists x)(B(x)),\, B(c_k)\vdash F[/math] и [math]\Gamma,(\exists x)(B(x)),\,B(c_k)\vdash\lnot F[/math].


Поскольку в выводах этих формул ∀-правило и ∃-правило вывода не применяются к константе [math]c_k[/math], то, заменив в них эту константу новой переменной [math]y[/math], не участвующей в выводах этих формул, получим выводы, доказывающие, что [math]\Gamma,\,(\exists x)(B(x)),\, B(y_k)\vdash \widetilde{F}[/math] и [math]\Gamma,\, (\exists x)(B(x)),\, B(y_k)\vdash\lnot \widetilde{F}[/math], где [math]\widetilde{F}[/math], получена из [math]F[/math] заменой константы [math]c_k[/math] на предметную переменную [math]y[/math] ([math]y[/math] — фиксированная переменная в этих выводах). Из двух последних выводимостей по производному правилу вывода (введения отрицания [math]\lnot[/math]-вв) получаем: [math]\Gamma,\,(\exists x)(B(x))\vdash\lnot B(y)[/math]. Отсюда по правилу введения квантора общности получаем


[math]\Gamma,~ (\exists x) \bigl(B(x)\bigr)\vdash (\forall y)\bigl(\lnot B(y)\bigr).[/math]
(2)

Кроме того, легко получается выводимость [math](\forall y)(\lnot B(y))\vdash\lnot (\exists y)(B(y))[/math]. Наконец, в силу выбора переменной [math]y[/math], которая свободна для [math]x[/math] в формуле [math]B(x)[/math], и на основании правила переименования связанных переменных из последней выводимости заключаем, что


[math](\forall y)\bigl(\lnot B(y)\bigr)\vdash\lnot (\exists x)\bigl(B(x)\bigr).[/math]
(3)

Из выводимостей (2) и (3), в силу транзитивности отношения выводимости (см. теорему 15.3, в), получаем:


[math]\Gamma,~ (\exists x)\bigl(B(x)\bigr)\vdash\lnot (\exists x) \bigl(B(x)\bigr).[/math]

Учитывая, что [math](\exists x)(B(x))\equiv A_n[/math], можно заключить, что множество [math]\Gamma\cup\{A_n\}[/math] противоречиво. Поскольку[math]\Gamma\subset\Sigma_n[/math], то [math]\Gamma\cup\{A_n\}\subset \Sigma_n\subset \{A_n\}[/math], а значит, множество [math]\Sigma_n\cup\{A_n\}[/math] также противоречиво, что противоречит исходному условию.


Следовательно, и в этом случае множество [math]\Sigma_{n+1}[/math] непротиворечиво.


2) Рассмотрим теперь множество [math]\Sigma^{\ast}=\cup\Sigma_{n}[/math] (объединение берется по [math]n[/math] от 0 до [math]\infty[/math]). Отметим два свойства этого множества формул. Во-первых, множество [math]\Sigma^{\ast}[/math] непротиворечиво. В самом деле, если бы из [math]\Sigma^{\ast}[/math] выводились формулы [math]F[/math] и [math]\lnot F[/math], то они выводились бы из конечного подмножества множества [math]\Sigma^{\ast}[/math], которое включалось бы в некоторое [math]\Sigma_{n}[/math] которое, следовательно, было бы противоречивым. Но это не так в силу предыдущего п. 1 доказательства. Во-вторых, для любой формулы [math]A[/math] исчисления предикатов сигнатуры [math]\sigma'~A\in \Sigma^{\ast}[/math] или [math]\lnot A\in \Sigma^{\ast}[/math] (свойство полноты множества [math]\Sigma^{\ast}[/math]). Это вытекает непосредственно из построения [math]\Sigma^{\ast}[/math], так как [math]A=A_n[/math] для некоторого натурального [math]n[/math].


Последнее свойство можно сформулировать несколько в ином виде. Сначала отметим, что [math]A\in \Sigma^{\ast}\Leftrightarrow \Sigma^{\ast}\vdash A[/math]. В самом деле, импликация слева направо очевидна. Предположив, что [math]\Sigma^{\ast}\vdash A[/math] и [math]A\notin \Sigma^{\ast}[/math], в силу отмеченного свойства получим [math]\lnot A\in\Sigma^{\ast}[/math]. В итоге получаем, что [math]\Sigma^{\ast}[/math] противоречиво, что противоречит первому отмеченному выше свойству.


Следовательно, второе отмечаемое утверждение принимает вид: [math]\Sigma^{\ast}\vdash A[/math] или [math]\Sigma^{\ast}\vdash\lnot A[/math] для любой формулы [math]A[/math].


3) Построим теперь саму модель [math]\mathbf{M}[/math]. Напомним, что ее сигнатура [math]\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots\bigr\}[/math]. Рассмотрим всевозможные термы расширенной сигнатуры [math]\sigma'[/math], не содержащие предметных переменных, а содержащие лишь предметные константы [math]a_0,a_1,\ldots,\, c_0,c_1,\ldots[/math]. Напомним, что термы представляют собой либо сами эти константы, либо выражения вида [math]f_i(t_1,\ldots,t_{n_i})[/math], где [math]f_i[/math] — функциональный символ из [math]\sigma[/math], a [math]t_1,\ldots,t_{n_i}[/math] — термы. Множество всех этих термов и есть базисное множество [math]M[/math] модели [math]\mathbf{M}[/math]. Сигнатурные операции на этом множестве зададим следующим образом:


[math]a_{i}^{M}= a_i,~ f_{i}^{M}(t_1,\ldots,t_{n_i})= f_i(t_1,\ldots,t_{n_i}),\quad i=0,1,2, \ldots[/math]

Наконец, выполнимость на [math]\mathbf{M}[/math] соответствующего сигнатурного отношения определим следующим образом:


[math]\mathbf{M}\vDash P_{j}^{M}(t_1,\ldots,t_{n_i})~ \Leftrightarrow~ \Sigma^{\ast}\vdash P_{j}(t_1,\ldots,t_{n_i}).[/math]
(4)

4) Проверим, что алгебраическая система [math]\mathbf{M}[/math] сигнатуры о действительно является моделью исходного множества [math]\Sigma[/math] формул исчисления предикатов сигнатуры [math]\sigma[/math], то есть [math]\mathbf{M}\vDash\Sigma[/math]. Для этого докажем сначала, что для всякой формулы [math]F(x_1,\ldots,x_n)[/math] сигнатуры [math]\sigma'[/math] и любых термов [math]t_1,\ldots,t_n\in M[/math] имеет место-следующее утверждение:


[math]\mathbf{M}\vDash F(t_1,\ldots,t_n)~ \Leftrightarrow~ \Sigma^{\ast}\vdash F(t_1,\ldots,t_n).[/math]
(5)

Доказательство будем вести индукцией по числу [math]k[/math] логических знаков, используемых при построении формулы [math]F[/math].


База индукции: [math]k=0[/math]. Тогда [math]F[/math] — атомарная формула, имеющая вид [math]P_j(t_1,\ldots,t_{m_j})[/math], а для нее утверждение (5) верно по определению (4).


Шаг индукции. Предположим, что для всех формул, в записи которых число логических символов [math]\leqslant k[/math], утверждение (5) верно. Пусть [math]F[/math] — произвольная формула, в записи которой участвует [math]k+1[/math] логический символ. Покажем, что тогда утверждение (5) будет справедливо и для нее. На основании определения (формулы) формула F имеет один из следующих видов: [math]\lnot A,\,A\to B,\, (\forall x)(B(x)),\, (\exists x)(B(x))[/math]. Рассмотрим последовательно каждый из этих случаев.


а)[math]F\equiv\lnot A[/math]. Предположим, что [math]\mathbf{M}\vDash\lnot A(t_1,\ldots, t_n)[/math]. Тогда по определению отрицания это означает, что [math]A(t_1,\ldots, t_n)[/math] не выполняется на [math]\mathbf{M}\colon\, \mathbf{M}\nvDash A(t_1,\ldots, t_n)[/math]. Отсюда по предположению индукции заключаем, что [math]\Sigma^{\ast}\nvdash A(t_1,\ldots, t_n)[/math]. Следовательно, по свойству полноты множества [math]\Sigma^{\ast}[/math], отмеченному в п. 2 настоящего доказательства, [math]\Sigma^{\ast}\vdash\lnot A(t_1,\ldots, t_n)[/math]. Легко видеть, что каждое утверждение настоящего рассуждения допускает обращение, так что


[math]\mathbf{M}\vDash\lnot A(t_1,\ldots, t_n)~ \Leftrightarrow~ \Sigma^{\ast}\vdash\lnot A(t_1,\ldots, t_n).[/math]

б) [math]F\equiv A\to B[/math]. Предположим, что [math]\mathbf{M}\vDash A(t_1,\ldots, t_n)\to B(t_1,\ldots, t_n)[/math]. Используя определения импликации, конъюнкции и отрицания, определение (4), полноту [math]\Sigma^{\ast}[/math] и предположение индукции для формул [math]A[/math] и [math]B[/math], проводим следующее рассуждение:


[math]\mathbf{M}\vDash A\to B \Leftrightarrow \mathbf{M}\vDash\lnot(A\land\lnot B) \Leftrightarrow \mathbf{M}\nvDash A\land\lnot B \Leftrightarrow \mathbf{M}\nvDash A[/math], или [math]\mathbf{M}\nvDash\lnot B \Leftrightarrow \mathbf{M}\nvDash A[/math],

или [math]\mathbf{M}\vDash B \Leftrightarrow \Sigma^{\ast}\nvdash A[/math], или [math]\Sigma^{\ast}\vdash B \Leftrightarrow \Sigma^{\ast}\vdash\lnot A[/math], или [math]\Sigma^{\ast}\vdash B[/math].

Теперь мы находимся в области формализованного исчисления высказываний. Дальнейшие рассуждения таковы. Из каждого из утверждений [math]\Sigma^{\ast}\vdash\lnot A[/math] и [math]\Sigma^{\ast}\vdash B[/math] по правилу [math]\lor[/math]-вв следует [math]\Sigma^{\ast} \vdash\lnot A\lor B[/math], то есть [math]\Sigma^{\ast}\vdash A\to B[/math]. Теперь нужно проделать обратное рассуждение. Предположим, что [math]\Sigma^{\ast}\vdash A\to B[/math] и [math]\Sigma^{\ast}\vdash\lnot A[/math]. Следовательно, по второму свойству множества [math]\Sigma^{\ast}[/math] из п. 2 настоящего доказательства [math]\Sigma^{\ast}\vdash A[/math]. Тогда из выводимостей [math]\Sigma^{\ast}\vdash A\to B[/math] и [math]\Sigma^{\ast}\vdash A[/math] и правила MP [math](A\to B,~ A\vdash B)[/math] следует, что [math]\Sigma^{\ast}\vdash B[/math].


Итак, мы доказали, что [math]\mathbf{M}\vDash A\to B \Leftrightarrow \Sigma^{\ast}\vdash A\to B[/math].


в) [math]F\equiv (\forall x)(B(x,t_1,\ldots,t_n))[/math]. Предположим, что [math]\mathbf{M}= (\forall x)(B(x,t_1,\ldots,t_n))[/math]. По определению квантора общности это означает, что [math]\mathbf{M}\vDash B(t,t_1,\ldots,t_n)[/math] для каждого элемента [math]t\in M[/math]. Таким образом, по предположению индукции (5) получим, что [math]\Sigma^{\ast}\vdash B(t,t_1,\ldots,t_n)[/math]. Отсюда, в силу правила введения квантора общности, заключаем, что [math]\Sigma^{\ast}\vdash (\forall x)(B(x,t_1,\ldots,t_n))[/math].


Обратно, пусть [math]\Sigma^{\ast}\vdash (\forall x)(B(x,t_1,\ldots,t_n))[/math]. Вместе с аксиомой [math]\mathsf{PA1}\colon (\forall x)(B(x,t_1,\ldots,t_n))\to B(t,t_1,\ldots,t_n)[/math], в силу правила MP, это дает: [math]\Sigma^{\ast}\vdash B(t,t_1,\ldots,t_n)[/math]. На основании предположения индукции (5) отсюда следует, что [math]\mathbf{M}\vDash B(t,t_1,\ldots,t_n)[/math]. Поскольку данная выполнимость на модели [math]\mathbf{M}[/math] имеет место для любого элемента [math]t\in M[/math], поэтому на основании определения квантора общности отсюда следует, что [math]\mathbf{M}\vDash (\forall x)(B(x,t_1,\ldots,t_n))[/math].


г) [math]F\equiv (\exists x)(B(x,t_1,\ldots,t_n))[/math]. Предположим, что [math]\mathbf{M}\vDash (\exists x)(B(x,t_1,\ldots,t_n))[/math]. Тогда по определению квантора существования [math]\mathbf{M}\vDash B(a_0,t_1,\ldots,t_n)[/math] для некоторого элемента [math]a_0\in M[/math]. В силу предположения индукции (5) отсюда получаем [math]\Sigma^{\ast}\vdash B(a_0,t_1,\ldots, t_n)[/math]. Вместе с аксиомой [math]\mathsf{PA2}\colon B(a_0,t_1,\ldots,t_n)\to (\exists x)(B(x,t_1, \ldots,t_n))[/math], в силу правила MP, это дает: [math]\Sigma^{\ast}\vdash (\exists x)(B(x,t_1,\ldots,t_n))[/math].


Обратно, пусть [math]\Sigma^{\ast}\vdash (\exists x)(B(x,t_1,\ldots,t_n))[/math]. Поскольку [math](\exists x)(B(x,t_1,\ldots,t_n))[/math] — замкнутая формула сигнатуры [math]\sigma'[/math], то она содержится в последовательности [math]A_1,A_2,\ldots,A_n,\ldots[/math] всех таких формул. Предположим, что это формула [math]A_m[/math]. Тогда множество [math]\Sigma_m\cup \{A_m\}[/math] непротиворечиво. (Если бы оно было противоречиво, то [math]\Sigma_{m+1}[/math] равнялось бы [math]\Sigma_m\cup \{\lnot A_m\}[/math], т.е. формула [math]\lnot A_m[/math] входила бы в множество [math]\Sigma^{\ast}[/math] и последнее было бы противоречивым, что не так в силу п. 2 настоящего доказательства.) Поскольку, кроме того, [math]A_m[/math] начинается с квантора существования, то в этом случае [math]\Sigma_{m+1}= \Sigma_{m}\cup \bigl\{A_m,\, B(c_k,t_1,\ldots,t_n)\bigr\}[/math] и, значит, [math]B(c_k,t_1,\ldots,t_n)\in \Sigma^{\ast}[/math]. Следовательно, для формулы [math]B(c_k,t_1,\ldots,t_n)[/math] по предположению индукции имеем [math]\mathbf{M}\vDash B(c_k,t_1,\ldots,t_n)[/math] для некоторой константы [math]c_k\in M[/math]. Тогда по определению квантора существования [math]\mathbf{M}\vDash (\exists x)(B(x,t_1,\ldots,t_n))[/math].


Итак, мы доказали, что всякая формула, выводимая из [math]\Sigma^{\ast}[/math] (и, в частности, принадлежащая [math]\Sigma^{\ast}[/math]), истинна (выполнима) на модели [math]\mathbf{M}[/math]. В частности, на [math]\mathbf{M}[/math] выполняются и все формулы исходной совокупности [math]\Sigma= \Sigma_0\subset \Sigma^{\ast}[/math], то есть [math]\mathbf{M}[/math] — действительно модель непротиворечивого множества формул £. Теорема полностью доказана.




Теоремы о непротиворечивости формул предикатов


Теорема Гёделя о существовании модели позволяет доказать теорему, обратную к теореме 29.8, и они вместе образуют следующую важную метатеорему.


Теорема 29.11 (о непротиворечивости). Множество формул узкого исчисления предикатов семантически непротиворечиво тогда и только тогда, когда оно синтаксически непротиворечиво.


Доказательство. Необходимость есть теорема 29.8. Обратно, если множество формул синтаксически непротиворечиво, то по теореме 29.10 оно имеет модель, а тогда по лемме 29.7 оно семантически непротиворечиво.


Наконец, объединим в одну метатеорему следствие из теоремы 29.8 и теорему 29.10. Получим следующее.


Теорема 29.12 (о непротиворечивости). Множество формул узкого исчисления предикатов синтаксически (дедуктивно) непротиворечиво тогда и только тогда, когда оно имеет модель.


Приведем интересный комментарий, который дает теореме о непротиворечивости известный логик Р. Линдон, по мнению которого доказательства (дедуктивной) непротиворечивости какой-либо теории посредством указания ее модели широко распространены в абстрактной математике. Менее очевидное из утверждений теоремы о непротиворечивости — о существовании модели у каждой дедуктивно непротиворечивой теории — используется далеко не так часто. Возможно, это объясняется тем, что математики не слишком-то большое значение придают понятию существования; теорему о непротиворечивости можно как раз и рассматривать как скромное, но зато точное выражение довольно-таки расплывчатого мнения, что существование в математике — это не что иное, как непротиворечивость.


Возможности применения теоремы о непротиворечивости к проблемам установления непротиворечивости конкретных теорий весьма ограниченны: дело в том, что построение модели обычно требует принятия в метаязыке допущений, значительно более сильных, нежели те, которые выражаются предметной теорией. Другой путь установления непротиворечивости какой-нибудь аксиоматической теории состоит в том, чтобы с помощью чисто синтаксических рассмотрений показать, что в данной теории нельзя доказать тождественно ложную формулу. Область применения этого метода, однако, также невелика. Теорема Гёделя не позволяет надеяться на получение доказательства непротиворечивости теории, если не допускать в теории, предназначенной для такого доказательства на метаязыке, по меньшей мере столь же сильных средств, что и в рассматриваемой предметной теории. Убеждение в непротиворечивости достаточно сложных математических теорий базируется в конечном счете на интуиции и опыте.




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


Доказав теорему Гёделя о существовании модели (теорема 29.10), можно доказать теорему, обратную теореме оправданности (следствие 29.2 из теоремы 29.1), т.е. утверждение о том, что из семантической выводимости следует синтаксическая выводимость. В самом деле, пусть [math]\Phi\vDash F[/math]. Покажем, что тогда множество формул [math]\Phi\cup\{\lnot F\}[/math] противоречиво. Допустим на время, что это не так. Тогда по теореме 29.10 это множество имеет модель [math]\mathbf{M}[/math], т.е. на [math]\mathbf{M}[/math] выполняется формула [math]\lnot F[/math] и все формулы из [math]\Phi[/math]. Из последнего, ввиду условия [math]\Phi\vDash F[/math], следует, что на [math]\mathbf{M}[/math] выполняется и формула [math]F[/math]. Получаем противоречие. Итак, множество [math]\Phi\cup\{\lnot F\}[/math] противоречиво. Значит, из него выводима любая формула, в частности [math]\Phi\cup\{\lnot F\}\vdash F[/math]. Тогда по теореме о дедукции имеем [math]\Phi\vdash\lnot F\to F[/math]. Учитывая, что, кроме того, формула [math](\lnot F\to F)\to F[/math] является теоремой ФИВ, по правилу MP заключаем, что [math]\Phi\vdash F[/math].


Итак, мы доказали, что если [math]\Phi\vDash F[/math], то [math]\Phi\vdash F[/math]. Объединив это утверждение со следствием 29.1 из теоремы 29.2, приходим к следующей важной метатеореме.


Теорема 29.13 (теорема адекватности). Формула [math]F[/math] синтаксически выводима из множества формул [math]\Phi[/math] тогда и только тогда, когда она семантически выводима из [math]\Phi\colon\, \Phi\vdash F \Leftrightarrow \Phi\vDash F[/math].


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


Заметим, что нетрудно показать, что теорема о существовании модели вытекает из теоремы адекватности. В самом деле, предположим, что [math]\Phi[/math] — непротиворечивое множество формул, не имеющее модели. Тогда ясно, что для любой формулы [math]F[/math] справедливо семантическое следование [math]\Phi\vDash F[/math]. В силу теоремы адекватности отсюда следует, что [math]\Phi\vdash F[/math] для любой [math]F[/math], что означает противоречивость множества [math]\Phi[/math], в противоречие с условием.


Теорема 29.14 (теорема Гёделя о полноте ФИП). Класс доказуемых замкнутых формул совпадает с классом общезначимых (или тождественно истинных) формул: [math]\vdash F \Leftrightarrow\vDash F[/math].


Доказательство. Эта теорема непосредственно вытекает из предыдущей при [math]\Phi= \varnothing[/math].


Справедлива она и для открытых формул. В самом деле, если [math]\vDash F(x_1,\ldots,x_n)[/math], где [math]x_1,\ldots,x_n[/math] — свободные предметные переменные в формуле [math]F[/math], то в силу определения квантора общности это будет равносильно тому, что [math]\vDash(\forall x_1)\ldots (\forall x_n) \bigl(F(x_1,\ldots,x_n)\bigr)[/math]. По теореме 29.14 это равносильно тому, что [math]\vdash(\forall x_1)\ldots (\forall x_n) \bigl(F(x_1,\ldots,x_n)\bigr)[/math]. В силу свойств выводимости последнее утверждение равносильно тому, что [math]\vdash F(x_1,\ldots,x_n)[/math].




Неполнота формализованного исчисления предикатов в абсолютном и узком смыслах


В учебнике обсуждаются два понятия полноты аксиоматической теории: абсолютная полнота и полнота в узком смысле (см. определение 27.6). Доказанная теорема 29.14 может быть истолкована как некая внешняя полнота формализованного исчисления предикатов, его полнота относительно логики предикатов: в этой теории могут быть формально доказаны все общезначимые формулы логики предикатов. Рассмотрим вопросы внутренней полноты формализованного исчисления предикатов, т.е. выясним, будет ли эта теория абсолютно полной и полной в узком смысле (см. определения 27.5 и 27.6). Поскольку на основании теоремы 29.14 множество теорем формализованного исчисления предикатов совпадает с множеством тавтологий (общезначимых формул) логики предикатов, а в логике предикатов существуют выполнимые, но не общезначимые формулы, формализованное исчисление предикатов не является абсолютно полной теорией. Здесь ситуация аналогична соответствующей ситуации в формализованном исчислении высказываний. Что же касается полноты формализованного исчисления предикатов в узком смысле, то исчисление предикатов (в отличие от исчисления высказываний, см. теорему 28.4) таким свойством не обладает. Для доказательства приведем пример формулы, не являющейся теоремой формализованного исчисления предикатов, добавление которой к аксиомам исчисления предикатов (с сохранением правил вывода) приводит к непротиворечивой формальной аксиоматической теории.


Пример 29.15. Рассмотрим формулу [math](\exists x)(F(x))\to (\forall x)(F(x))[/math]. Нетрудно убедиться в том, что она не является общезначимой (приведите пример конкретного одноместного предиката, превращающего эту формулу в ложное высказывание). Поэтому на основании теоремы К. Гёделя о полноте она не доказуема в формализованном исчислении предикатов. С другой стороны, добавив к аксиомам формализованного исчисления предикатов рассматриваемую формулу, получим непротиворечивую формальную теорию [math]T[/math]. Ее непротиворечивость можно доказать следующим образом.


Рассмотрим модель этой теории на одноэлементном множестве [math]M=\{a\}[/math]. Ясно, что данная формула тождественно истинна на [math]M[/math]. Далее, учитывая, что на [math]M[/math] можно определить для каждого натурального [math]n[/math] лишь два n-местных предиката [math]P_1^n[/math] и [math]P_2^n[/math], причем [math]\lambda(P_1^n(a,\ldots,a))=0[/math] и [math]\lambda(P_2^n(a,\ldots,a))=1[/math], нетрудно доказать, что все аксиомы новой теории [math]T[/math] тождественно истинны на этой модели и правила вывода от тождественно истинных на [math]M[/math] формул приводят к тождественно истинным на [math]M[/math] формулам. Таким образом, доказывается утверждение: всякая теорема теории [math]T[/math] тождественно истинна на одноэлементном множестве [math]M[/math].


Следовательно, если бы для некоторой формулы [math]F[/math] обе формулы [math]F[/math] и [math]\lnot F[/math] были теоремами теории [math]T[/math], то они были бы тождественно истинны на одноэлементном множестве [math]M[/math], что невозможно. Поэтому расширенная теория [math]T[/math] непротиворечива, что и доказывает неполноту в узком смысле формализованного исчисления предикатов.




Теорема компактности


Мы уже отмечали (см. теорему 15.3, б) и неоднократно использовали тот простой факт, непосредственно вытекающий из определения понятия вывода, что [math]\Phi\vdash F[/math] тогда и только тогда, когда [math]\Phi_0\vdash F[/math], где [math]\Phi_0[/math] — некоторое конечное подмножество множества [math]\Phi[/math] формул. Теорема адекватности, установленная на основании выдающейся теоремы Гёделя о существовании модели, позволяет получить из этого тривиального соображения аналогичную теорему семантического содержания, уже отнюдь не столь очевидную.


Теорема 29.16 (теорема К. Гёделя–А. И. Мальцева). Если [math]\Phi\vDash F[/math], то для некоторого конечного подмножества [math]\Phi_0\subset\Phi[/math] имеет место [math]\Phi_0\vDash F[/math].


Доказательство. Если [math]\Phi\vDash F[/math], то по теореме 29.13 (теорема адекватности) [math]\Phi\vdash F[/math]. В силу сделанного перед настоящей теоремой замечания найдется такое конечное подмножество [math]\Phi_0\subset\Phi[/math], что [math]\Phi_0\vdash F[/math]. Отсюда по теореме оправданности (следствие 29.2 из теоремы 29.1) заключаем, что [math]\Phi_0\vDash F[/math].


Следствие 29.17(локальная теорема К. Гёделя—А. И. Мальцева). Множество [math]\Sigma[/math] замкнутых формул узкого исчисления предикатов сигнатуры [math]\sigma[/math] имеет модель тогда и только тогда, когда каждое его конечное подмножество имеет модель.


Доказательство. Необходимость очевидна. Обратно, пусть каждое конечное подмножество множества [math]\Sigma[/math] имеет модель. Тогда [math]\Sigma[/math] — синтаксически непротиворечиво. (Если бы это было не так, то для некоторой формулы [math]F[/math] имелись бы выводимости [math]\Sigma\vdash F[/math] и [math]\Sigma\vdash\lnot F[/math], а значит, нашлось бы такое конечное подмножество [math]\Sigma_0\subset \Sigma[/math], что[math]\Sigma_0\vdash F[/math] и [math]\Sigma_0\vdash\lnot F[/math], то есть [math]\Sigma_0[/math] было бы синтаксически противоречиво, а значит, по теореме 29.12 не имело бы модели, что противоречило бы условию.) Следовательно, по теореме 29.10 о существовании модели множество [math]\Sigma[/math] имеет модель. Следствие доказано.


В заключение приведем еще одну теорему о формулах узкого исчисления предикатов и их моделях.


Теорема 29.18 (Лёвенгейм–Сколем). Пусть [math]\sigma[/math] — счетная сигнатура и [math]\Sigma[/math] — множество замкнутых формул узкого исчисления предикатов сигнатуры [math]\sigma[/math]. Если [math]\Sigma[/math] имеет модель, то [math]\Sigma[/math] имеет счетную модель.


Доказательство. Пусть [math]\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots \bigr\}[/math] и множество [math]\Sigma[/math] формул имеет модель. Тогда (по теореме 29.12) [math]\Sigma[/math] синтаксически непротиворечиво и модель этого множества формул может быть построена, как в доказательстве теоремы 29.10. Построенная таким образом модель будет счетной: она состоит из элементов [math]a_0,a_1,\ldots;\, c_0,c_1,\ldots[/math] и всех термов (не содержащих переменных), построенных из констант [math]a_i,\,c_j[/math]. Эти термы можно занумеровать, например, по следующему правилу:


[math]\nu(a_i)=4i+1,\quad \nu(c_i)=4i+3,\quad \nu\bigl(f_i(t_1,\ldots,t_{n_i})\bigr)= 2^{n_{n_i}+1}\cdot 3^{\nu(t_1)}\cdot 5^{\nu(t_2)}\cdot \ldots\cdot p_{n_i}^{\nu(t_{ni})},[/math]

где [math]p_0=2,\,p_1=3,\,p_2=5,\,\ldots,\,p_{n_i},\,\ldots[/math] — последовательность простых чисел.


Эта теорема может быть доказана и в более общей мощностной формулировке: если множество [math]\Sigma[/math] формул имеет бесконечную модель и мощность множества всех букв, из которых составлены формулы из [math]\Sigma[/math], равна [math]n[/math], то для любой бесконечной мощности [math]m\geqslant n[/math] существует модель множества [math]\Sigma[/math] мощности [math]m[/math].


Укажем два следствия этой теоремы:

1) если [math]\Sigma[/math]— множество формул мощности [math]n[/math], имеющее бесконечную модель, то [math]\Sigma[/math] имеет бесконечные модели любых мощностей, превышающих [math]n[/math];

2) всякое конечное множество или счетное непротиворечивое множество формул либо имеет только конечные модели, либо имеет бесконечные модели любых мощностей.


Теорема Лёвенгейма–Сколема дает ряд поразительных следствий двух типов: одни из них гласят, что некоторая теория имеет неожиданно обширные модели, другие — что теория имеет неожиданно узкие модели. Дальнейшее развитие эта мысль получит в следующей лекции.


Часовой пояс: UTC + 4 часа [ Летнее время ]


Яндекс.Метрика

Copyright © 2010-2016 MathHelpPlanet.com. All rights reserved