4. Подстановки. Метод семантических таблиц в логике предикатов, корректность табличного вывода (1131913)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Математическая логикаЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2017, весенний семестрЛекция 4ПодстановкиМетод семантических таблицв логике предикатовКорректность табличного выводаПроблема общезначимости формуллогики предикатовформулируется так:для заданной формулы ϕлогики предикатовпроверить её общезначимость:|= ϕ ?Проблема общезначимости формуллогики предикатовС каких сторон можно исследовать эту проблему?IIIIIIкак общезначимость связана с выполнимостью иневыполнимостью?насколько проверкаобщезначимости/выполнимости/невыполнимостизатрудняется наличием свободных переменных?как адаптировать метод семантических таблиц логикивысказываний к логике предикатов?насколько (теоретически) трудно проверитьобщезначимость формулы?как можно “практически разумно” обобщить задачу SAT налогику предикатов?...Проблема общезначимости формуллогики предикатовС каких сторон можно исследовать эту проблему?IIIкак общезначимость связана с выполнимостью иневыполнимостью?насколько проверкаобщезначимости/выполнимости/невыполнимостизатрудняется наличием свободных переменных?как адаптировать метод семантических таблиц логикивысказываний к логике предикатов?Проблема общезначимости формуллогики предикатовформула ϕ(exn ) общезначимаϕ(exn ) = ¬ψ(exn )ψ(exn ) = ¬ϕ(exn )формула ψ(exn ) невыполнимаϕ=ψпротивоположныйответформула ϕ(exn ) выполнимаψ = ∀exn ϕ(exn )предложение ψ общезначимоϕ = ∃exn ψ(exn )предложение ϕ невыполнимоψ = ∃exn ϕ(exn )предложение ψ выполнимо∀exn — сокращение для ∀x1 .

. . ∀xn∃exn — сокращение для ∃x1 . . . ∃xnПроблема общезначимости формуллогики предикатовУтверждениеформула ϕ(exn ) общезначимаϕ(exn ) = ¬ψ(exn )ψ(exn ) = ¬ϕ(exn )ψ = ∀exn ϕ(exn )предложение ψ общезначимоформула ψ(exn ) невыполнимаϕ=ψпротивоположныйответϕ = ∃exn ψ(exn )предложение ϕ невыполнимоформула ϕ(exn ) выполнимаψ = ∃exn ϕ(exn )предложение ψ выполнимоДоказательство.Самостоятельно (это просто)Проблема общезначимости формуллогики предикатовА как проверить общезначимость формулы?Подход “в лоб” — перебрать все интерпретацииКак задать бесконечную интерпретацию и проверить истинностьформулы в ней?Можно ли ограничиться только конечными интерпретациями?УтверждениеСуществует необщезначимое предложение, истинное влюбой интерпретации с конечной предметной областьюПроблема общезначимости формуллогики предикатовУтверждениеСуществует необщезначимое предложение, истинное влюбой интерпретации с конечной предметной областьюДоказательство.

Вот пример такого предложения ϕ:∀x ¬R(x, x) & ∀x ∀y ∀z (R(x, y) & R(y, z) → R(x, z)) →∃x ∀y ¬R(x, y)Проблема общезначимости формуллогики предикатовУтверждениеСуществует необщезначимое предложение, истинное влюбой интерпретации с конечной предметной областьюДоказательство. Вот пример такого предложения ϕ:∀x ¬R(x, x) & ∀x ∀y ∀z (R(x, y) & R(y, z) → R(x, z)) →∃x ∀y ¬R(x, y)Формула ϕ необщезначима:Предметная область: натуральные числаR(x, y) = “x < y”Посылки ϕ: никакое число не может быть меньше себяесли x < y и y < z то x < zВывод ϕ: существует максимальное натуральное числоПосылки верны, но вывод неверенПроблема общезначимости формуллогики предикатовУтверждениеСуществует необщезначимое предложение, истинное влюбой интерпретации с конечной предметной областьюДоказательство.

