Зарипова, Э.Р. Дискретная математика Часть II. Математическая логика
65 противоречива в том и только в том случае, когда S противоречиво. Доказательство. Пусть F находится в предваренной нормальной форме, т.е. ] ,..., ) [ )...( ( n 1 n n 1 1 F Q x Q x M x x . Здесь M [ x 1 ,…,x n ] означает, что матрица M содержит переменные x 1 ,…,x n . Пусть Q r - первый квантор существования и пусть 1 1 1 1 1 1 1 1 1 1 ( )...( )( )...( ) [ ,..., , ( ,..., ), ,... ], r r r n n r r r n F x x Q x Q x M x x f x x x x где 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 )) , для которого ,... ] ), ,..., , ( ..., ) [ )...( ( r 1 r 1 n 1 r 1 1 n n r 1 r 1 f x x x x Q x Q x M x x истинна в I . Таким образом F истинна в I , что противоречит предположению. Следовательно, F 1 должна быть противоречива. Пусть теперь F 1 противоречива. Если F непротиворечива, то существует интерпретация I , что F истинна в I , т.е. для всех x 1 ,…,x r-1 существует такой элемент x r , что (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 ,... ] ), ,..., , ( ..., ) [ )...( ( r 1 r 1 n 1 r 1 1 n n r 1 r 1 f x x x x Q x Q x M x x истинна в 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 противоречива,
Made with FlippingBook
RkJQdWJsaXNoZXIy MTExODQxMg==