Лекции по дискретной математике. Математическая логика. Зарипова Э.Р - 57 стр.

UptoLike

57
(Q
r+1
x
r+1
)…(Q
n
x
n
)M[x
1
,…,x
r-1
, x
r
,x
r+1
,…x
n
]
истинна в I. Расширим интерпретацию I, включив в нее функцию f,
которая отображает (x
1
,…,x
r-1
) на x
r
для всех x
1
,…,x
r-1
из D , т.е.
f(x
1
,…,x
r-1
)=x
r
. Обозначим такое расширение I через I
. Ясно, что
для всех x
1
,…,x
r-1
],...),,...,(,...,[))...((
n1r1r11r1nn1r1r
xxxxfxxMxQxQ
+++
истинна в I
, т.е. F
1
истинна в I
, что противоречит предположению
о противоречивости F
1
. Следовательно F - противоречива.
Пусть в F имеется m кванторов существования. Пусть F
0
=F, а
F
k
получается из F
k-1
заменой первого квантора существования в
F
k-1
скулемовской функцией, k=1,…,m. Ясно, что S=F
m
.
Аналогично предыдущему можно показать, что F
k-1
противоречива
тогда и только тогда, когда F
k
противоречива, k=1,…,m. Т.о. F
противоречива тогда и только тогда, когда множество S
противоречиво.
Замечания.
Пусть S- стандартная форма формулы F. Если F противоречива,
то из доказанной теоремы следует, что F=S . Если F -
непротиворечива, то вообще говоря F
S.
Например: F: (x)P(x), S:P(a). S есть стандартная форма
формулы F. Пусть I есть следующая интерпретация:
D={1,2}, a=1, P(1)= Л,P(2)=И
Тогда F истинна в I, но S ложна в I , т.е. F
S. Отметим, что
формула может иметь более чем одну стандартную форму.
Подстановка и унификация.
В методе резолюций существенным является нахождение
контрарных пар. Для дизъюнктов, не содержащих функции это
просто. Задача усложняется для дизъюнктов, содержащих
функции.
Пример 13.1.
)())((:
)()(:
xRxfPC
xQxPC
2
1
Здесь нет контрарных пар. Но если в C
1
вместо x подставить f(a), а
в C
2
вместо x подставить a, то получим