LectLog4 (1158000), страница 2
Текст из файла (страница 2)
Тогдасуществует интерпретация 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 |= Γ[d1 , . . . , dn ] и J 6|= ∆[d1 , . . . , dn ].Следовательно, таблица hΓ, ϕ(x){x/c}|∆i выполнима винтерпретации J.На каком этапе доказательства существенно используется тотфакт, что константа c не входит в состав формул из Γ, ∆ иформулы ϕ ?КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАТеорема корректности табличного выводаЕсли для семантической таблицы T0 существуетуспешный табличный вывод, то таблица T0невыполнима.ДоказательствоСледует изIопределения табличного вывода,Iлеммы о корректности правил табличного вывода,Iи утверждения о невыполнимости закрытых таблиц.СледствиеЕсли для таблицы Tϕ = h ∅ |ϕ i можно построить успешныйтабличный вывод, то |= ϕ.КОНЕЦ ЛЕКЦИИ 4..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
