Математическая логика и теория алгоритмов

Пусть имеется только один квантор существования /4~Vxi... VXr-l3X/- • • • лО- Положим As='ix\.., V.ViV.\:,4.1... VA' „S(XbX2,. • -Л-! Дх1^2>-• .,Xr-l), х,+ь - г д е Д х ь ~ сколемовская фушсция. Покажем, что А противоречива тогда и только тогда, когда про­ тиворечива As- Пусть Л - противоречие. Допустим, что не противоречие, следовательно, существует интерпретация, в которой А^ выполнима, т.е. для УХ1,\/Х2,... ,Vx,..i Зхг = что при Vx,+b... ,Vx „ фор­ мула В принимает значение "И", а это противоречит тому, что А - противоречие. Следовательно,/i,-— противоречие. Обратно, пусть А^ - противоречие. Допустим, что А ~ непроти­ воречие, т.е. существует интерпретация, в которой А - выполнимо. Следовательно, для VxbVx2,...,Vxr.[ найдется л> такое, что при VXrti,...,Vx „ формула В примет значение И. Введем функцию =ijCr-Тогда ясно» что А^=И, что протипоречит условию As - противоречие. Если в префиксе имеется т кванторов сутцествования, то доказательство проводится аналогично. Следствие 3.1. Если А - противоречие и As~(.Qi, .. •, Qi) C\(&Cji&.. . то A~C i &C 2&,...,& C „,. Следствие 3.2. Пусть As - стандартная форма формулы А и пусть А - противоречие. Тогда А, '-А . Отметим, что если А не является противоречием, то может быть, что А не равносильна А^. Например, пусть у4=3.\:Д.х:). Тогда As=P(a). Построим интерпретацию. Пусть область интерпретации М={\,2}. Положим, что а - ] , а Р{х) обозначает предикат «.х - четное 106