Вот пример такого предложения ϕ:∀x ¬R(x, x) & ∀x ∀y ∀z (R(x, y) & R(y, z) → R(x, z)) →∃x ∀y ¬R(x, y)А что если предметная область конечна? Например:Предметная область: все сотрудники компании NR(x, y) = “игрек является начальником икса”Посылки ϕ: никто собой не командуетначальник начальника — тоже начальникВывод ϕ: есть тот, кому никто не указИ посылки, и вывод верныПроблема общезначимости формуллогики предикатовУтверждениеСуществует необщезначимое предложение, истинное влюбой интерпретации с конечной предметной областьюДоказательство. Вот пример такого предложения ϕ:∀x ¬R(x, x) & ∀x ∀y ∀z (R(x, y) & R(y, z) → R(x, z)) →∃x ∀y ¬R(x, y)А что если предметная область конечна? Общее истолкование:“Если бинарное отношение R антирефлексивно и транзитивно,то существует элемент, максимальный относительно R”Проблема общезначимости формуллогики предикатовУтверждениеСуществует необщезначимое предложение, истинное влюбой интерпретации с конечной предметной областьюДоказательство.

Вот пример такого предложения ϕ:∀x ¬R(x, x) & ∀x ∀y ∀z (R(x, y) & R(y, z) → R(x, z)) →∃x ∀y ¬R(x, y)А что если предметная область конечна? Общее истолкование:“Если R — отношение строгого частичного порядка,то существует элемент, максимальный относительно R”Любое конечное частично упорядоченное множествосодержит максимальный элемент(это частный случай леммы Цорна)HМетод семантических таблицИтог: никак нельзя решить проблему “|= ϕ?” явным переборомвсех интерпретаций с проверкой истинности ϕ в каждой из нихМожно попытаться решить эту проблему с помощьюметода семантических таблиц:IIIIрассуждая “от противного”, пытаемся построитьконтрмодель I: I 6|= ϕоперируем семантическими таблицами: предположениями отом, что выполняется и не выполняется в Iэти предположения структурируем в виде дерева вывода,строящегося по правилам табличного выводаT0T1 , (T2 )если все предположения явно опровергнуты закрытымитаблицами, то формула общезначимаМетод семантических таблицСемантическая таблица (логики предикатов) — это парамножеств формул: T = h Γ | ∆ i.

. . |= Φ . . . (. . . 6|= Φ . . . ) — сокращение для“для любой формулы ϕ из Φ верно (неверно) . . . |= ϕ . . . ”(Φ — множество формул)nПусть ex — все свободные переменные формул из Γ ∪ ∆Таблица T выполнима, если существуют интерпретация I инабор предметов den из области интерпретации,такие что I |= Γ[den ] и I 6|= ∆[den ]закрыта, если Γ ∩ ∆ = ∅атомарна, если содержит только атомыПримерСледующая семантическая таблица выполнима:h ∃x P(x), ¬P(y) | ∀x P(x), P(x) & ¬P(x) i(подтверждается интерпретацией: {d1 , d2 }, P(d1 ) = t, P(d2 ) = fи набором d1 , d2 значений свободных переменных x, y)Метод семантических таблицТеорема о табличной проверке общезначимости|= ϕ⇔таблица h | ϕ i невыполнимаДоказательство.|= ϕ(exn )⇔n enI |= ϕ(ex )[d ] для любой интерпретации Iи любого набора предметов den⇔таблица h | ϕ i невыполнима HУтверждениеЛюбая закрытая таблица невыполнимаУтверждениеЛюбая незакрытая атомарная таблица выполнимаДоказательство.

