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

Математическая логикаЛектор:Подымов Владислав Васильевич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.