LectLog4 (2) (Старые лекции, в целом тоже самое), страница 2

. . , dn i значенийсвободных переменных, для которых I |= Γ[d̄],I 6|= ∆[d̄],I |= (ϕ → ψ)[d̄]Рассмотрим правилоL →:КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ϕ → ψ|∆i.hΓ, ψ|∆i, hΓ|ϕ, ∆iТаблица hΓ, ϕ → ψ|∆i выполнима ⇐⇒существует интерпретация I и набор d̄ = hd1 , . . . , dn i значенийсвободных переменных, для которых I |= Γ[d̄], I |= Γ[d̄],⇐⇒I 6|= ∆[d̄],I 6|= ∆[d̄],I |= ψ[d̄] или I 6|= ϕ[d̄]I |= (ϕ → ψ)[d̄]Рассмотрим правилоL →:КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ϕ → ψ|∆i.hΓ, ψ|∆i, hΓ|ϕ, ∆iТаблица hΓ, ϕ → ψ|∆i выполнима ⇐⇒существует интерпретация I и набор d̄ = hd1 , . . .

, dn i значенийсвободных переменных, для которых I |= Γ[d̄], I |= Γ[d̄],⇐⇒⇐⇒I 6|= ∆[d̄],I 6|= ∆[d̄],I |= ψ[d̄] или I 6|= ϕ[d̄]I |= (ϕ → ψ)[d̄]Рассмотрим правило⇐⇒ I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄]L →: I |= Γ[d̄],илиI 6|= ∆[d̄],I 6|= ϕ[d̄]КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ϕ → ψ|∆i.hΓ, ψ|∆i, hΓ|ϕ, ∆iТаблица hΓ, ϕ → ψ|∆i выполнима ⇐⇒существует интерпретация I и набор d̄ = hd1 , . . . , dn i значенийсвободных переменных, для которых I |= Γ[d̄], I |= Γ[d̄],⇐⇒⇐⇒I 6|= ∆[d̄],I 6|= ∆[d̄],I |= ψ[d̄] или I 6|= ϕ[d̄]I |= (ϕ → ψ)[d̄]Рассмотрим правило⇐⇒ I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄]L →: I |= Γ[d̄],илиI 6|= ∆[d̄],I 6|= ϕ[d̄]⇐⇒одна из таблиц T1 = hΓ, ψ|∆i или T2 = hΓ|ϕ, ∆i выполнима.КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыАналогично доказывается корректность остальных 7 правилдля логических связокКОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыРассмотрим правилоL∀:hΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iКОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒Рассмотрим правилоL∀:КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒ существуетинтерпретация I и набор d1 , .

. . , dn значений свободныхпеременных, для которых I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . . . , dn ],I |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоL∀:КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒ существуетинтерпретация I и набор d1 , . . . , dn значений свободныхпеременных, для которых I |= Γ[d1 , .

. . , dn ],I 6|= ∆[d1 , . . . , dn ],Пусть d0 = t[d1 , . . . , dn ]. ТогдаI |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоI |= (∀x0 ϕ)[d1 , . . . , dn ]L∀:КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒ существуетинтерпретация I и набор d1 , .

. . , dn значений свободныхпеременных, для которых I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . . . , dn ],Пусть d0 = t[d1 , . . . , dn ]. ТогдаI |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоL∀:I |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ]КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒ существуетинтерпретация I и набор d1 , . . . , dn значений свободныхпеременных, для которых I |= Γ[d1 , .

. . , dn ],I 6|= ∆[d1 , . . . , dn ],Пусть d0 = t[d1 , . . . , dn ]. ТогдаI |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоL∀:I |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ] ⇒⇒ I |= ϕ[t[d1 , . . . , dn ], d1 , . . . , dn ]КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒ существуетинтерпретация I и набор d1 , . . . , dn значений свободныхпеременных, для которых I |= Γ[d1 , .

. . , dn ],I 6|= ∆[d1 , . . . , dn ],Пусть d0 = t[d1 , . . . , dn ]. ТогдаI |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоL∀:I |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ] ⇒⇒ I |= ϕ[t[d1 , . . . , dn ], d1 , . . . , dn ] ⇒ I |= ϕ{x0 /t}[d1 , . . . , dn ].КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒ существуетинтерпретация I и набор d1 , . . . , dn значений свободныхпеременных, для которых I |= Γ[d1 , . .

. , dn ],I 6|= ∆[d1 , . . . , dn ],Пусть d0 = t[d1 , . . . , dn ]. ТогдаI |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоL∀:I |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ] ⇒⇒ I |= ϕ[t[d1 , . . . , dn ], d1 , . . . , dn ] ⇒ I |= ϕ{x0 /t}[d1 , . . . , dn ].Следовательно, таблица hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iвыполнима в интерпретации IКОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒ существуетинтерпретация I и набор d1 , . . . , dn значений свободныхпеременных, для которых I |= Γ[d1 , . .

. , dn ],I 6|= ∆[d1 , . . . , dn ],Пусть d0 = t[d1 , . . . , dn ]. ТогдаI |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоL∀:I |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ] ⇒⇒ I |= ϕ[t[d1 , . . . , dn ], d1 , . . . , dn ] ⇒ I |= ϕ{x0 /t}[d1 , . . . , dn ].Следовательно, таблица hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iвыполнима в интерпретации IНа каком этапе доказательства существенно используется тотфакт, что переменная x0 свободна для терма t в формуле ϕ ?КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыРассмотрим правилоL∃:hΓ, ∃xϕ(x)|∆i.hΓ, ϕ(x){x/c}|∆iКОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∃xϕ(x)|∆i.hΓ, ϕ(x){x/c}|∆iОчевидно, что выполнимость таблицы hΓ, ϕ(x){x/c}|∆i влечетвыполнимость таблицы hΓ, ∃xϕ(x)|∆iРассмотрим правилоL∃:КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∃xϕ(x)|∆i.hΓ, ϕ(x){x/c}|∆iОчевидно, что выполнимость таблицы hΓ, ϕ(x){x/c}|∆i влечетвыполнимость таблицы hΓ, ∃xϕ(x)|∆iРассмотрим правилоL∃:Допустим, что выполнима таблица hΓ, ∃xϕ(x)|∆i.

