Лекция 3. Выполнимые и общезначимые формулы. Модели... (Лекции 2014), страница 2

Изучим эту контрмодель.I 6|= ϕI |= ∀x (P(x) → R(x)) I 6|= ∀x P(x) → ∀x R(x)ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима. Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ.

Изучим эту контрмодель.I 6|= ϕI |= ∀x (P(x) → R(x)) I 6|= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I 6|= ∀x R(x)ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима. Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I 6|= ϕI |= ∀x (P(x) → R(x)) I 6|= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I 6|= ∀x R(x)I 6|= R(x)[d]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима. Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I 6|= ϕI |= ∀x (P(x) → R(x)) I 6|= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I 6|= ∀x R(x)I 6|= R(x)[d]I |= (P(x) → R(x))[d]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима.

Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I 6|= ϕI |= ∀x (P(x) → R(x)) I 6|= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I 6|= ∀x R(x)I 6|= R(x)[d]I |= (P(x) → R(x))[d]I |= P(x)[d]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима. Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I 6|= ϕI |= ∀x (P(x) → R(x)) I 6|= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I 6|= ∀x R(x)I 6|= R(x)[d]I |= (P(x) → R(x))[d]I |= P(x)[d]I |= R(x)[d]Получили противоречие. Значит, контрмодели I не существует.ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима.

Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I 6|= ϕI |= ∀x (P(x) → R(x)) I 6|= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I 6|= ∀x R(x)I 6|= R(x)[d]I |= (P(x) → R(x))[d]I |= P(x)[d]I |= R(x)[d]Получили противоречие. Значит, контрмодели I не существует.Значит, |= ϕ.ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима.

Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I 6|= ∀x P(x)ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I 6|= ∀x P(x)I |= P(x)[d1 ]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I 6|= ∀x P(x)I |= P(x)[d1 ]I 6|= P(x)[d2 ]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима.

Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I 6|= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I 6|= ∀x P(x)I |= P(x)[d1 ]I 6|= P(x)[d2 ]Противоречия нет.I = hDI , Predi: DI = {d1 , d2 }, P(d1 ) = true, P(d2 ) = false,I 6|= ϕ.Следовательно, 6|= ϕ.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫПопробуем систематизировать этот способ проверкиобщезначимости формул.IОбщезначимость формулы доказываем «от противного»,пытаясь построить контрмодель.IКонтрмодель строим, указывая, какие формулы должны вней выполняться, а какие нет. Требования(не)выполнимости формул, предъявляемые к контрмодели,сводим в таблицу и последовательно их уточняем.IЕсли требования, которые предъявляются к контрмодели,оказываются несовместными, значит, проверяемаяформула неопровержима, т. е.

общезначима.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫСемантическая таблица — это упорядоченная пара множествформул h Γ ; ∆ i , Γ, ∆ ⊆ Form.Γ — это множество формул, которые мы хотим считатьистинными,∆ — это множество формул, которые мы хотим считатьложными.Пусть {x1 , x2 , . . . , xn } — множество свободных переменных вформулах множеств Γ, ∆.Семантическая таблица h Γ ; ∆ i называется выполнимой ,если существует такая интерпретация I и такой набор значенийd1 , d2 , .

. . , dn ∈ DI свободных переменных, для которыхII |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] для любой формулы ϕ,ϕ ∈ Γ,II 6|= ψ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] для любой формулы ψ,ψ ∈ ∆.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫПримерыСемантическая таблицаT = h {∃x P(x), ¬P(y )} ; {∀xP(x), P(x) & ¬P(x)} iвыполнима. Ее выполнимость подтверждает интерпретацияI = hDI , Predi: DI = {d1 , d2 }, P(d1 ) = true, P(d2 ) = false, инабор d1 , d2 значений свободных переменных x, y.Семантическая таблицаT = h ∅ ; {∃y ∀xR(x, y ) → ∀x∃yR(x, y )} iневыполнима. Почему?СЕМАНТИЧЕСКИЕ ТАБЛИЦЫТеорема (о табличной проверке общезначимости)|= ϕ ⇐⇒ таблица Tϕ = h ∅ ; {ϕ} i невыполнима.Доказательство.

|= ϕ ⇐⇒ для любой интерпретации I и длялюбого набора d1 , . . . , dn ∈ DI значений свободных переменныхx1 , . . . , xn имеет место I |= ϕ(x1 , . . . , xn )[d1 , . . . , dn ] ⇐⇒таблица Tϕ = h ∅ ; {ϕ} i невыполнима ни в однойинтерпретации.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫСемантическая таблица h Γ ; ∆ i, у которой Γ ∩ ∆ 6= ∅,называется закрытой .УтверждениеЗакрытая таблица невыполнима.Доказательство. Самостоятельно.Семантическая таблица h Γ ; ∆ i, у которой множества Γ, ∆состоят только из атомарных формул, называется атомарной .УтверждениеНезакрытая атомарная таблица выполнима.Доказательство. Самостоятельно.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫТаким образом, для доказательства общезначимости |= ϕдостаточно разработать систему правил, позволяющихпреобразовывать семантическую таблицу Tϕ = h ∅ ; {ϕ} i кзакрытым таблицам.Доказательства такого вида называются логическим выводом .Если в выводе участвуют семантические таблицы, тологический вывод называется табличным .Чтобы табличный вывод был корректным, правилапреобразования таблиц (правила табличного вывода ) должнысохранять выполнимость семантических таблиц.Поэтому начнем с разработки правил табличного вывода ипроверки их корректности.КОНЕЦ ЛЕКЦИИ 3..