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

Описание файла

Файл "LectLog4 (2)" внутри архива находится в папке "Старые лекции, в целом тоже самое". PDF-файл из архива "Старые лекции, в целом тоже самое", который расположен в категории "лекции и семинары". Всё это находится в предмете "математическая логика и логическое программирование" из седьмого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 2 страницы из PDF

. . , 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..

Свежие статьи
Популярно сейчас