4 - Исчисление предикатов. Построение теории P. Правила естественного вывода. Глобальные свойства теории P (Конспект лекций), страница 3

Рассмотрим формулузанную Геделем. Предварительно вспомним дополнительное правилоÔÍ-12ÌÃÒÓ47ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124. ИСЧИСЛЕНИЕ ПРЕДИКАТОВÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓЛюбопытна следующая интерпретация функциональных символов: функциональному символу f ставим в соответствие отображение, которое термы t1 , t2 , .

. . , tn преобразует в термf (t1 , t2 , . . . , tn ).Надо построить интерпретацию предикатных символов. Сформируем два множества замкнутых формул L и R, выдерживая следующее условие разделенности: для любого списка X1 ,X2 , . . . , Xn из L и любого списка Y1 , Y2 , . . . , Ym из R формула X1 ∧X2 ∧. . .∧Xn →Y1 ∨Y2 ∨. . .∨Ym невыводима в исчислении P с языком Ψ. Для этого выберем выводимую в исчислении предикатовзамкнутую формулу S (например S = C ∨ ¬C) и сформируем множество L0 из всех нелогических аксиом теории с дополнительной формулой S и множество R0 , содержащее единственнуюформулу ¬S.

В силу непротиворечивости теории множества L0 и R0 разделены. Далее строимпоследовательность пар разделенных множеств Ln , Rn , в которой каждая очередная пара естьрасширение предыдущей:Ln ⊃Ln−1 , Rn ⊃ Rn−1 . Затем объединяем две последовательностиS∞S∞множеств: L = n=1 Ln , R = n=1 Rn . Очевидно, что если все пары Ln , Rn разделены, то имножества L, R разделены.

Опишем процедуру расширения пары множеств Ln , Rn . При этомотметим, что невыводимость в исчислении P формулы X1 ∧ X2 ∧ . . . ∧ Xn → Y1 ∨ Y2 ∨ . . . ∨ Ymравносильна тому, что не существует вывода X1 , X2 , . . . , Xn ` Y1 ∨ Y2 ∨ . . . ∨ Ym . Дизъюнкциювсех формул списка ∆ будем обозначать V∆ .Выбираем произвольную формулу Z ∈ Ln \ Ln−1 . Пусть Z = U ∧ W . Для произвольной парысписков Γ ∈ Ln и ∆ ∈ Rn секвенция Γ∧Z ` V∆ невыводима.

Это значит, что для любых списковΓ и ∆ нет выводимости Γ, U, W ` V∆ , и мы можем включить формулы U и W в множество Ln+1 ,не нарушая условия разделенности. Действительно, в противном случае существуют списки Γ1 ,∆1 , для которых, например, секвенция Γ1 , U ` V∆1 явялется выводимой.

но тогда Γ1 , U, W ` V∆1и Γ1 , U ∧ W ` V∆1 , что противоречит разделенности множеств Ln и Rn .Пусть Z = U ∨ W . Невыводимость Γ, U ∨ W ` V∆ означает, что мы можем включить однуиз формул U или W в множество Ln+1 , не нарушая условия разделенности. Действительно,если для пары списков Γ1 , ∆1 есть выводимость Γ1 , U ` V∆1 а для пары списков Γ2 , ∆2 —выводимость Γ2 , W ` V∆2 , то сразу получаем выводимости Γ1 , Γ2 , U ` V∆1 ∨ V∆2 и Γ1 , Γ2 , W `V∆1 ∨ V∆2 (по правилам введения гипотез и введения дизъюнкции), откуда Γ1 , Γ2 , U ∨ W `V∆1 ∨ V∆2 , что противоречит разделенности Ln и Rn .Пусть Z = U → W .

