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