5. Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем (В.А. Захаров - Лекции), страница 2

т. д.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,L0 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,L0 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,L1 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4).

В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,L1 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,(R∃)L1 = {c1 , c2 }?T2 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∆, ∃xχ(x), χ(c1 ), χ(c2 ) i,L2 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,(R∃)L1 = {c1 , c2 }?T2 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∆, ∃xχ(x), χ(c1 ), χ(c2 ) i,L2 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4).

В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = h ∀xϕ(x), Γ | ∃y χ(y ), ∆ i,(L∀)?L0 = {c1 , c2 }T1 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), ∆ i,(R∃)L1 = {c1 , c2 }?T2 = h Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∆, ∃xχ(x), χ(c1 ), χ(c2 ) i,L2 = {c1 , c2 }и. т. д.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАПредположим, что указанная стратегия не приводит кпостроению успешного вывода для невыполнимой таблицыT0 = h Γ0 | ∆0 i. Тогда в дереве вывода либо существуетбесконечная ветвь, не содержащая закрытых таблицT0 −→ T1 −→ T2 −→ . . .

−→ Tn −→ Tn+1 −→ . . .либо существует ветвь, оканчивающаяся незакрытой атомарнойтаблицейT0 −→ T1 −→ T2 −→ . . . −→ Tatom −→ Tatom −→ Tatom −→ . . .Будем полагать, что в последнем случае последовательностьтаблиц также бесконечна.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАНа основе бесконечной последовательности незакрытых таблицT0 , T1 , . . . , Tn , Tn+1 , . . . , каждая из которых имеет видTn = h Γn | ∆n i построим три множества:∞S1).

Γω =Γiмножество всех формул из левых частейтаблиц,∆iмножество всех формул из правых частейтаблиц,LTiмножество всех констант из списков констант, ассоциированных с таблицами избесконечной ветви.i=02). ∆ω =∞Si=03). Lω =∞Si=0Используя множества Γω , ∆ω , Lω , построим интерпретацию Iω ,в которой будет выполняться каждая таблицапоследовательности.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАIω = hDI , Const, PrediDI = Lωпредметная область состоит из всех константных символов,входящих в состав формул из Γω и ∆ω ,Const : Const → Lωзначением c каждой константы c (как символа из алфавита)является ее собственное изображение c ( как элементмножества Lω ), т.