Тогда мы, не нарушая разделенности, можем включить либо U в Rn+1 ,либо W в Ln+1 . Если бы это было не так, то существовали бы выводимости Γ1 ` V∆1 ∨ Uи Γ2 , W ` V∆2 . Значит, есть выводимость Γ1 , ¬V∆1 ` U , и мы заключаем, что существуетвыводимость Γ1 , Γ2 , ¬V∆1 , U → W ` V∆2 , из которой заключаем о существовании выводимостиΓ1 , Γ2 , U → W ` V∆1 ∨ V∆2 , а это противоречит разделенности Ln и Rn .Пусть Z = ¬U . Тогда мы можем включить U в множество Rn+1 , поскольку из существования выводимости Γ ` U ∨ V∆ следует существование выводимости Γ, ¬U ` V∆ , что противречитразделенности Ln и Rn .Пусть Z = ∀xU . В множество Ln+1 включаем все формулы Ucx , где c пробегает множествовсех констант языка.

В противном случае для некоторой константы c существует выводимостьΓ, Ucx ` V∆ , откуда с учетом ∀xU ` Ucx в силу правила сечения получаем выводимость γ, ∀xU `V∆ , противоречащую разделенности Ln и Rn .Пусть X = ∃xU . Тогда есть такая константа c, для которой добавление Ucx в Ln не нарушаетусловия разделенности с Rn . Впрочем, отметим, что если для любой константы c имеет местоΓc , Ucx ` ∆c , то в силу счетности множества констант сделать заключение о существовании выводимости Γ, ∃xU ` ∆ мы не сможем, поскольку объединение всех участвующих гипотез можетбыть счетным.

Выход из возникшей проблемы такой. Выберем константу c, не входящую нив одну из формул множеств Ln и Rn . Тогда существование выводимости Γ, Ucx ` V∆ с некоторыми списками Γ и ∆ равносильно существованию выводимости Γ, Uyx ` ∆ с произвольнойпеременной y, не входящей в формулы списка Γ (мы, не нарушая требований по всему выводуможем заменить c на y). Отсюда заключаем о существовании выводимости Γ, ∃xU ` ∆, чтопротиворечит разделенности Ln и Rn . Чтобы эта схема работала, надо гарантировать, чтоÌÃÒÓÔÍ-12ÌÃÒÓ48ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124.

ИСЧИСЛЕНИЕ ПРЕДИКАТОВÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12Замечание. Изложенное доказательство верно по сути, но, вообще-то не может быть признано строгим по некоторым соображениям. Дело в том, что в доказательстве идет манипуляция бесконечными множествами, причем на содержательном уровне. Такого рода рассужденияв современной математической логике не считаются достаточно надежными. Однако следуетучесть, что все множества, рассматриваемые в доказательстве, являются счетными. Поэтому построение множеств L и R, обладающих свойством замкнутости (в определенном смысле)ÔÍ-12ÌÃÒÓна любом шаге будет существовать свободная константа c.

Для этого надо скорректироватьдействия при анализе формулы вида Z = ∀xU . При обработке такой формулы надо включатьв Ln+1 не все формулы Ucx , а хотя бы одну с нерассмотренной еще константой c, но обеспечитьбесконечное количество обработок этой формулы: если в других случаях обработанная формула больше не рассматривается, то эту надо периодически просматривать, генерируя очередныеформулы вида Ucx .

Сделать это можно, поскольку и количество формул в рассматриваемомязыке, и количество констант счетно.Рассмотрим теперь формулу Z ∈ Rn . Если Z = U ∧W , то в множество Rn+1 можно включитьодну из формул U или W , не нарушая условия разделенности. Действительно, если существуютвыводимости Γ1 ` V∆1 ∨U и Γ2 ` V∆2 ∨W , то существуют выводимости Γ2 , ¬V∆1 ` U и Γ2 , ¬V∆2 `W , откуда с помощью введения гипотез и введения конъюнкции получаем Γ1 , Γ2 , ¬V∆1 , ¬V∆2 `U ∧ W и Γ1 , Γ2 ` V∆1 ∨ V∆2 ∨ (U ∧ W ), что противоречит разделенности Ln и Rn .Если Z = U ∨W , то в Rn+1 включаем и U , и W . Например, если есть выводимость Γ ` V∆ ∨U ,то сразу Γ ` V∆ ∨ U ∨ W , а порядок дизъюнкций справа не играет роли.Пусть Z = U → W .

Тогда включаем U в Ln+1 , а W в Rn+1 . Действительно, если существуетвыводимость Γ, U ` V∆ , то Γ, U ` V∆ ∨ W , откуда Γ, ¬V∆ , U ` W и в силу теоремы о дедукцииΓ, ¬V∆ ` U → W . Следовательно, Γ, ¬V∆ ` V∆ ∨ (U → W ), что противоречит разделенностиLn и R n .Если Z = ¬U , формулу U включаем в Ln+1 : из выводимости Γ, U ` V∆ следует выводимостьΓ ` V∆ ∨ ¬U , которая противоречит разделенности Ln и Rn .Пусть Z = ∀xU . Выбрав константу c, не входящую ни в одну из формул множеств Ln иRn , заключаем, что нет выводимости Γ ` V∆ ∨ Ucx . Действительно, из существования такойвыводимости с некоторыми списками Γ и ∆ следует выводимость Γ ` V∆ ∨ Uyx , где переменнаяy не входит в формулы списков Γ и ∆, а из последней — выводимость Γ ` V∆ ∨ ∀xU , противоречащая условию разделенности Ln и Rn .

Для выбранной константы в список Rn+1 включаемформулу Ucx .Если Z = ∃xU , то в Rn+1 включаем формулы Ucx для всех констант c, обеспечив их посте”пенное поступление“, как в случае формулы Z = ∀xU из множества Ln .Построив последовательности разделенных множеств {Ln } и {Rn }, переходим к их объединениям L и R. Эти объединения тоже разделены: если бы существовала выводимость Γ ` V∆с некоторыми списками Γ и ∆, то в силу конечности списков можно было бы утверждать, чтоΓ ⊂ Lk и ∆ ⊂ Rk для некоторого номера k и что множества Lk и Rk не являются разделенными.Элементарным формулам множества L присвоим истинностное значение 1, элементарнымформулам множества R — истинностное значение 0, остальным — неважно.

