Основы математической логики и теории алгоритмов
Подождите немного. Документ загружается.
0
a
, для которого A╞
0
a
, если такой элемент существует, и произвольный элемент
Aa
, если такого
0
a
нет. Для формулы
n
xxxx ,...,,
100
(n > 0) и элементов
Aaa
n
,...,
1
в качестве
n
aaf ,...,
1
берем элемент
0
a
, для которого A╞
n
aaa ,...,,
10
,
если такой элемент существует, и произвольный элемент
Aa
, если такого
0
a
нет.
Скулемизация позволяет "убирать" кванторы у формул старой сигнатуры Σ.
Однако после обогащения появляются формулы новой сигнатуры
S
, в которых
кванторы "остаются". Для устранения этого недостатка используется проведение
скулемизации счетное число раз.
Пусть Σ — сигнатура, S(Σ) — множество аксиом Скулема для сигнатуры Σ.
Положим по индукции
S
0
,
n
SS
n
S
n
)(
1
. Cигнатура
n
S
n
c
S
называется
полной скулемизацией сигнатуры Σ.
Определение. Если A — алгебраическая система сигнатуры Σ, то любое ее
обогащение A
cS
= <A;
S
c
>, являющееся моделью множества
)(
n
S
n
S
, называется
полной скулемизацией системы A.
Предложение 2. Любая алгебраическая система A имеет некоторую полную
скулемизацию A
cS
.
При работе с методом резолюций нам предстоит с помощью скулемизации
снимать кванторы с формул, находящихся в предклазуальной нормальной форме.
Говорят, что формула φ находится в клазуалъной нормальной форме (КлНФ), если
она получается из формулы φ, находящейся в предклазуальной нормальной форме,
удалением всех кванторов существования с одновременной заменой соответствующих
переменных на термы, определяемые аксиомами Скулема, и последующим удалением
всех кванторов всеобщности.
Пример 2. В примере 1 главы о нормальных формах найдена формула
x
y
u
v (
φ(x, у)
(и,v)),
находящаяся в ПКНФ. С помощью скулемовских функций
xf
1
и
xf
2
(заменяющих переменные у и u соответственно), эта формула преобразуется к
следующей формуле, находящейся в КлНФ: (
φ(x,
xf
1
)
(
xf
2
,v)).
51
П р и м е р 3.Ввести скулемовские функции для формулы:
))()()(( xuzuxyzyuyzx
. Так как предикат имеет конкретный вид, то
и подбирем некоторые конкретные скулемовские функции для области
определения . Пусть
)(
1
xfz
и
),(
2
yxfu
, тогда
))),(())(),(())(((
2121
xyxfxfyxfxyxfyyx
подбирем f
1
и f
2
, чтобы
формула была истинна для любых x, y. Например,
1)(
1
xxf
и
xyxf ),(
2
, тогда
1111))())1(())1((( xxxxxyxy
2.8. Метод резолюций в исчислении предикатов
Зафиксируем некоторую сигнатуру Σ.
Подстановкой сигнатуры Σ называется конечное множество вида {t
1
/x
1
,...,t
n
/x
n
}, где
t
i
— терм сигнатуры Σ, отличный от переменных x
i
(i=1..n), и все переменные х
1
,...,х
п
различны. Подстановка, которая не содержит элементов, называется пустой и
обозначается через ε.
Мы будем использовать греческие буквы для записи подстановок.
П р и м е р 1. Множества {F
1
(z)/x, y/z}, {c
1
/x, F
2
(y)/y, F
1
(F
2
(c
2
))/z} — подстановки
сигнатуры Σ = {F
1
(1)
, F
2
(1)
, c
1
(0)
, c
2
(0)
}.
Пусть θ = { t
1
/x
1
,...,t
n
/x
n
} — подстановка сигнатуры Σ, W — множество формул
(термов) сигнатуры Σ. Тогда W θ - множество формул (термов) сигнатуры Σ, полученных
из формул (термов) множества W заменой в них одновременно всех вхождений x
i
(i=1..n)
на термы t
i
(i=1..n). При этом предполагается, что выполняются все условия на записи
формул
n
n
xx
tt
,...,
,..,
1
1
)(
,
W.
Если W = {Ф} или W = {t}, где Φ — формула, t — терм сигнатуры Σ, то вместо
{Ф}
и {t}
будем писать Φ
и t
соответственно.
П р и м е р 2. Пусть θ = { c
1
/x, F
2
(с
2
)/y,y/z} — подстановка сигнатуры Σ = {
c
1
(0)
, c
2
(0)
, . F
(1)
, F
1
(3)
, }, t = F
1
{x,y,z), Φ = (F(x) F
1
(x,c
1
,z)). Тогда tθ=F
1
(c
l
,F(c
2
),y),
Φ
= (F(c
1
)
F
1
(c
1
,c
1
, y)).
Пусть θ = { t
1
/x
1
,...,t
n
/x
n
} и λ = { q
1
/y
1
,...,q
m
/y
m
} — подстановки сигнатуры Σ.
Тогда композиция подстановок θ и
(θ ) есть подстановка, которая получается из
множества { t
1
/x
1
,...,t
n
/x
n
, q
1
/y
1
,...,q
m
/y
m
} вычеркиванием всех элементов t
j
/x
j
, для
которых t
j
= x
j
, и всех элементов q
i
/y
i
, таких, что y
I
{x
1
,..., х
п
}.
52
П р и м е р 3. Пусть θ = { t
1
/x
1
, t
2
/x
2
} = {F(y)/x, z/y}, λ = {q
1
/y
1
, q
2
/y
2
, q
3
/y
3
} = {c
1
/
x,c
2
/y,y/z} — подстановки сигнатуры Σ = { c
1
(0)
, c
2
(0)
, . F
(1)
}. Тогда t
1
/x
1
, t
2
/x
2
, q
1
/y
1
, q
2
/
y
2
, q
3
/y
3
} = {F(c
2
)/x,y/y,c
1
/x,c
2
/y,y/z}. Так как t
2
λ = у, то у/у должно быть вычеркнуто.
Так как х, у {х, у}, то c
1
/x,c
2
/y также должны быть вычеркнуты. Таким образом, θ о
= {F(c
2
)/x,
y/z}.
Подстановка θ сигнатуры Σ называется унификатором для множества {Φ
1
,..., Φ
k
}
формул сигнатуры Σ, если Φ
1
= ... = Φ
k
. Множество формул {Φ
1
,..., Φ
k
} сигнатуры Σ
называется унифицируемым, если для него существует унификатор сигнатуры Σ.
П р и м е р 4. Множество {P(c
1
,y),P(x,F(c
2
))} формул сигнатуры Σ = { c
1
(0)
, c
2
(0)
,
P
(2
,
)
. F
(1)
} унифицируемо, так как подстановка θ = {c
1
/x,F(c
2
)/y} является его
унификатором.
Унификатор σ для множества { Φ
1
,..., Φ
k
} формул сигнатуры Σ называется
наиболее общим унификатором (НОУ), если для каждого унификатора θ сигнатуры Σ
этого множества существует подстановка сигнатуры Σ такая, что θ = σ ο λ.
Пусть W = {Φ
1
,..., Φ
k
} — непустое множество атомарных формул сигнатуры Σ.
Множеством рассогласований в W называется множество термов {t
1
,...,t
k
}, где t
i
входит в
Ф
i
· и начинается с символа (который есть либо сигнатурный символ, либо переменная),
стоящего на первой слева позиции в Ф
i
·, на которой не для всех формул Φ
1
,..., Φ
k
находится один и тот же символ.
П р и м е р 5. Пусть W = {P(x,F(y,z)),P(x,c), P(x, F(y,F
1
(z))) — множество
формул сигнатуры Σ = {Р
(2)
, F
(2)
, F
1
(1)
}. Во всех трех формулах первые четыре символа
Р(х, совпадают, а на пятом месте в первой и второй формулах стоят разные символы: F, с.
Таким образом, множество рассогласований в W – { F(y,z),c, F(y,F
1
(z))}.
Алгоритм унификации предназначен для распознавания того, является ли данное
конечное непустое множество атомарных формул унифицируемым, и нахождения НОУ
для этого множества в случае его унифицируемости.
Пусть W — конечное непустое множество атомарных формул. Алгоритм
унификации для множества W:
Шаг 1. Полагаем k = 0, W
k
= W,
k
= ε.
Шаг 2. Если W
k
— одноэлементное множество, то остановка:
k
- НОУ для W. В
противном случае найдем множество D
k
рассогласований для W
k.
Шаг 3. Если существуют x
k
,, t
k
D
k
такие, что x
k
— переменная, не входящая в
53
терм t
k
, то перейти к шагу 4. В противном случае остановка: множество W не
унифицируемо.
Шаг 4. Полагаем
k+1
=
k
{ t
k
/ x
k
} и W
k+1
= W
k
{ t
k
/x
k
) (заметим, что W
k+1
=
W
k+1
)·
Шаг 5. Присвоить k значение k+1 и перейти к шагу 2.
Теорема 1. Если W — конечное непустое унифицируемое множество
атомарных формул, то алгоритм унификации будет всегда заканчивать работу на
шаге 2 и последняя подстановка σ
k
будет НОУ для W.
П р и м е р 6. Найти НОУ для множества
W={Р(с,х,F
2
(F
1
(y))),P(z,F
2
(z),F
2
(u))}.
1.
Положим k = 0, W
0
= W, σ
0
= ε.
2.
Так как W — неодноэлементное множество, то σ
0
не является НОУ для
W. Множество рассогласований для W
0
есть D
0
= {c,z}.
3.
В D
0
существует переменная x
0
=z, которая не встречается в терме t
0
=c.
Поэтому переходим к шагу 4.
4.
Полагаем σ
1
= σ
0
{с/z} = ε {с/z} = {с/z}, W
1
=
W
0
(c/z) =
{
Р(с,х,F
2
(F
1
(y))),P(c,F
2
(c),F
2
(u))
}.
5.
Присваиваем k = 1.
6.
Так как W
1
— неодноэлементное множество, множество
рассогласований для W
1
есть D
1
= {x,F
2
(c)}.
7.
Из D
1
находим, что х
1
= х, t
1
= F
2
(c).
8.
Полагаем σ
2
= σ
1
{F
2
(c)/x}, W
2
= W
1
{F
2
(c)/x} ={Р(с, F
2
(c), F
2
(F
1
(y))),
P(c, F
2
(c), F
2
(u))}.
9.
Присваиваем k = 2.
10.
Так как W
2
— неодноэлементное множество, множество
рассогласований для W
2
есть D
2
= {F
1
(y),u}.
10.
Из D
2
найдем, что х
2
= и, t
2
= F
1
(y).
11.
Полагаем
σ
3
= σ
2
{F
1
(y)/u} = {c/z,F
2
(c)/x,F
1
(y)/u},
W
3
= W
2
{F
1
(y)/
u}={P(c, F
2
(c), F
2
(F!(y))), P(c, F
2
(c),F
2
(F
1
(y)))} = {P(c,F
2
(c),F
2
(F
1
(y)))}.
12.
Множество W
3
одноэлементно. Поэтому σ
3
= {c/z,F
2
(c)/x, F
1
(y)/u} -
НОУ для W.
Литерой сигнатуры Σ называется атомарная формула или отрицание
54
атомарной формулы сигнатуры Σ. Дизъюнктом сигнатуры Σ называется литера
сигнатуры Σ или дизъюнкция литер сигнатуры Σ.
Пусть Φ — дизъюнкт сигнатуры Σ вида
1
·…
n
или
1
·…
n
, где
i
—
атомарные формулы сигнатуры Σ (1 <= i <= n). Предположим, что множество
формул {
1, …
,
п
} имеет НОУ σ. Тогда
1
σ
χσ или соответственно
1
σ
χσ
называется склейкой Ф. Полученную формулу в дальнейшем будем обозначать через
Φσ.
П р и м е р 7. В формуле Φ = Ρ (x) P(F(y)) Р
2
(x) подформулы Ρ(x) и P(F(y))
имеют НОУ σ = {F(y)/x}. Следовательно, Φσ = P(F(y))
P
2
(F(y)) — склейка Ф.
Пусть Φ
1
, Ф
2
— два дизъюнкта, не имеющих общих переменных, L
1
, L
2
—
литеры в Φ
1
и Ф
2
соответственно. Если литеры L
1
и L
2
L
2
имеют НОУ σ, то
дизъюнкт, получаемый из дизъюнкта Φ
1
σΦ
2
σ вычеркиванием L
1
σ и L
2
σ, называется
бинарной резольвентой Φ
1
и Ф
2
, а литеры L
1
и L
2
называются отрезаемыми
литерами. Если Φ
1
σ = L
1
и Φ
2
σ = L
2
, то полагаем бинарную резольвенту Φ
1
и Ф
2
равной 0.
Если Φ
1
и Ф
2
имеют общие переменные, то, заменив в формуле Ф
2
эти общие
переменные на переменные, не встречающиеся в Φ
1
и Ф
2
, получим формулу Ф
2
,
которая не имеет общих переменных с формулой Φ
1
. Бинарной резольвентой формул
Φ
1
и Ф
2
называется бинарная резольвента формул Ф
1
и Ф'
2
.
Резольвентой дизъюнктов Φ
1
и Ф
2
(res(Φ
1
,Φ
2
)) является одна из следующих
бинарных резольвент:
—
бинарная резольвента Φ
1
и Ф
2
;
—
бинарная резольвента склейки Φ
1
и Ф
2
;
—
бинарная резольвента Φ
1
и склейки Ф
2
;
—
бинарная резольвента склейки Φ
1
и склейки Ф
2
.
П р и м е р 8. Найти res(Ф
1
,Ф
2
), где
))(())(()(
111
yFPyFPxPФ
;
)()))(((
22112
cPcFFPФ
Склейка
))(())((}/)({
1111
yFPyFPxyFФФ
, тогда
)))((()(),(),(
111222121
сFFPcPФФresФФres
Пусть S — множество дизъюнктов сигнатуры Σ. Резолютивный вывод
формулы Φ из S есть такая конечная последовательность Φ
1
, ..., Ф
k
дизъюнктов, что
55
Φ
k
: = Φ и каждый дизъюнкт Φ
i
или принадлежит S, или является резольвентой
дизъюнктов, предшествующих Ф
i
.
Универсальным замыканием формулы Φ(x
1
,... ,х
п
) называется предложение
x
1
,... ,х
п
Φ(x
1
,... ,х
п
).
Теорема 2. (теорема о полноте метода резолюций). Если S — множество
дизъюнктов сигнатуры Σ, то множество универсальных замыканий формул из S
невыполнимо тогда и только тогда, когда существует резолютивный вывод нуля
из S.
П р и м е р 9. Доказать невыполнимость множества формул W = {Φ
1
,...,Φ
6
},
где
Φ
1
=P
1
(c
1
,F(c
2
),F(c
3
)),
Φ
2
= P
2
(c
1
),
Φ
3
= Ρ
1
(x,x,F(x)),
Φ
4
= Ρ
1
(x,y,z) Ρ
3
(x,z),
Φ
5
= Ρ
2
(x) Ρ
1
(y,z,u) Ρ
3
(x,u) Ρ
3
(x,y) Ρ
3
(x,z),
Φ
6
=Ρ
3
(c
1
, c
3
).
Построим резолютивный вывод 0 из W:
Ф
7
= геs(Ф
2
,Ф
5
) = геs(Ф
2
,Ф
5
{z/y}) = Ρ
1
(z,z,u) Ρ
3
(c
1
,u) Ρ
3
(c
1
,z);
}/{
1
xc
Ф
8
= res(Φ
3
, Ф
7
) = Ρ
3
(c
1
,F(x)) Ρ
3
(c
1
,x);
}/)(,/{ uxFzx
Ф
9
=res(Ф
6
,Ф
8
) =Ρ
3
(c
1
,F(c
3
));
}/{
3
xc
Ф
10
= геs(Ф
4
,Ф
9
) = Ρ
1
(c
1
,y, F(c
3
))
}/)(,/{
31
zcFxc
Φ
11
=res(Φ
1
,Φ
10
) =0.
}/)({
2
ycF
П р и м е р 10. Показать выполнимо ли множество формул {Ф
1
,Ф
2
}?
)()()(),(
43211
yPyPxPzxPxzyФ
;
),()()(
1342
yxyPxPxPxФ
Приведем формулы к ПКНФ:
)(),()())(),((
413211
yPzxPyPxPzxPxzyФ
.
),()()(
1342
yxPxPxPyxФ
.
Приведем к КлНФ: Введением скулемовской константы с и функции F,
получаем, что выполнимость формул Ф
1
,Ф
2
сигнатуры
)1(
4
)1(
3
)1(
2
)2(
1
,,, PPPP
56
равносильна выполнимости формул {
)(),()())(),((
41321
сPzxPсPxPzxPxz
,
))(,()()(
134
xFxPxPxPx
} сигнатуры
},{
)1(
Fc
или {
),(,),()()),(),((
41321
сPzxPсPxzxPzxPxz
))(,(,)()(
134
xFxPxxPxPx
}.
{
),(,),()(),(),(
41321
сPzxPсPxPzxP
))(,(,)()(
134
xFxPxPxP
}.
}/)({)()))(,(,),()((
3113
zxFсPxFxPzxPсPres
}/{)())(,)()((
4334
xccPcPxPxPres
0))(),((
44
cPcPres
, тогда множество формул – невыполнимо.
Следующий пример показывает, как формализуются предложения и методом
резолюций эффективно доказываются теоремы при переходе к соответствующим
формализациям.
П р и м е р 11. Установить, что из посылки "Студенты суть граждане" следует
заключение "Голоса студентов суть голоса граждан".
Пусть формулы S(x),C(x) и V(x,y) означают "х — студент", "х — гражданин"
и "х есть голос у" соответственно. Тогда посылка и заключение запишутся
следующим образом:
y(S(y)
C(y)) (посылка),
x(
y(S(y)
V(x, у))
z(C(z)
V(x, z))) (заключение).
Формула, соответствующая посылке, эквивалентна дизъюнкту
-
S(y)
C(y).
Так как
x(
y(S(y)
V(x, у))
z(C(z)
V(x, z)))
x(
y(
S(y)
V(x, у))
z(C(z)
V(x, z)))
x
y
z
(
S(y)
V(x, у)
(C(z)
V(x, z)))
x
y
z(S(y) V(x, у) (
C(z)
V(х, z))), имеем три дизъюнкта, определяющие отрицание заключения (а,в –
скулемовские константы):
S(b), V(a,b),
C(z)
V(a,z).
Доказательство заканчивается следующим образом:
res(
S(y)
C(y),
S(b))=C(b),
res(C(b),
C(z)
V(a,z))=
V(a,b),
res(V(a,b),
V(a,b))=0.
Т.о. теорема доказана.
57
2.9. Некоторые проблемы аксиоматического исчисления
предикатов
2.9.1. Разрешимость
Проблема, заключающаяся в отыскании алгоритма, решающего ту или иную серию
однотипных задач, называется алгоритмической проблемой разрешимости.
Неразрешимость алгоритмической проблемы означает, что такой алгоритм
невозможен. Простейший пример проблемы разрешимости— проблема разрешимости
алгебры логики, которая состоит в отыскании алгоритма, позволяющего для любой
формулы алгебры логики установить, является ли она тождественно истинной,
тождественно ложной или выполнимой. Для алгебры логики эта проблема решена.
Проблема разрешимости для исчисления предикатов, в отличие от исчисления
высказываний, оказалась связанной с серьезными трудностями, зависящими от точного
определения понятия алгоритма. После появления точного определения алгоритма
появилась возможность доказать, что проблема разрешимости для исчисления
предикатов неразрешима, т. е. необходимый в ЭТОЙ проблеме алгоритм невозможен
.
2.9.2. Непротиворечивость и независимость
Противоречивым называется такое исчисление, в котором какая-либо формула
доказуема вместе со своим отрицанием. Эта проблема для исчисления предикатов
решается в положительном смысле. Для доказательства непротиворечивости
достаточно обнаружить какую-нибудь невыводимую формулу в исчислении
предикатов.
Можно показать, что всякой выводимой формуле исчисления предикатов
соответствует выводимая формула исчисления высказываний, для которого
проблема непротиворечивости решена. Отсюда немедленно следует непроти-
воречивость исчисления предикатов. В самом деле, если бы исчисление предикатов
было противоречиво, то в нем всякая формула была бы выводимой. В частности, была
бы выводима формула А, состоящая из одной буквы. Но тогда А была бы выводима и в
исчислении высказываний, что не верно. Помимо непротиворечивости возникает
вопрос о выводимости каждой аксиомы из остальных. Это вопрос независимости
системы аксиом. Система аксиом исчисления предикатов — независимая система.
Независимость аксиом говорит о том, что в системе нет лишних аксиом. Эту
58
независимость можно установить посредством интерпретации. Метод интерпретаций,
однако, приложим к вопросам независимости только в известных границах. Ранее
обсуждался вопрос независимости аксиом исчисления высказываний. Вопрос о
независимости аксиом обычно ставится для непротиворечивых систем. В этом случае
ограничиваются сведением независимости к вопросу о непротиворечивости данной
системы аксиом.
2.9.3. Полнота в узком смысле
Логическая система называется полной в узком смысле, если нельзя без противоречия
присоединить к ее аксиомам в качестве новой аксиомы никакую не выводимую в ней
формулу так, чтобы полученная при этом система была бы непротиворечивой.
В отличие от исчисления высказываний, исчисление предикатов оказывается неполным
в узком смысле. К его аксиомам можно присоединить без противоречия недоказуемую
в нем формулу
xF(x) —>
xF(x). Все предметы тождественны — таков
содержательный смысл этой формулы. Приведем для доказательства лишь
соображения, носящие общий характер. Каждая выводимая формула исчисления
высказываний имеет выводимый аналог в исчислении предикатов и может быть
присоединена к аксиомам этого исчисления. Например, такая: А—> А. Она выводима в
исчислении высказываний. Если область определения М предиката F(x) состоит из
одного элемента х, то А—> А превращается в исчислении предикатов в формулу
xF(x) —>
xF(x), которая будет истинной. Она не будет истинной, если М
содержит больше, чем один элемент. Однако из общелогических положений нельзя
заключить, что область М содержит более одного элемента. Таким образом,
исчисление предикатов неполно в узком смысле.
2.9.4. Полнота в широком смысле
Логическая система полна в широком смысле, если любая тождественно истинная
формула в нем доказуема. На основании теоремы Геделя проблема полноты в
широком смысле решается для исчисления предикатов положительным образом.
Все выводимые формулы исчисления предикатов представляют собой тождественно
истинные высказывания. Обратно, каждая тождественно истинная формула выводима
в исчислении предикатов. Из этого ясно, что в исчислении предикатов нельзя вывести
сколько-нибудь содержательное по существу высказывание, в частности,
математическое. Однако если к аксиомам исчисления предикатов присоединить какие-
59
либо невыводимые формулы в качестве новых аксиом, то получится другое
исчисление, в котором выводимы, помимо тождественно истинных формул, и другие
формулы. Средствами этого исчисления могут быть описаны различные
математические дисциплины, например арифметика, теория чисел, геометрия, теория
множеств. Любая дедуктивная система может быть выражена указанными средствами.
При этом любая выбранная система аксиом должна быть внутренне непротиворечива и
независима, т. е. каждая из аксиом должна быть не выводима из остальных.
3. ЭЛЕМЕНТЫ ТЕОРИИ АЛГОРИТМОВ
При изучении дискретной математики и формальных исчислений мы
рассматривали большое количество различных алгоритмов. Это и алгоритм Евклида
нахождения наибольших общих делителей, и алгоритмы нахождения кратчайших
маршрутов во взвешенном графе, и алгоритм распознавания доказуемости формул
исчисления высказываний.
Отметим несколько основных общих черт алгоритмов.
1. Алгоритм — это процесс последовательного построения (вычисления)
величин, протекающий в дискретном времени так, что в начальный момент
времени задается исходная конечная система величин, а в каждый последующий
момент система величин получается по определенному закону (программе) из
системы величин, имевшихся в предыдущий момент времени (дискретность
алгоритма).
2. Система величин, получаемых в любой не начальный момент времени,
однозначно определяется системой величин, полученных в предыдущие моменты
времени (детерминированность алгоритма).
3. Закон получения последующей системы величин из предшествующей
должен быть простым (элементарность шагов алгоритма).
4. Если способ получения последующей величины из какой-нибудь
заданной величины не дает результата, то должно быть указано, что надо считать
результатом алгоритма (направленность алгоритма).
5. Алгоритм должен быть пригоден для решения всех задач из заданного
класса (массовость алгоритма).
60