е. c = c,Pred : Pred → (Lω n → {true, false})для каждого предикатного символа P (n) и набора элементовci1 , . . . , cin из LωP(ci1 , . . . , cin ) = true ⇐⇒ P(ci1 , . . . , cin ) ∈ Γω .ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАПокажем, чтолюбая формула ϕ, ϕ ∈ Γω , выполнима в интерпретации Iω ,любая формула ψ, ψ ∈ ∆ω , невыполнима в интерпретации Iω .Доказательство проведем при помощи индукции по числулогических операций (связок и кванторов) в формуле.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАБазис индукцииϕ, ψ — атомарные формулы.Во всех таблицах Ti содержатся только замкнутые формулы(почему ? ).Поэтому формулы ϕ, ψ имеют вид P(ci1 , . . . , cin ).Если ϕ ∈ Γω , то P(ci1 , .

. . , cin ) = true, и поэтому Iω |= ϕ.Если ψ ∈ ∆ω , то ψ 6∈ Γω (почему ? ).Значит, P(ci1 , . . . , cin ) = false, и поэтому Iω 6|= ψ.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходПредположим, что утверждение верно для всех формул,имеющих не более n связок и кванторов. Рассмотрим формулыϕ, ψ, содержащие n + 1 связку и квантор.Если ϕ = ϕ1 → ϕ2 ∈ Γω , то есть такая таблица Ti = hΓi |∆i i,что ϕ1 → ϕ2 ∈ Γi .Согласно описанию применяемой стратегии построениятабличного вывода, существует такая таблица Tj = hΓj |∆j i,j ≥ i, что ϕ1 → ϕ2 — первая формула в списке формул Γj .Поэтому либо ϕ1 ∈ ∆j+1 , либо ϕ2 ∈ Γj+1 .В первом случае, согласно индуктивному предполжению,Iω 6|= ϕ1 , и поэтому Iω |= ϕ.Во втором случае, согласно индуктивному предполжению,Iω |= ϕ2 , и поэтому Iω |= ϕ.Итак, в обоих случаях получаем Iω |= ϕ1 → ϕ2 .ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходАналогичные рассуждения применимы и для других связок.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходЕсли ϕ = ∀xϕ1 (x) ∈ Γω , то формула ∀xϕ1 (x) бесконечно частовстречается в левых частях таблиц Ti = hΓi |∆i i (почему ? ).Поэтому правило (L∀) применяется к формуле ∀xϕ1 (x)бесконечно часто.Тогда, согласно описанию применяемой стратегии построениятабличного вывода, для любой константы c, c ∈ Lω ,существует такая таблица Tj = hΓj |∆j i, что ϕ1 (c) ∈ Γj .Значит, согласно индуктивному предполжению, Iω |= ϕ1 (c) длялюбой константы c, c ∈ Lω .Так как DI = Lω , приходим к заключению о том, чтоIω |= ∀xϕ1 (x).ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходЕсли ϕ = ∀xϕ1 (x) ∈ ∆ω , то есть такая таблица Ti = hΓi |∆i i,что ∀xϕ1 (x) ∈ ∆i .Согласно описанию применяемой стратегии построениятабличного вывода, существует такая таблица Tj = hΓj |∆j i,j ≥ i, что ∀xϕ1 (x) — первая формула в списке формул ∆j .Поэтому существует такая константа c, c ∈ Lω , чтоϕ1 (c) ∈ ∆j+1 .Согласно индуктивному предполжению, это означает, чтоIω 6|= ϕ1 (c), и поэтому Iω 6|= ∀xϕ1 (x).Аналогичные рассуждения применимы и для формул сквантором ∃.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТаким образом,любая формула ϕ, ϕ ∈ Γω , выполнима в интерпретации Iω ,любая формула ψ, ψ ∈ ∆ω , невыполнима в интерпретации Iω .Поскольку, Γ0 ⊆ Γω и ∆0 ⊆ ∆ω , приходим к заключению о том,чтоIω |= Γ0 , Iω 6|= ∆0 .Это означает, что таблица T0 выполнима в интерпретации Iωвопреки условию о невыполнимости T0 .Источник полученного противоречия — предположение оневозможности построить успешный вывод, руководствуясьописанной стратегией.

Значит, предложенная стратегияпозволяет построить успешный вывод для всякойневыполнимой таблицы.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАЭто было упрощенное доказательство теоремы полноты.А насколько существенны те упрощения, которые былиобъявлены в начале доказательства? А именно,IКакие изменения нужно внести в структуру данных,представляющих таблицы, чтобы доказательство можнобыло распространить и на таблицы, содержащиебесконечные множества формул?IКакие изменения нужно внести в стратегию построениятабличного вывода, чтобы построить успешный вывод дляневыполнимой таблицы, формулы которой содержатсложные термы?IКакие изменения нужно внести в определениеинтерпретации Iω , чтобы доказательство можно былоприменить к таблицам, содержащим незамкнутыеформулы?ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТеорема Геделя (о полноте)Если формула ϕ общезначима, то существует успешныйтабличный вывод для таблицу Tϕ = h∅|ϕi.ДоказательствоСледует из теоремы полноты.Итак, формула ϕ общезначима⇐⇒для таблицы Tϕ существует успешный вывод.И в доказательстве теоремы полноты показано, как построитьэтот вывод.ТЕОРЕМА ЛЕВЕНГЕЙМА-СКОЛЕМАТеоремаФормула ϕ выполнима ⇐⇒ ϕ имеет модель сконечной или счетно-бесконечной предметной областью.ДоказательствоЕсли ϕ выполнима, то для таблицы Tϕ∗ = hϕ|∅i нельзяпостроить успешный вывод.