Ещё одни лекции В.А. Захарова (1158033), страница 2
Текст из файла (страница 2)
. . , xn ) — запись обозначающая терм t, у которогоVart ⊆ {x1 , x2 , . . . , xn }.Если Vart = ∅, то терм t называется основным термом.СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫПримеры термов.x2т. к. x2 ∈ Var ;c1т. к. c1 ∈ Const;f (2) (x2 , c)т. к. f (2) ∈ Func, x2 , c ∈ Term;×(x, +(1, exp(2, y )))т. к. ×, +, exp ∈ Func,1, 2 ∈ Const, x, y ∈ Var ;x × (1 + 2y )инфиксная форма записи термов;f (c1 , g (h(c1 ), c2 ))основной терм.СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫОпределение формулы.Формула — этоатомарная формулаP (m) (t1 , t2 , . . . , tm )составная формула(ϕ&ψ)(ϕ ∨ ψ)(ϕ → ψ)(¬ϕ)(∀xϕ)(∃xϕ), если P (m) ∈ Pred, {t1 , t2 , . . . , tm } ⊆ Term;, если ϕ, ψ — формулы;, если x ∈ Var , ϕ — формула.Form — множество всех формул заданного алфавита.СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫP (m) (t1 , t2 , .
. . , tm )«значения термов t1 , t2 , . . . , tmнаходятся в отношении P (m) »;(ϕ&ψ)«ϕ и ψ»;(ϕ ∨ ψ)«ϕ или ψ»;(ϕ → ψ)«если ϕ, то ψ»;(¬ϕ)«неверно, что ϕ»;(∀xϕ)«для любого значения x верно ϕ»;(∃xϕ)«существует такое значение x,для которого верно ϕ».СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫПримеры формул.P (2) (x1 , f (c, x2 ))т. к. P (2) ∈ Pred,x1 , f (c, x2 ) ∈ Term;R (1) (x1 )т. к. R (1) ∈ Pred,x1 ∈ Term;(¬R (1) (x1 ))((∀x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 )))(∃x2 ((∀x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))))СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))) )СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))) )Область действия квантора ∃СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))) )6переменная, связанная квантором ∃Область действия квантора ∃СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))) )6связанные вхожденияпеременной x26переменная, связанная квантором ∃Область действия квантора ∃СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀ x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))))Область действия квантора ∀СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀ x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))))6переменная, связанная квантором ∀Область действия квантора ∀СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀ x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))))66связанные вхожденияпеременной x1переменная, связанная квантором ∀Область действия квантора ∀СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀ x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))))6свободные вхожденияпеременной x1Область действия квантора ∀СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.(∃ x2 ((∀x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))) )66666свободные вхожденияпеременной x1связанные вхожденияпеременной x1связанные вхождения переменной x2СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.Квантор связывает ту переменную, которая следует за ним.Вхождение переменной в области действия квантора,связывающего эту переменную, называется связанным .Вхождение переменной в формулу, не являющееся связанным,называется свободным .Переменная называется свободной , если она имеет свободноевхождение в формулу.Пример .ϕ = (∃ x2 ((∀x1 (¬R (1) (x1 ))) → P (2) (x1 , f (c, x2 ))) )Формула ϕ имеет единственную свободную переменную x1 .СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.Varϕ — множество свободных переменных формулы ϕ.mVarti ;ϕ = P (m) (t1 , t2 , .
. . , tm ) Varϕ =i=1ϕ = (ψ1 &ψ2 )ϕ = (ψ1 ∨ ψ2 )ϕ = (ψ1 → ψ2 )Varϕ = Varψ1 ∪ Varψ2 ;ϕ = (¬ψ)Varϕ = Varψ ;ϕ = (∀xψ)ϕ = (∃xψ)Varϕ = Varψ \ {x}.СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫϕ(x1 , x2 , . . . , xn ) — запись, обозначающая формулу ϕ, у которойVarϕ ⊆ {x1 , x2 , .
. . , xn }.Если Varϕ = ∅, то формула ϕ называетсязамкнутой формулой , или предложением .CForm — множество всех замкнутых формул.Соглашение о приоритете логических операцийВ порядке убывания приоритета связки и кванторырасполагаются так:¬, ∀, ∃&∨→СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫПример правильного восстановления скобок∀x1 ¬P(x1 ) & ∃x2 R(x1 , x2 ) → ∃x1 (¬P(x1 ) ∨ P(x2 ))(∀x1 (¬P(x1 ))) & (∃x2 R(x1 , x2 )) → (∃x1 ((¬P(x1 )) ∨ P(x2 )))((∀x1 (¬P(x1 ))) & (∃x2 R(x1 , x2 ))) → (∃x1 ((¬P(x1 )) ∨ P(x2 )))(((∀x1 (¬P(x1 ))) & (∃x2 R(x1 , x2 ))) → (∃x1 ((¬P(x1 )) ∨ P(x2 ))))СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫПример формулы, выражающей математическоеопределениеАлфавитКонстанты0 — константа, действительное число ноль;Функциональные символыh(2) (x, y ) — «абсолютная разность чисел x и y »;Предикатные символыR (1) (x) — «x — действительное число»;N (1) (x) — «x — натуральное число»;S (1) (x) — «x — последовательность действительных чисел»;E (3) (x, y , z) — «x — это y -ый член последовательности z»;<(2) (x, y ) — «число x меньше числа y ».СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫПример формулы, выражающей математическоеопределениеФормула limit(x, y )limit(x, y ) — «число x — предел последовательностидействительных чисел y ».limit(x, y ):R(x) & S(y ) & ∀z(R(z) & < (0, z) →∃u(N(u) & ∀v (N(v ) & < (u, v ) →∃w (E (w , v , y ) & < (h(w , x), z)))))СЕМАНТИКА: ИНТЕРПРЕТАЦИИСемантика — это свод правил, наделяющих значением(смыслом) синтаксические конструкции языка.В языке логики предикатов значением термов являютсяфункции, а значением формул — отношения (предикаты).Значения термов и формул определяются на основеалгебраических систем .Алгебраические системы, используемые в таком качестве,называются интерпретациями .СЕМАНТИКА: ИНТЕРПРЕТАЦИИИнтерпретация сигнатуры Const, Func, Pred — этоалгебраическая система I = DI , Const, Func, Pred, гдеDI — непустое множество, которое называется областьюинтерпретации , предметной областью , или универсумом ;Const : Const → DI — оценка констант ,сопоставляющая каждой константе c элемент (предмет) c̄из области интерпретации;Func : Func (n) → (DIn → DI ) — оценкафункциональных символов , сопоставляющая каждомуфункциональному символу f (n) местности n всюдуопределенную n-местную функцию f̄ (n) на областиинтерпретации;Pred : Pred (m) → (DIm → {true, false}) — оценкапредикатных символов , сопоставляющая каждомупредикатному символу P (m) местности m всюдуопределенное m-местное отношение P̄(m) на областиинтерпретации.СЕМАНТИКА: ИНТЕРПРЕТАЦИИПримерСигнатура Const = {c1 , c2 }, Func = {f (1) }, Pred = {P (1) , R (2) }.Интерпретация I = DI , Const, Func, Pred:Область интерпретацииОценка константDI = {d1 , d2 , d3 };c1 = d1 , c2 = d3 ;Оценка функциональных и предикатных символовf(x)P(x)R(x, y )xfxPd1d2d3d1 d2d1 trued1 true true falsed2 d3d2 falsed2 true false trued3 d1d3 trued3 false true trueСЕМАНТИКА: ИНТЕРПРЕТАЦИИЗначение термаПусть заданы интерпретация I = DI , Const, Func, Pred, термt(x1 , x2 , .
. . , xn ) и набор d1 , d2 , . . . , dn элементов (предметов) изобласти интерпретации DI .Значение t(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] терма t(x1 , x2 , . . . , xn )на наборе d1 , d2 , . . . , dn определяется рекурсивно.Если t(x1 , x2 , . .
. , xn ) = xi , тоt(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] = di ;Если t(x1 , x2 , . . . , xn ) = c, тоt(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] = c̄;Если t(x1 , x2 , . . . , xn ) = f (t1 , . . . , tk ), тоt(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] =f̄(t1 [d1 , d2 , . . . , dn ], . . . , tk [d1 , d2 , .
. . , dn ]).СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулЗначение формул в интерпретации определяется при помощиотношения выполнимости |=.Пусть заданы интерпретация I = DI , Const, Func, Pred,формула ϕ(x1 , x2 , . . . , xn ) и набор d1 , d2 , . . . , dn элементов(предметов) из области интерпретации DI .Отношение выполнимости I |= ϕ(x1 , x2 , . .
. , xn )[d1 , d2 , . . . , dn ]формулы ϕ в интерпретации I на наборе d1 , d2 , . . . , dnопределяется рекурсивно.Если ϕ(x1 , x2 , . . . , xn ) = P(t1 , . . . , tm ), тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒P̄(t1 [d1 , d2 , . . . , dn ], . . . , tm [d1 , d2 , . . . , dn ]) = true;СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулЕсли ϕ(x1 , x2 , . . . , xn ) = ψ1 &ψ2 , тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . .
, dn ]⇐⇒I |= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]I |= ψ2 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]Если ϕ(x1 , x2 , . . . , xn ) = ψ1 ∨ ψ2 , тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒I |= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]илиI |= ψ2 (x1 , x2 , . .
. , xn )[d1 , d2 , . . . , dn ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулЕсли ϕ(x1 , x2 , . . . , xn ) = ψ1 → ψ2 , тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒I |= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]илиI |= ψ2 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]Если ϕ(x1 , x2 , . . . , xn ) = ¬ψ, тоI |= ϕ(x1 , x2 , .
. . , xn )[d1 , d2 , . . . , dn ]⇐⇒I |= ψ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулЕсли ϕ(x1 , x2 , . . . , xn ) = ∀x0 ψ(x0 , x1 , x2 , . . . , xn ), тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . .
, dn ]⇐⇒для любого элемента d0 , d0 ∈ DI , имеет местоI |= ψ(x0 , x1 , x2 , . . . , xn )[d0 , d1 , d2 , . . . , dn ]Если ϕ(x1 , x2 , . . . , xn ) = ∃x0 ψ(x0 , x1 , x2 , . . . , xn ), тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒для некоторого элемента d0 , d0 ∈ DI , имеет местоI |= ψ(x0 , x1 , x2 , .
. . , xn )[d0 , d1 , d2 , . . . , dn ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛИнтерпретацияI = DI , Const, Func, PredОбласть интерпретацииОценка константDI = {d1 , d2 , d3 };c1 = d1 , c2 = d3 ;Оценка функциональных и предикатныхf(x)P(x)R(x, y )yxfxPd1xd1 d2d1 trued1 trued2 d3d2 falsed2 trued3 d1d3 trued3 falseсимволовd2truefalsetrued3falsetruetrueФормулаϕ = ∀x1 (P(x1 ) → ∃x2 (R(x1 , x2 ) & ¬P(f (x2 ))))СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3I |= R(x1 , x2 )[d1 , d1 ]PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3I |= R(x1 , x2 )[d1 , d1 ]I |= P(f (x2 ))[d1 ]PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falseI |= R(x1 , x2 )[d1 , d1 ]I |= P(f (x2 ))[d1 ] ⇒ I |= ¬P(f (x2 ))[d1 ]d2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falseI |= R(x1 , x2 )[d1 , d1 ]I |= P(f (x2 ))[d1 ] ⇒ I |= ¬P(f (x2 ))[d1 ]I |= R(x1 , x2 ) & ¬P(f (x2 ))[d1 , d1 ]d2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falseI |= R(x1 , x2 )[d1 , d1 ]I |= P(f (x2 ))[d1 ] ⇒ I |= ¬P(f (x2 ))[d1 ]I |= R(x1 , x2 ) & ¬P(f (x2 ))[d1 , d1 ]I |= ∃x2 (R(x1 , x2 ) & ¬P(f (x2 )))[d1 ]d2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= R(x1 , x2 )[d1 , d1 ]I |= P(f (x2 ))[d1 ] ⇒ I |= ¬P(f (x2 ))[d1 ]I |= R(x1 , x2 ) & ¬P(f (x2 ))[d1 , d1 ]I |= ∃x2 (R(x1 , x2 ) & ¬P(f (x2 )))[d1 ]I |= P(x1) → ∃x2(R(x1, x2)&¬P(f (x2)))[d1]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3I |= P(x1 )[d2 ]PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d2 ]I |= P(x1) → ∃x2(R(x1, x2)&¬P(f (x2)))[d2]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3I |= P(x1 )[d3 ]PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueI |= P(x1 )[d3 ]I |= R(x1 , x2 )[d3 , d1 ]R(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueСЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I |= R(x1 , x2 )[d3 , d1 ] ⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I |= R(x1 , x2 )[d3 , d1 ]I |= ¬P(f (x2 ))[d2 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I |= R(x1 , x2 )[d3 , d1 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]I |= ¬P(f (x2 ))[d2 ] ⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I |= R(x1 , x2 )[d3 , d1 ]I |= ¬P(f (x2 ))[d2 ]I |= ¬P(f (x2 ))[d3 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I |= R(x1 , x2 )[d3 , d1 ]I |= ¬P(f (x2 ))[d2 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]I |= ¬P(f (x2 ))[d3 ] ⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d3 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I |= R(x1 , x2 )[d3 , d1 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]I |= ¬P(f (x2 ))[d2 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]I |= ¬P(f (x2 ))[d3 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d3 ]I |= ∃x2 (R(x1 , x2 ) & ¬P(f (x2 )))[d3 ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛf(x)xd1d2d3fd2d3d1P(x)xd1d2d3PtruefalsetrueR(x, y )yd1xd1 trued2 trued3 falsed2truefalsetrued3falsetruetrueI |= P(x1 )[d3 ]I |= R(x1 , x2 )[d3 , d1 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d1 ]I |= ¬P(f (x2 ))[d2 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d2 ]I |= ¬P(f (x2 ))[d3 ]⇒ I |= R(x1 , x2 ) & ¬P(f (x2 ))[d3 , d3 ]I |= ∃x2 (R(x1 , x2 ) & ¬P(f (x2 )))[d3 ]I |= P(x1) → ∃x2(R(x1, x2)&¬P(f (x2)))[d3]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛИтак, мы имеемI |= (P(x1 ) → ∃x2 (R(x1 , x2 ) & ¬P(f (x2 ))))[d1 ]I |= (P(x1 ) → ∃x2 (R(x1 , x2 ) & ¬P(f (x2 ))))[d2 ]I |= (P(x1 ) → ∃x2 (R(x1 , x2 ) & ¬P(f (x2 ))))[d3 ]Значит,I |= ∀x1 (P(x1) → ∃x2(R(x1, x2) & ¬P(f (x2))))КОНЕЦ ЛЕКЦИИ 2.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.