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

UptoLike

ВУЗ: 

РУДН | Москва

Составители: 

Рубрика: 

56
стандартная
форма формулы F или просто стандартная форма
формулы F. Константы и функции, используемые для замены
переменных квантора существования, называются скулемовскими
функциями.
Пример 13.1.
Получить стандартную форму формулы F.
).,,,,,())()()()()(( wvuzyxPwvuzyx
∃
∀
∃∀∀∃
Заменяем переменную x на константу a, переменную u на
двухместную функцию f(y,z), переменную w - на трехместную
функцию g(y,z,v). Получаем следующую стандартную форму
формулы F:
)),,(,),,(,,,())()(( vzygvzyfzyaPvzy ∀∀
∀
.
Будем считать, что множество дизъюнктов S есть конъюнкция
всех дизъюнктов из S, где каждая переменная в S управляется
квантором всеобщности. Тогда стандартная форма формулы F
может быть представлена множеством дизъюнктов S .
Теорема
. Пусть S - множество дизъюнктов, представляющее
стандартную форму формулы F. Тогда F противоречива в том и
только в том случае, когда S противоречиво.
Доказательство.
Пусть F находится в предваренной нормальной
форме, т.е.
],...,[))...((
n1nn11
xxMxQxQF = . Здесь M[x
1
,…,x
n
]
означает, что матрица M содержит переменные x
1
,…,x
n
. Пусть Q
r
-
первый квантор существования и пусть
11 111 1 11 11
( )...( )( )...( ) [ ,..., , ( ,..., ), ,... ],
rrr nn r rr n
F
xxQxQxMxxfxxxx
−++ − −+
=∀ ∀
где f -скулемовская функция, соответствующая x
r
, 1
≤
r
≤
n . Нужно
показать, что F противоречива тогда и только тогда, когда F
1
противоречива.
Пусть F противоречива. Если F
1
непротиворечива, то
существует такая интерпретация I, что F
1
истинна в I, т.е. для всех
x
1
,…,x
r-1
существует по крайней мере один элемент (а именно
f(x
1
,…,x
r-1
)), для которого
],...),,...,(,...,[))...((
n1r1r11r1nn1r1r
xxxxfxxMxQxQ
+−−++
истинна в I. Таким образом F истинна в I, что противоречит
предположению. Следовательно, F
1
должна быть противоречива.
Пусть теперь F
1
противоречива. Если F непротиворечива, то
существует интерпретация I, что F истинна в I, т.е. для всех
x
1
,…,x
r-1
существует такой элемент x
r
, что

Страницы