Тогдасуществует интерпретация I и набор d1 , . . . , dn значенийсвободных переменных, для которых I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . . . , dn ],I |= (∃xϕ)[d1 , . . . , dn ]КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∃xϕ(x)|∆i.hΓ, ϕ(x){x/c}|∆iОчевидно, что выполнимость таблицы hΓ, ϕ(x){x/c}|∆i влечетвыполнимость таблицы hΓ, ∃xϕ(x)|∆iРассмотрим правилоL∃:Допустим, что выполнима таблица hΓ, ∃xϕ(x)|∆i. Тогдасуществует интерпретация I и набор d1 , .

. . , dn значенийсвободных переменных, для которых I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . . . , dn ],I |= (∃xϕ)[d1 , . . . , dn ]Выполнимость ∃xϕ[d1 , . . . , dn ] означает, что существует такойэлемент d0 ∈ DI , что I |= ϕ[d0 , d1 , . . . , dn ].КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыРассмотрим интерпретацию J, которая отличается от I , толькотем, что в J константа c имеет другое значение, а именноc̄ = d0 .Тогда J |= (ϕ{x/c})[d1 , .

. . , dn ].КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыРассмотрим интерпретацию J, которая отличается от I , толькотем, что в J константа c имеет другое значение, а именноc̄ = d0 .Тогда J |= (ϕ{x/c})[d1 , . . . , dn ].Кроме того, J |= Γ[d1 , . . . , dn ] и J 6|= ∆[d1 , . . . , dn ]. Почему?КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыРассмотрим интерпретацию J, которая отличается от I , толькотем, что в J константа c имеет другое значение, а именноc̄ = d0 .Тогда J |= (ϕ{x/c})[d1 , .

. . , dn ].Кроме того, J |= Γ[d1 , . . . , dn ] и J 6|= ∆[d1 , . . . , dn ]. Почему?Следовательно, таблица hΓ, ϕ(x){x/c}|∆i выполнима винтерпретации J.КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыРассмотрим интерпретацию J, которая отличается от I , толькотем, что в J константа c имеет другое значение, а именноc̄ = d0 .Тогда J |= (ϕ{x/c})[d1 , . . . , dn ].Кроме того, J |= Γ[d1 , . . . , dn ] и J 6|= ∆[d1 , . . . , dn ]. Почему?Следовательно, таблица hΓ, ϕ(x){x/c}|∆i выполнима винтерпретации J.На каком этапе доказательства существенно используется тотфакт, что константа c не входит в состав формул из Γ, ∆ иформулы ϕ ?КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАТеорема корректности табличного выводаЕсли для семантической таблицы T0 существуетуспешный табличный вывод, то таблица T0невыполнима.КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАТеорема корректности табличного выводаЕсли для семантической таблицы T0 существуетуспешный табличный вывод, то таблица T0невыполнима.ДоказательствоСледует изIопределения табличного вывода,Iлеммы о корректности правил табличного вывода,Iи утверждения о невыполнимости закрытых таблиц.КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАТеорема корректности табличного выводаЕсли для семантической таблицы T0 существуетуспешный табличный вывод, то таблица T0невыполнима.ДоказательствоСледует изIопределения табличного вывода,Iлеммы о корректности правил табличного вывода,Iи утверждения о невыполнимости закрытых таблиц.СледствиеЕсли для таблицы Tϕ = h ∅ |ϕ i можно построить успешныйтабличный вывод, то |= ϕ.КОНЕЦ ЛЕКЦИИ 4..