Тогда можноутверждать, что все формулы множества L будут иметь истинностное значение 1, а все формулы множества R — истинностное значение 0. Доказательство этого проводится индукциейпо построению формул. Действительно, для элементарных формул это вытекает из заданнойинтепретации. Пусть Z ∈ L имеет, например, вид Z = U → W . Тогда в соответствии спостроением множеств L и R имеем либо U ∈ R, либо W ∈ L.

В первом случае, согласно индуктивному предположению, формула U ложна, а значит, формула U → W истинна. Во второмслучае формула W истинна, поэтому U → W истинна. Если Z = U → W ∈ R, то по построениюU ∈ L, W ∈ R. Значит, U истинна, а W ложна, откуда заключаем, что Z ложна. Аналогичнорассматриваются остальные случаи.Поскольку множество L содержит все нелогические аксиомы, заключаем, что они в построенной интерпретации истинны, а интерпретация является моделью.

IÌÃÒÓÔÍ-12ÌÃÒÓ49ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124. ИСЧИСЛЕНИЕ ПРЕДИКАТОВÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ50можно провести так, что на каждом шаге мы будем иметь дело с конечными множествами.Требуется аккуратная работа с нумерациями счетных множеств, но эти детали затушевываютосновную идею доказательства.Доказанная теорема позволяет сделать вывод о полноте исчисления предикатов в широкомсмысле.ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-124.

ИСЧИСЛЕНИЕ ПРЕДИКАТОВÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12Пример 4.3. Рассмотрим формулу ∃x(p→q(x))→(p→∀xq(x)). Попробуем построить контрпример, т.е. интерпретацию, в которой она ложна, или убедиться в ее истинности. Редукциюформулы удобно построить в виде дерева, в котором преобразуется формула вида Γ > ∆, где Γ и∆ — конечные списки формул.

Слева — формулы множества L, справа — формулы множестваÌÃÒÓИсчисление предикатов не является разрешимой теорией. Это становится понятно, если учесть, что средств исчисления предикатов достаточно, чтобы представить содержаниепрактически любой математической теории. Было бы странно предполагать, что есть некийформальный алгоритм, по которому можно любую теорему проверить, верна она или нет. Это,разумеется, расходится с нашим представлением о бесконечном разнообразии окружающего мира. Однако строгое доказательство этого факта выходит за рамки курса: требуется строгоематематическое описание понятия алгоритм“ и развитая теория об алгоритмах, чтобы можно”было строго показать неразрешимость исчисленния предикатов.Но здесь важно одно обстоятельство. Доказанная теорема устанавливает эквивалентностьпонятий выводимая“ и истинная“.