Ещё одни лекции В.А. Захарова (1158033), страница 7
Текст из файла (страница 7)
В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = ∀xϕ(x), Γ | ∃y χ(y ), Δ ,(L∀)?L0 = {c1 , c2 }T1 = Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), Δ ,L1 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = ∀xϕ(x), Γ | ∃y χ(y ), Δ ,(L∀)?L0 = {c1 , c2 }T1 = Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), Δ ,L1 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = ∀xϕ(x), Γ | ∃y χ(y ), Δ ,(L∀)?L0 = {c1 , c2 }T1 = Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), Δ ,(R∃)L1 = {c1 , c2 }?T2 = Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | Δ, ∃xχ(x), χ(c1 ), χ(c2 ) ,L2 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4).
В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = ∀xϕ(x), Γ | ∃y χ(y ), Δ ,(L∀)?L0 = {c1 , c2 }T1 = Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), Δ ,(R∃)L1 = {c1 , c2 }?T2 = Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | Δ, ∃xχ(x), χ(c1 ), χ(c2 ) ,L2 = {c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА4). В случае применения к таблице T правил (L∀) и (R∃) вкачестве подстановочных термов используются всеконстанты из списка LT .T0 = ∀xϕ(x), Γ | ∃y χ(y ), Δ ,(L∀)?L0 = {c1 , c2 }T1 = Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | ∃y χ(y ), Δ ,(R∃)L1 = {c1 , c2 }?T2 = Γ, ∀xϕ(x), ϕ(c1 ), ϕ(c2 ) | Δ, ∃xχ(x), χ(c1 ), χ(c2 ) ,L2 = {c1 , c2 }и.
т. д.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАПредположим, что указанная стратегия не приводит кпостроению успешного вывода для невыполнимой таблицыT0 = Γ0 | Δ0 . Тогда в дереве вывода либо существуетбесконечная ветвь, не содержащая закрытых таблицT0 −→ T1 −→ T2 −→ . . . −→ Tn −→ Tn+1 −→ . . .либо существует ветвь, оканчивающаяся незакрытой атомарнойтаблицейT0 −→ T1 −→ T2 −→ . . . −→ Tatom −→ Tatom −→ Tatom −→ .
. .Будем полагать, что в последнем случае последовательностьтаблиц также бесконечна.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАНа основе бесконечной последовательности незакрытых таблицT0 , T1 , . . . , Tn , Tn+1 , . . . , каждая из которых имеет видTn = Γn | Δn построим три множества:1). Γω =∞2). Δω =3). Lω =Γiмножество всех формул из левых частейтаблиц,Δiмножество всех формул из правых частейтаблиц,LTiмножество всех констант из списков констант, ассоциированных с таблицами избесконечной ветви.i=0∞i=0∞i=0Используя множества Γω , Δω , Lω , построим интерпретацию Iω ,в которой будет выполняться каждая таблицапоследовательности.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАIω = DI , Const, PredDI = 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ω |= ϕ.Если ψ ∈ Δω , то ψ ∈ Γω (почему ? ).Значит, P(ci1 , . . . , cin ) = false, и поэтому Iω |= ψ.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходПредположим, что утверждение верно для всех формул,имеющих не более n связок и кванторов. Рассмотрим формулыϕ, ψ, содержащие n + 1 связку и квантор.Если ϕ = ϕ1 → ϕ2 ∈ Γω , то есть такая таблица Ti = Γi |Δi ,что ϕ1 → ϕ2 ∈ Γi .Согласно описанию применяемой стратегии построениятабличного вывода, существует такая таблица Tj = Γj |Δj ,j ≥ i, что ϕ1 → ϕ2 — первая формула в списке формул Γj .Поэтому либо ϕ1 ∈ Δj+1 , либо ϕ2 ∈ Γj+1 .В первом случае, согласно индуктивному предполжению,Iω |= ϕ1 , и поэтому Iω |= ϕ.Во втором случае, согласно индуктивному предполжению,Iω |= ϕ2 , и поэтому Iω |= ϕ.Итак, в обоих случаях получаем Iω |= ϕ1 → ϕ2 .ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходАналогичные рассуждения применимы и для других связок.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходЕсли ϕ = ∀xϕ1 (x) ∈ Γω , то формула ∀xϕ1 (x) бесконечно частовстречается в левых частях таблиц Ti = Γi |Δi (почему ? ).Поэтому правило (L∀) применяется к формуле ∀xϕ1 (x)бесконечно часто.Тогда, согласно описанию применяемой стратегии построениятабличного вывода, для любой константы c, c ∈ Lω ,существует такая таблица Tj = Γj |Δj , что ϕ1 (c) ∈ Γj .Значит, согласно индуктивному предполжению, Iω |= ϕ1 (c) длялюбой константы c, c ∈ Lω .Так как DI = Lω , приходим к заключению о том, чтоIω |= ∀xϕ1 (x).ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходЕсли ϕ = ∀xϕ1 (x) ∈ Δω , то есть такая таблица Ti = Γi |Δi ,что ∀xϕ1 (x) ∈ Δi .Согласно описанию применяемой стратегии построениятабличного вывода, существует такая таблица Tj = Γj |Δj ,j ≥ i, что ∀xϕ1 (x) — первая формула в списке формул Δj .Поэтому существует такая константа c, c ∈ Lω , чтоϕ1 (c) ∈ Δj+1 .Согласно индуктивному предполжению, это означает, чтоIω |= ϕ1 (c), и поэтому Iω |= ∀xϕ1 (x).Аналогичные рассуждения применимы и для формул сквантором ∃.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТаким образом,любая формула ϕ, ϕ ∈ Γω , выполнима в интерпретации Iω ,любая формула ψ, ψ ∈ Δω , невыполнима в интерпретации Iω .Поскольку, Γ0 ⊆ Γω и Δ0 ⊆ Δω , приходим к заключению о том,чтоIω |= Γ0 , Iω |= Δ0 .Это означает, что таблица T0 выполнима в интерпретации Iωвопреки условию о невыполнимости T0 .Источник полученного противоречия — предположение оневозможности построить успешный вывод, руководствуясьописанной стратегией.
Значит, предложенная стратегияпозволяет построить успешный вывод для всякойневыполнимой таблицы.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАЭто было упрощенное доказательство теоремы полноты.А насколько существенны те упрощения, которые былиобъявлены в начале доказательства? А именно,Какие изменения нужно внести в структуру данных,представляющих таблицы, чтобы доказательство можнобыло распространить и на таблицы, содержащиебесконечные множества формул?Какие изменения нужно внести в стратегию построениятабличного вывода, чтобы построить успешный вывод дляневыполнимой таблицы, формулы которой содержатсложные термы?Какие изменения нужно внести в определениеинтерпретации Iω , чтобы доказательство можно былоприменить к таблицам, содержащим незамкнутыеформулы?ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТеорема Геделя (о полноте)Если формула ϕ общезначима, то существует успешныйтабличный вывод для таблицу Tϕ = ∅|ϕ.ДоказательствоСледует из теоремы полноты.Итак, формула ϕ общезначима⇐⇒для таблицы Tϕ существует успешный вывод.И в доказательстве теоремы полноты показано, как построитьэтот вывод.ТЕОРЕМА ЛЕВЕНГЕЙМА-СКОЛЕМАТеоремаФормула ϕ выполнима ⇐⇒ ϕ имеет модель сконечной или счетно-бесконечной предметной областью.ДоказательствоЕсли ϕ выполнима, то для таблицы Tϕ∗ = ϕ|∅ нельзяпостроить успешный вывод.
Применим стратегию издоказательства теоремы полноты. Т. к. Tϕ∗ выполнима,получим дерево с ветвью, в которой нет закрытых таблиц.Tϕ∗ = T0 −→ T1 −→ T2 −→ . . . −→ Tn −→ Tn+1 −→ . . .Для этой ветви построим интерпретацию Iω , в которойDi = Lω = {c1 , c2 , . . . } — конечное или счетно-бесконечноемножество констант из таблиц последовательности;выполнимы все таблицы Ti (в т.ч. и Tϕ∗ ).ТЕОРЕМА КОМПАКТНОСТИ МАЛЬЦЕВАТеоремаΓ |= ϕ ⇐⇒существует такое конечное подмножество Γ , Γ ⊆ Γ, что Γ |= ϕ.Доказательство1.
Γ |= ϕ ⇐⇒ таблица T = Γ|ϕ невыполнима (почему? )2. Таблица T = Γ|ϕ невыполнима ⇐⇒ cуществуетуспешный вывод для T (почему? )3. успешный вывод — это конечное дерево, и поэтомусуществует лишь конечое множество формул Γ , Γ ⊆ Γ,к которым применяются правила вывода.4. Но тогда для таблицы T = Γ |ϕ cуществует точно такойже успешный вывод.5.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
