являются кванторы существования 3xi..3xni, то им соответствуют постоянные функции, которые сводятся к заданию их значений ai,...,ani-

Сняв группу кванторов в формуле Л, мы в В оставляем переменные 2/1,..., Уп21 по которым стояли кванторы всеобщности, а вместо следующих за ними переменных zi,..., связанных кванторами существования, подставляем полученные функции gi{yi, ...,2/2)-

В результате имеем набор функций

ai,...,a„i,gi(2/i,...,2/„J,...,g„3 (yi,-, 2/12).-...,hi{wi,...,Wnk-i),---hnk (wi, ...,U)„j, J

и формулу

B(ai, ...,a„i,2/i, ...,2/„2,ffi(2/ii--lyns), ,дпзivi,2/rt2)i

...,Sl{wi,...,Wnk-l), ,8пк {Wl, ....U)„j, J).

(1.6)

(1.7)

Функции (1.6) называются сколемовскими (разрешающими) в интерпретации Ш, если формула (1.7) истинна в Ш. Очевидно, что формула (1.7) истинна в Ш1 тогда и только тогда, когда

ОТ НА,

As = V2/i...V2/„2---VU)i...V№„j, iB(ai,ащ, yi, ...,gi{yi,2/2)1

...,wi, ...,hi{wi, ...,Wnk i), hnk{wi,...,Wn -i))-

Формула As не содержит кванторов существования и является V-формулой, полученной в результате сколемизации исходной формулы А.

Теорема 1.6 (Эрбран). Формула А имеет модель Ш тогда и только тогда, когда для нее существуют сколемовские функции.

Доказательство.

Рассмотрим только случай формулы, начинающейся с группы кванторов существования Применим метод математической индукции по числу Ipyun кванторов.

Если

А = ЧХ1...ЧХпВ{Х1, ...,Хп):

Полное доказательство см. в [32].

то, как следует ш определения модели, 9[)Т [= Л тогда и только тогда, когда существует набор элементов ai,an G М, для которого A{ai, ...,ап) = Т. Но набор ai,...,an - это как раз сколемовские

фуНК7ДИИ Д/1Я А.

Пусть теорема верна для формул с р группами кванторов и дана формула

А=Чх1..3хпгУ1-Уп2-В{х1,...,у1,...), (1.8)

содержащая (р + 1) группу кванторов.

Для того чтобы формула А была истинна в интерпретации 9[)Т, необходимо и достаточно, чтобы существовали oi,an € М такие, что формула

С = \/у1...Ууп2 ...B(ai,а„1, yi,...)

была истинна в 9[)Т. Но формула С содержит уже р групп кванторов. Поэтому по индукционному предположению 9ОТ = С тогда и только тогда, когда существуют сколемовские функции

9i(2/i, 2/112)1 ,"3(2/1, ,Уп2), для формулы с. Легко видеть, что функции

ai,...,a„i,gi(2/i,...,2/„2),...,g„3(2/i, ...

являются сколемовскими для А. Для них формула

B(ai,а„1,2/1,2/„2.Si(2/i. 2/12). )

истинна в Ш1. Но это означает истинность формулы А в Ш1. Теорема 1.6 доказана.

Пример 1.2. Провести сколемизацию формулы

А = 3x3yizu3vB{x, y,z,u,v).

Переменные х, у заменяем на константы а, b соответственно. Переменные z,u оставляем, а вместо г; вводим сколемовскую функцию f(z,u). Получаем формулы

B{a,b,z,u,f{z,u))

Л{а,Ь) =VzV«i3(a,6,2,«,/(2,«)).

1.3. Метод резолюций

1.3.1. Метод резолюций в логике высказываний

Предположим, что дана формула логики высказываний А. Как проверить общезначимость формулы Л? Это задача решается с помощью метода резолюций Дж. Робинсона, к изложению которого мы приступаем.

Очевидно, что = А тогда и только тогда, когда является противоречием формула -lA.

Формулу ~>А приводим к конъюнктивной нормальной форме (КНФ). КНФ - это формула, равносильная данной формуле и записанная в виде конъюнкции элементарных дизъюнкций, построенных на пропозициональных переменных, т.е. в данном случае

~A = ViL...k.Vp,

где Т>г есть дизъюнкция конечного числа пропозициональных переменных или их отрицаний. Тем самым мы формируем множество дизоюнктов К = {Vi,Т>р}.

Два дизъюнкта этого множества T>i и T>j, содержащие пропозициональные переменные с противоположными знаками, - контрарные литералы, т.е., к примеру, У и ~~iY, и, следовательно, Т>г - Т>{У Y, T>j - T>j V -Y, формируют третий дизъюнкт - резольвенту Т>\ V T>j, в которой исключены контрарные литералы:

в частности, если T>i = Y, Vj = ~iY, то резольвента для них -это дизъюнкция, ничего не содержащая (отсутствуют Т>[ и Т>). Ее называют пустой резольвентой и обозначают знаком □.

Теорема 1.7. Резольвента Т>[ У Vj, - это логическое следствие дизоюнктов Vi и Vj, т.е.

Vi,VjiV[y Vj).

Одним из первых реализовал метод Эрбраыа на вычислительной машине Гилмор. Однако его программа справилась с доказательством нескольких простых формул, но столкнулась с большими трудностями в доказательстве других формул логики первого порядка.