Самостоятельно (очевидно? )Метод семантических таблицА если формула начинается с квантора, то как из неё получитьявное противоречие?Пример: |= ∀x P(x) → P(c) ?h | ∀x P(x) → P(c) iизбавляемся от импликацииh ∀x P(x) | P(c) i?подставляем константу c на место xh ∀x P(x), P(c) | P(c) iСтрого определим, что такое “подставляем”ПодстановкиПодстановка — это отображение θ : Var → TermОбласть подстановки θ: Domθ = {x | x ∈ Var, θ(x) 6= x}Подстановка конечна, если её область конечнаSubst — множество всех конечных подстановок{x1 /t1 , .

. . , xn /tn } — это конечная подстановка θ, для которойверно:IIDomθ = {x1 , . . . , xn }θ(xi ) = ti(1 ≤ i ≤ n)Пара xi /ti — это связкаε — это тождественная (пустая) подстановка: Domθ = ∅ПодстановкиПусть E — логическое выражение (терм или формула) и θ —подстановка.Результат E θ применения подстановки θ к E определяется так:xθ = θ(x)cθ = cf(t1 , .

. . , tn )θ = f(t1 θ, . . . , tn θ)P(t1 , . . . , tn )θ = P(t1 θ, . . . , tn θ)(ϕ & ψ)θ = (ϕθ & ψθ)(ϕ ∨ ψ)θ = (ϕθ ∨ ψθ)(ϕ → ψ)θ = (ϕθ → ψθ)(¬ϕ)θ = (¬ϕθ)(∀x ϕ)θ = (∀x ϕθ0 )(∃x ϕ)θ = (∃x ϕθ0 )(x ∈ Var)(c ∈ Const)(f ∈ Func, t1 , . . . , tn ∈ Term)(P ∈ Pred)(ϕ, ψ ∈ Form)(θ0 (x) = x;θ0 (y) = θ(y) для y 6= x)ПодстановкиПример применения подстановкиϕ: ∀x (P(x) → ¬R(y)) → R(f(x)) ∨ ∃y P(y) ∨ R(u)θ: {x/g(x, c), y/x, z/f(z)}Выделяются все свободные вхождения переменных в ϕϕ: ∀x (P(x) → ¬R(y)) → R(f(x)) ∨ ∃y P(y) ∨ R(u)К этим вхождениям применяется θϕθ: ∀x (P(x) → ¬R(x)) → R(f(g(x, c))) ∨ ∃y P(y) ∨ R(u)ПодстановкиПри применении подстановок для выявления “частных случаев”следует соблюдать осторожностьНапример:ϕ(x): ∀x ∃y P(x, y) → ∃y P(x, y)“если у каждого есть дед, то у x тоже есть дед”Очевидно, что |= ϕ(x)Применим к ϕ подстановку θ = {x/y}ϕ(x)θ: ∀x ∃y P(x, y) → ∃y P(y, y)“если у каждого есть дед, то есть и тот, кто сам себе дед”Очевидно, что 6|= ϕ(x)θПочему смысл формулы после применения подстановки такисказился?ПодстановкиПеременная x свободна для терма t в формуле ϕ, если ни односвободное вхождение переменной x не лежит в области действияквантора, связывающего переменную из множества VartПодстановка θ = {x1 /t1 , .

. . , xn /tn } — правильная для формулыϕ, если для каждой связки xi /ti переменная xi свободна длятерма ti в формуле ϕНапример, подстановка {x/y} не является правильной дляформулы∀x ∃y P(x, y) → ∃y P(x, y)а подстановка {x/f(u, v)} — правильная для этой формулыМетод семантических таблицПравила табличного вывода:правила для логических связок такие же,как в логике высказываний:L&h Γ, ϕ & ψ | ∆ ih Γ, ϕ, ψ | ∆ iR&h Γ | ∆, ϕ & ψ ih Γ | ∆, ϕ i, h Γ | ∆, ψ iL∨h Γ, ϕ ∨ ψ | ∆ ih Γ, ϕ | ∆ i, h Γ, ψ | ∆ iR∨h Γ | ∆, ϕ ∨ ψ ih Γ | ∆, ϕ, ψ iL→h Γ, ϕ → ψ | ∆ ih Γ, ψ | ∆ i, h Γ | ∆, ϕ iR→h Γ | ∆, ϕ → ψ ih Γ, ϕ | ∆, ψ iL¬h Γ, ¬ϕ | ∆ ih Γ | ∆, ϕ iR¬h Γ | ∆, ¬ϕ ih Γ, ϕ | ∆ iМетод семантических таблицПравила табличного вывода:L∀h Γ, ∀x ϕ | ∆ ih Γ, ∀x ϕ, ϕ {x/t} | ∆ iR∃h Γ | ∆, ∃x ϕ ih Γ | ∆, ∃x ϕ, ϕ {x/t} iДополнительное ограничение:переменная x свободна для терма t в формуле ϕL∃h Γ, ∃x ϕ | ∆ ih Γ, ϕ {x/c} | ∆ iR∀h Γ | ∆, ∀x ϕ ih Γ | ∆, ϕ {x/c} iДополнительное ограничение:константа c не содержится в формулах из Γ, ∆и в формуле ϕМетод семантических таблицПочему важны ограничения в правилах L∀, R∀, L∃, R∃?Если разрешить использовать любые подстановки в L∀, R∃:h ∀x ∃y P(x, y) | ∃y P(y, y) ih ∀x ∃y P(x, y), ∃y P(y, y) | ∃y P(y, y) i— выполнимая таблица— невыполнимая таблицаЕсли разрешить подставлять “несвежие” константы в L∃, R∀:h ∃x P(x) | P(c) ih P(c) | P(c) i— выполнимая таблица— невыполнимая таблицаМетод семантических таблицТабличный вывод — это корневое дерево, размеченноесемантическими таблицами, построенное по правилам вывода ипо каждой конечной ветви завершающееся закрытой илиатомарной таблицей(дословно переносится из логики высказываний)Успешный табличный вывод (табличное опровержение) — этоконечный вывод, все листья которого помечены закрытымитаблицамиА можно ли дословно или с незначительными изменениямиперенести из логики высказываний утверждения о табличномвыводе для проверки общезначимости формул?Следующие далее примеры показывают, что нет, не всё такпростоПримеры табличных выводовh|∀x (M(x) → A(x)) →(∀x M(x) → ∀x A(x))iR→h∀x (M(x) → A(x))|∀x M(x) →∀x A(x)iR→h∀x (M(x) → A(x)), ∀x M(x)|∀x A(x)iR∀h∀x (M(x) → A(x)), ∀x M(x)|A(c)iL∀h∀x (M(x) → A(x)), ∀x M(x), M(c)|A(c)iL∀h∀x (M(x) → A(x)), ∀x M(x), M(c) →A(c), M(c)|A(c)i∀x (M(x) → A(x)),h|A(c)i∀x M(x), A(c), M(c)Закрытая таблицаL→h∀x (M(x) → A(x)),|A(c), M(c)i∀x M(x), M(c)Закрытая таблица|= ∀x (M(x) → A(x)) →(∀x M(x) → ∀x A(x))(?)h|∃x P(x) →∀x P(x)iR→h∃x P(x)|∀x P(x)iL∃hP(c1 )|∀x P(x)iR∀hP(c1 )|P(c2 )iНезакрытая атомарная таблица6|= ∃x P(x) → ∀x P(x)(?)h|∀x ∃y P(x, y) →∃y ∀x P(x, y)iR→h∀x ∃y P(x, y)|∃y ∀x P(x, y)iL∀h∀x ∃y P(x, y), ∃y P(c1 , y)|∃y ∀x P(x, y)iR∃h∀x ∃y P(x, y), ∃y P(c1 , y)|∃y ∀x P(x, y), ∀x P(x, c2 )iL∃h∀x ∃y P(x, y), P(c1 , c3 )|∃y ∀x P(x, y), ∀x P(x, c2 )iR∀h∀x ∃y P(x, y), P(c1 , c3 )|∃y ∀x P(x, y), P(c4 , c2 )iL∀∞(???)Корректность табличного выводаЛемма корректности правил выводаКаково бы ни было правило табличного выводаL&, R &, L∨, R∨, L→, R→, L¬, R¬, L∀, R∀, L∃, R∃T0 ,T1 , (T2 )таблица T0 выполнима тогда и только тогда, когдавыполнима таблица T1 (или выполнима таблица T2 )Корректность табличного выводаДоказательство.Рассмотрим правило L→:h Γ, ϕ → ψ | ∆ ih Γ, ψ | ∆ i, h Γ | ∆, ϕ iМожет, применить доказательство из леммы корректности длялогики высказываний?Это работает.

