Основы математической логики и теории алгоритмов
Подождите немного. Документ загружается.
)
1(8...8
,...
1
,...,
1
)(
,...
1
,...,
1
)(,...,
,...
1
,...,
1
)
1
(
8,12
,...
1
,...,
1
)...)...(
2
(
,...
1
,...,
1
)
1
(
,...
1
,...,
1
)
1
(
,...
1
,...,
1
)
1
(;
,...
1
,...,
1
)...)...(
1
(
,...
1
,...,
1
)...)...(
1
()...)...(
1
(,...,
1
)(13...13
)...)...(
1
(,...,
1
)(7...7
)...)...(
1
(
,...
1
раз
k
n
xx
n
tt
n
xx
n
tt
k
n
xx
n
tt
n
xx
n
tt
k
n
xx
n
tt
в
аксиома
n
xx
n
tt
n
xx
n
tt
n
xx
n
tt
k
n
xx
n
tt
kkn
xxразn
kn
xx
разк
k
k
41
докажем р):
8
)(
;7
))())((
14,12,11
))(,
)()(
x
t
x
t
x
t
x
t
x
t
x
t
x
xx
x
.
Покажем, что для отношения на множестве термов доказуемы обычные
свойства равенства (рефлексивности, симметричности и транзитивности), т.е.
доказуемо в ИПС
, что — отношение эквивалентности.
Предложение 5. Для любых термов t,q,r Τ(Σ) следующие секвенции доказуемы
в ИПС
:
a) ├(t
t);
b) (t
q)├(q
t);
c) (t
q),(q
r)├(t
r).
Доказательство. Доказуемость секвенции ├ (t
t) устанавливается применением
допустимого правила (п) из предложения.4:
)(
)(
)(
п
tt
xx
Для доказательства секвенции (б) рассмотрим аксиому
z
q
z
t
tztzqt )()(),(
которая
равна секвенции (t
q),( t
t)├ (q
t). Выпишем дерево, которое с участием этой
аксиомы представляет доказательство свойства симметричности:
7
8
)()(
)(;)()()(
)()(),(
tqqt
tttqttqt
tqttqt
Доказуемость секвенции (в) устанавливает следующее дерево:
8,11,12
)()(),(
)()(;)()()(
)()(),(
rtrqqt
rqqtrttqrq
rzrztq
z
t
z
q
.
Пусть A = <Α;Σ> — алгебраическая система, S = S(x
1
,..., x
n
) — секвенция ИПС
,
все свободные переменные формул которой содержатся среди x
1
,..., x
n
. Будем
говорить, что секвенция S истинна на элементах a
1
,...,a
n
А в алгебраической системе
A и писать A ╞ S(a
1
,...,a
n
), если выполняется одно из следующих условий:
1) S равна φ
1
,..., φ
n
├ψ и из A |= φ
i
(a
1
,...,a
n
) для всех i = 1,... n следует A ╞
42
ψ(a
1
,...,a
n
);
2) S равна φ
1
,..., φ
n
├ и хотя бы одна из формул φ
1
,..., φ
n
ложна на элементах
a
1
,...,a
n
А в алгебраической системе A.
Если секвенция S не истинна на элементах a
1
,...,a
n
А в алгебраической системе
A, то будем говорить, что S ложна на элементах a
1
,...,a
n
А в A. В частности,
секвенция ├ ложна на любой алгебраической системе.
Секвенция S = S(x
1
,..., x
n
) в ИПС
называется тождественно истинной, если S
истинна на любых элементах a
1
,...,a
n
А в любой алгебраической системе A = <Α; Σ>.
В дальнейшем нам предстоит доказать теорему о полноте для исчисления
предикатов, установленную К. Гёделем и утверждающую, что класс доказуемых в
ИПС
секвенций совпадает с классом тождественно истинных секвенций ИПС
. Одна
часть этого утверждения — это
Теорема 6. (теорема о непротиворечивости ИПС
). Если секвенция S
доказуема в ИПС
, то S тождественно истинна. В частности, не все формулы ИПС
доказуемы в ИПС
.
Доказательство проводится индукцией по высоте дерева доказательства
секвенции S. Тождественная истинность аксиом ИПС
очевидна. Проверку сохранения
тождественной истинности при переходе по правилам 1-16 мы проведем на примере
правила 14
x,
)(,
x
t
оставив рассмотрения остальных правил в качестве упражнения. Итак, пусть
секвенция Г, (φ)
t
x
├ψ тождественно истинна, т.е. в предположении истинности в
системе A = <Α; Σ> на каких-то элементах a
1
,...,a
n
А всех формул из Г и формулы
(φ)
t
x
мы имеем A |= ψ(a
1
,...,a
n
). Если в системе A на каких-то элементах a
1
,...,a
n
А
истинны все формулы из Г и формула
х φ, то, в частности, будет справедливо A ╞
ψ(a
1
,...,a
n
). Значит, по условию будет верно A╞ ψ(аι,..., α
η
). Следовательно, секвенция
Г, x φ├ψ тождественно истинна.
2.3.
Эквивалентность формул в
ИПС
Формулы φ и ψ сигнатуры Σ называются эквивалентными в
ИПС
(и пишут
ψ
), если секвенции φ├
и ψ ├ φ доказуемы в ИПС
.
43
Аналогично лемме 1.3.3 доказывается, что отношение является
эквивалентностью на множестве формул сигнатуры Σ. При этом отношение φ
не зависит от выбора сигнатуры, содержащей все сигнатурные символы формул ψ и
. Поэтому в дальнейшем мы будем часто говорить о доказуемости в ИПС без
упоминания конкретной сигнатуры Σ.
Формулы ψ и
сигнатуры Σ называются пропозиционалъно эквивалентными
(и пишут φ
p
), если секвенции φ├
и ψ ├ φ доказуемы в ИПС с
использованием лишь правил 1-12.
Предложение 1. Пусть φ = φ(Α
1
,..., Α
n
),
=
( Α
1
,..., Α
n
) — формулы ИС,
построенные из пропозициональных переменных, χ
1
, . . . , χ
n
- формулы сигнатуры
Σ,
'=
( χ
1
, . . . , χ
n
),
'= ψ(χ
1
,. . . , χ
n
) — формулы сигнатуры Σ, получающиеся из φ
и
соответственно подстановкой формул χ
i
вместо пропозициональных
переменных. Если имеет место ψ
в ИС, то φ'
p
'.
Таким образом, для любых формул φ,
и χ сигнатуры Σ справедливы все
утверждения лемм 1.3.4 и 1.4.1 с заменой
на
p
. Например, выполняется φ (
χ)
p
(φ
)
(
χ).
Предложение 2. В ИПС выполнимы все следующие эквивалентности, в
которых предполагается, что переменная х не входит свободно в формулу φ:
(а) x x; (б) xx;
(в)
x(
)
x
; (г)
x(
)
x
;
(д)
x(
)
x
; (е)
x(
)
x
;
(ж) xy
x
y
)(
; (з) xy
x
y
)(
;
Д о к а з а т е л ь с т в о . Приведем деревья, обосновывающие эквивалентности
(а), (в) и (ж), оставляя проверку остальных на самостоятельную работу. При этом
в пункте (а) мы будем использовать допустимое правило
, которое легко
выводится с помощью закона двойного отрицания, а в пункте (ж) — равенство
y
x
x
y
))((
.
(а)
44
13
15
xx
л
x
x
xx
xx
x
x
16
14
e
xx
xxx
x
)(|
15
)(|
5
)(|
|
16
)(|
15
)(|
4
|
|
16
|)(
|)(
5
|
|)
4
|
15
|
|
xx
e
x
xx
x
Теорема 3. (теорема о замене). Пусть φ — формула сигнатуры
,
— ее
подформула, а формула
' получается из φ заменой некоторого вхождения
на
формулу
' сигнатуры Σ. Тогда если
', то φ
'.
2.4. Нормальные формы
В этом параграфе мы определим аналоги ДНФ и КНФ, имеющие место в
исчислении предикатов, и укажем алгоритмы приведения произвольных формул
ИПС к соответствующим формам.
Будем говорить, что бескванторная формула φ сигнатуры Σ находится в
дизъюнктивной (конъюнктивной) нормальной форме (сокращенно ДНФ и КНФ
соответственно), если φ получается из формулы ИС, находящейся в ДНФ (КНФ),
подстановкой вместо пропозициональных переменных некоторых атомарных
формул сигнатуры Σ.
Будем говорить, что формула φ сигнатуры Σ находится в пренексной
(предклазуальной) нормальной форме (сокращенно ПНФ и ПКНФ соответственно),
если φ имеет вид
=Q
1
x
1
,..., Q
n
x
n
45
где Q
1
,..., Q
n
— кванторы, а
находится в ДНФ (КНФ). При этом формула
называется дизъюнктивным (конъюнктивным) ядром, а слово Q
1
x
1
,..., Q
n
x
n
-
кванторной приставкой формулы φ.
Теорема 1. Для любой формулы φ сигнатуры Σ существует формула
сигнатуры Σ, находящаяся в ПНФ (ПКНФ) и эквивалентная формуле φ.
Д о к а з а т е л ь с т в о . Для приведения формулы φ к ПНФ (ПКНФ) на
основании теоремы о замене используются эквивалентности, описанные в
предложении 2.3.3, а также эквивалентность (φ
) (
). Сначала формула φ
преобразуется в эквивалентную ей формулу φ', не содержащую символа импликации.
Затем формула φ' последовательным вынесением кванторов (при этом, если
необходимо, переименовываются связанные переменные) приводится к виду
Q
1
x
1
,..., Q
n
x
n
φ", где Q
i
€ {,}, 1<=i<=n , φ" — бескванторная формула. Наконец,
формула φ" приводится к ДНФ (КНФ), как показано в 1.4.
П р и м е р 1. Считая формулы φ и
атомарными, привести к пренексной и
предклазуальной нормальным формам формулу
χ = x
у
(x,у)
х
у
(х,у).
Избавясь от импликации, получаем
χ = x
у φ(x, у)
х
у
(х, у).,
Используя пп. (а, б) предложения 2.3.3 и теорему о замене, получаем
=
х
у
(х,у)
х
у
(х, у).,
Так как в формуле
х
у
(х, у), переменные х, у являются связанными, то
по пп. (в, г) предложения 2.3.3. имеем
χ =
х
у (
φ(x, у)
х
у
(х, у)).
Пусть и, ν — некоторые новые переменные. Тогда по пунктам (ж, з)
предложения 2.3.3 получаем
χ =
х
у (
φ(x, у)
и
v
(и,v)),
откуда
χ =
x
y
u
v (
φ(x, у)
(и,v)).
Формула
φ(x, у)
(и,v) находится в ДНФ и в КНФ одновременно, а значит,
формула
x
y
u
v (
φ(x, у)
(и,v)).находится и в ПНФ, и в ПКНФ.
46
2.5. Теорема о существовании модели
Определение. Множество формул
сигнатуры
называется
противоречивым или несовместным, если для некоторых формул
n
,...
1
в
ИПС
доказуема секвенция
|,...
1 n
.
Множество формул сигнатуры
, не являющееся противоречивым, называется
непротиворечивым или совместным.
Определение. Формула
сигнатуры
называется логическим следствием
множества формул
сигнатуры
, если в
ИПС
доказуема секвенция
|,...
1 n
для некоторых формул
n
,...
1
.
Теорема о существовании модели: Если
- совместное множество формул
сигнатуры
, то
имеет модель мощности, не превосходящей
},max{
.
Следствие 1 (теорема Геделя о полноте). Любая тождественно истинная
секвенция
ИПС
доказуема в
ИПС
.
Т.е. проверка доказуемости сводится к проверке тождественно истинности, но
в отличие от ИВ в общем случае не существует алгоритма распознавания
доказуемости формул
ИПС
, т.е.
ИПС
- неразрешимо. Однако метод резолюций
позволяет определить невыполнимость формул.
Определение. Множество формул
сигнатуры
называется локально
выполнимым, если любое конечное подмножество
0
множества
выполнимо.
Следствие 2 (теорема Мальцева о компактности). Каждое локально
выполнимое множество формул
сигнатуры
- выполнимо.
Следствие 3. Если для любого
n
множество формул
сигнатуры
имеет модель мощности
n
, то
имеет бесконечную модель.
2.6.
Исчисление предикатов гильбертовского типа
ИП
Формулами
ИП
называются формулы
, секвенций нет.
Аксиомами
ИП
являются следующие формулы для любых формул φ,
, χ,
)(,,, TtVzyx
:
1.
(
)
2. (
)
((
(
))
(
))
3. (
)
47
4. (
)
5. (
)
((
)
(
(
)))
6.
(
)
7.
(
)
8. (
)
((
)
((
)
))
9. (
)
((
)
)
10.
11.
x
t
x )(
12.
x
x
t
)(
13.
)( xx
14.
))()(()(
z
y
z
x
yx
Правила вывода в
ИП
:
1.
;
2.
x
3.
x
,
где x не входит свободно в
.
Аналогично определяются понятия доказательства формулы
(|-
) и вывод из
гипотез
)|(
.
Предложение 1. Для любых формул φ,
сигнатуры
в
ИП
справедливы
следующие соотношения:
a)
x|
b)
x
x
t
|
c)
x
x
t
|
d)
x
x
t
|
Д о к а з а т е л ь с т в о .
а )
Пусть
- доказуемое предложение, например
, тогда
2
1
;
1
;
x
x
48
b) для доказательства возьмем вторую аксиому
с
подстановкой
x
,
x
t
,
, тогда получим
1
;
1
11
Fxx
xАxxx
x
t
x
t
x
t
x
t
в аксиому 1 подставим
x
t
,
x
, продолжим доказательство:
1
1
;
;
1
x
Fx
x
x
t
x
t
x
t
x
t
с) аналогично
d)
1
;
12
x
xA
x
t
x
t
.
Справедлива теорема о дедукции: Если Γ,φ ├
, то Г ├
, где Г ― набор
некоторых формул φ
1
, ..., φ
n
.
.
Теорема об эквивалентности
ИПС
и
ИП
1) Секвенция
1
,... ,
n
├ доказуема в
ИПС
тогда и только тогда, когда
формула
выводима в
ИП
из формул
1
,... ,
n
.
2) Секвенция
1
,... ,
n
├ доказуема в
ИПС
тогда и только тогда, когда формула
xx
выводима в
ИП
из формул
1
,... ,
n
.
Следствие.
ИП
- непротиворечиво.
2.7. Скулемизация алгебраических систем
Рассмотрим конструкцию, предложенную Скулемом и позволяющую расширять
сигнатуру данной алгебраической системы так, чтобы появилась возможность
"убирать" кванторы у формул. Необходимость такого преобразования объясняется
тем, что работать с формулами, содержащими кванторы, значительно трудней, чем с
бескванторными. Далее будет изложен метод резолюций в исчислении предикатов,
использующий скулемизацию.
Алгебраическая система A = <Α; Σ> называется обогащением алгебраической
системы A' = <Α';Σ'>, если А = Α', Σ'
Σ и совпадают интерпретации всех
сигнатурных символов из Σ' в системах A и A'.
Если система A сигнатуры Σ является обогащением системы A' сигнатуры Σ', то
49
A' называется обеднением алгебраической системы A.
Пример 1. Система A = <Ζ; +, •, 0,1> является обогащением системы B = <Ζ;
+,0,1>, а система C= <Ζ;+,0> — обеднением системы B.
Определение. Пусть Σ — некоторая сигнатура,
S
— сигнатура, полученная из Σ
добавлением:
а) новых константных символов
c
для каждой формулы φ
сигнатуры Σ, имеющей вид
00
xx
;
б) новых n-местных функциональных символов
f
для каждой формулы
n
xxxx ,...,,
100
сигнатуры Σ, имеющей n > 0 свободных переменных.
Тогда сигнатура
S
называется скулемизацией сигнатуры Σ. Через S(Σ)
обозначим множество следующих предложений сигнатуры
S
, называемых
аксиомами Скулема:
а)
cxx )(
00
для каждой формулы
00
xx
сигнатуры Σ;
б)
),...,),,...,(),...,,((,...,
111001 nnnn
xxxxfxxxxxx
для каждой формулы
n
xxxx ,...,,
100
(п > 0) сигнатуры Σ.
Согласно аксиомам Скулема из существования элемента, который можно
подставить вместо переменной
0
x
в формулу
следует возможность подстановки
значения некоторой функции
f
(константы
c
), зависящего от оставшихся свободных
переменных.
Определение. Если A — алгебраическая система сигнатуры Σ, то любое ее
обогащение A
S
= <Α;
S
>, являющееся моделью множества S(Σ), называется
скулемизацией системы A. Возникающие при обогащении константы и операции,
соответствующие символам
c
и
f
, называются скулемовскими константами и
скулемовскими функциями соответственно.
Отметим, что в отличие от
S
и S(Σ) скулемизация A
S
не определяется
однозначно, поскольку из существования элементов, которые можно подставлять
вместо переменных
0
x
, вообще говоря, не следует их единственность.
Предложение 1. Любая алгебраическая система A имеет некоторую
скулемизацию A
S
.
Доказательство. Если
00
xx
, то в качестве значения
c
берем элемент
50