Полнота ИИВ. 
Дискретный анализ. 
Формальные системы и алгоритмы

Теорема 2.26 (полнота ИИВ). Любая И-тавтология. вывод илш в ИИВ.

Доказательство теоремы 2.26 принципиально не отличается от доказательства теоремы 2.11 полноты системы ИИВ-«. Однако возникают технические трудности при доказательстве леммы 2.18 применительно к построенной выше модели Крипке (И⁷ф, ^ф). Поэтому мы модифицируем эту модель.

Замечание 2.27. Другой способ доказательства теоремы полноты состоит в том, чтобы модифицировать определение 2.12 противоречивой пары множеств формул для удобства доказательства леммы 2.18, см., например, [4].

Итак, проследим за доказательством теоремы 2.11 и обобщим его для формальной системы ИИВ. Как и раньше, фиксируем некоторую невыводимую формулу А. Определения непротиворечивой, совместной и полной нары множеств подформул формулы А остаются теми же самыми. Наша цель состоит в доказательстве совместности пары (0, {И}).

Леммы 2.16 о расширении непротиворечивой пары одной формулой и 2.17 о дополнении непротиворечивой пары до полной выполняются и для ИИВ, причём их доказательства. остаются теми же самыми.

Для доказательства совместности пары (0, {И}) мы не сможем использовать ту же самую модель Кринке (Иф, ^ф), что и раньше. Для построения искомой модели нужно ограничиться лишь норлшльными полными непротиворечивыми парами.

Определение 2.28. Непротиворечивую полную пару (Г, Д) назовём нормальной, если для любой дизъюнкции В = = С V D, В 6 Ф, из В € Г следует С? Г или D е Г.

Лемма 2.29. Пусть (Г, Д) — непротиворечивая полная пара. Тогда существует нормальная непротиворечивая полная пара (Г', Д') такая, что Г С Г'. Если при этом А € Д, то существует такая нормальная непротиворечивая полная. пара (Г', Д'), что Г С Г', А? Д'.

Замечание 2.30. В формулировке леммы А обозначает ту самую невыводимую формулу, которую мы фиксировали в начале всего рассуждения.

Доказательство леммы 2.29. Построим по ненормальной непротиворечивой полной паре (Го, До) её нормализацию (Г', Д'). Построение будет происходить по шагам.

Пусть В € Го, В = С V D, С, D € ДоДокажем, что пара (Го U {С}, {D}) непротиворечива. Действительно, если Го U {С} Ь D, то, но теореме дедукции Го Ь C^D. Но С V D, C-+D Ь D (формула (2.5) леммы 2.3) и получаем противоречивость пары (Го, До)*.

Дополняя непротиворечивую пару (Го U {С}, {/}}) до полной, получаем пару (Г], ДД.

Повторим описанные действия для пары (Г^ДД, а затем для следующей пары и т. д., пока, это возможно. Изза конечности множества формул Ф через конечное число шагов процесс остановится. Полученная в итоге пара (Г', Д') и будет искомой нормальной полной непротиворечивой парой.

Осталось доказать вторую часть леммы, которая говорит о случае A G ДоРассуждаем аналогично. Прежде всего заметим, что А не является подформулой никакой формулы из Ф, так что А ф С, А ф D. Докажем, что хотя бы одна из пар (Го U {С}, {A, D}) или (Го U {D}, {Л, С}) непротиворечива. Выводимости.

не могут выполняться одновременно. Действительно, если допустить противное, то по теореме дедукции получаем выводимости Го Ь С—>А, Го Ь D—>А. Но тогда можно вывести А из Го: к аксиоме (Р8).

добавим выводы С—>А, D—>А и применим трижды правило modus ponens (вспомним, что С V D = В € Го). Полученное противоречие доказывает, что хотя бы одна из выводимостей (2.7) не выполняется.

Пусть Го U {С} У А. Тогда пара (Го U {C},{A, D}) непротиворечива., так выше было доказано, что ГоГ1{С} У D. Дополняя пару (ToUjC}, {A.D}) до полной, получаем пару (Г 1, Ai), А <�Е Д_ь

Пусть Го U {D} У А. Тогда пара (Го U {D}, {А, С}) непротиворечива. Рассуждения аналогичны первому случаю. При доказательстве утверждения Го U {D} У С нужно применять формулу (2.6) леммы 2.3 вместо формулы (2.5).

Продолжая построение как и выше, придём к нормальной полной непротиворечивой паре (Г', Д'), причём по построению А € А'. ?

Теперь построим модифицированную модель Крипке. Шкалой (ЛГф, ^ф) этой модели будут нормальные полные непротиворечивые пары (Г, Д) множеств формул из Ф. Отношение порядка остаётся тем же самым: если Гi С Г2, то (Г1.Д1)^ф (Г2,Д‘2) — Функцию истинности для переменных зададим аналогично модели (РГф,^ф): если а; € Г, то х истинна в мире (Г.Д), в противном случае х ложна в этом мире.

Докажем лемму, аналогичную лемме 2.18.

Лемма 2.31. В любом мире (Г, Д) модели Крипке (А^гф, ^ф) все формулы из множества Г истинны, а все (формулы из множества Д — ложны.

Доказательство. Индукция по построению формулы.

База индукции доказывается в точности так же, как в лемме 2.18.

Индукционный переход. Предположим, что утверждение справедливо для формул длины меньше п, где п > 1. Рассмотрим формулу В длины п и возможные варианты её внешней связки и принадлежности множеству Г. По предположению индукции для подформул формулы В, как более коротких, утверждение леммы справедливо.

Пусть В = C—>D. В этом случае можно дословно повторить рассуждения из доказательства леммы 2.18.

Пусть В = С AD, В € Г. Так как С AD h С, С AD Ь D, формулы С и D также принадлежат Г. По предположению индукции они истинны. Значит, истинна и формула В.

Пусть В = С A D, В € А. Пусть С, D? Г. Так как С, D Ь С A D (аксиома (Р5) и два modus ponens), приходим к противоречию с непротиворечивостью пары (Г. А). Таким образом, хотя бы одна из формул С или D входит в А. По предположению индукции эта формула ложна. Значит, ложна и формула В.

Пусть В = С V D, В € Г. В этом случае мы используем условие нормальности пары (Г, А). Хотя бы одна из формул С или D входит в Г. По предположению индукции эта формула истинна. Значит, истинна и формула В.

Пусть В = С V D, В € А. Если хотя бы одна из формул С, D принадлежит Г, пара (Г, А) противоречива: С—>(CvD), ?)—>(CvD) — аксиомы (Р6) и (Р7) соответственно, добавляя к ним гипотезу С или D и применяя modus ponens, выводим формулу В = С V D. Значит, обе формулы С, D принадлежат А. По предположению индукции эти формулы ложны. Значит, ложна и формула В. ?

Чтобы завершить доказательство теоремы о полноте заметим, что, но лемме (2.31) формула А ложна в мире, соответствующем нормальной полной непротиворечивой паре, построенной применением лемм 2.17 и 2.29 из пары (0, {А}).

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

Задача 2.7. Если в ПИВ выполнено h А V В, то справедлива хотя бы одна из выводимостей Ь А или Ь В.