Надо толькоIIIначать с “Пусть exn — все свободные переменные формулверхней таблицы”заменить “существует интерпретация I”на “существуют интерпретация I и набор предметов den ”заменить (не)выполнимость формулы в интерпретации I на(не)выполнимость формулы в интерпретации I на наборепредметов denЭто работает для всех логических связокКорректность табличного выводаДоказательство.Рассмотрим правило L∀:h Γ, ∀x0 ϕ | ∆ ih Γ, ∀x0 ϕ, ϕ {x0 /t} | ∆i i(⇐): очевидно: если вычеркнуть формулу из выполнимойтаблицы, она остаётся выполнимой(⇒): пусть верхняя таблица выполнима, и exn — все свободныепеременные формул нижней таблицыВерхняя таблица выполнима ⇔существуют интерпретация I и набор предметов den , такие чтоI |= Γ[den ],I 6|= ∆[den ],I |= (∀x0 ϕ)[den ]Корректность табличного выводаДоказательство.Рассмотрим правило L∀:h Γ, ∀x0 ϕ | ∆ ih Γ, ∀x0 ϕ, ϕ {x0 /t} | ∆i i(⇐): очевидно: если вычеркнуть формулу из выполнимойтаблицы, она остаётся выполнимой(⇒): пусть верхняя таблица выполнима, и exn — все свободныепеременные формул нижней таблицыПри этом:I |= (∀x0 ϕ)[den ] ⇒ I |= ϕ[t[den ], den ]I |= ϕ {x0 /t} [den ]Значит, нижняя таблица также выполнима⇒А где используется тот факт, что переменная x0 свободна длятерма t в формуле ϕ?Корректность табличного выводаДоказательство.Рассмотрим правило L∃:h Γ, ∃x ϕ | ∆ ih Γ, ϕ {x/c} | ∆ i(⇐): очевидно: если “верно для c”, то “существует предмет, длякоторого верно”(⇒): пусть верхняя таблица выполнима, и exn — все свободныепеременные формул верхней таблицыВерхняя таблица выполнима ⇔существуют интерпретация I и набор предметов den , такие чтоI |= Γ[den ],I 6|= ∆[den ],I |= (∃x0 ϕ)[den ]Последнее соотношение означает, что существует предмет d0 ,такой что I |= ϕ[d0 , den ]Корректность табличного выводаДоказательство.Рассмотрим правило L∃:h Γ, ∃x ϕ | ∆ ih Γ, ϕ {x/c} | ∆ iI |= ϕ[d0 , den ]Рассмотрим интерпретацию J , отличающуюся от I толькооценкой константы c:c = d0Тогда J |= (ϕ {x/c})[den ]Кроме того, J |= Γ[den ] и J 6|= ∆[den ]Значит, нижняя таблица выполнимаА где используется тот факт, что c — “свежая” константа?Для правил R∀, R∃ доказательство аналогичноHКорректность табличного выводаТеорема корректности табличного выводаЕсли существует успешный вывод для семантическойтаблицы T , то эта таблица невыполнимаДоказательство.

Следует из определения табличного вывода,леммы корректности правил табличного вывода и утвержденияо невыполнимости закрытых таблицСледствиеЕсли для таблицы h | ϕ i существует успешныйтабличный вывод, то |= ϕА можно ли построить этот вывод?А что делать если такого вывода не существует?Пусть существует конечный неуспешный табличный вывод:тогда формула ϕ необщезначима (почему?)Пусть такого вывода не существует:?Конец лекции 4.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций