Законы эквивалентных преобразований логики предикатов.

Правила вывода в исчислении предикатов.

Системы аксиом логики предикатов.

Системы аксиом исчисления высказываний остаются верными и в исчислении предикатов первого порядка, только к ним следует добавить еще две аксиомы, которые дают возможность оперировать с кванторами:

1. ("x) P(x)® P(y);

2. P(y) ®($x) P(x).

Эти 2 аксиомы, добавленные в классическую систему аксиом или в систему аксиом Новикова, образуют системы аксиом, обладающие свойствами полноты, независимости и непротиворечивости.

Из правил вывода исчисления высказываний в исчислении предикатов действует только правило Modus Ponens. Правило одновременной подстановки модифицировано, а остальные правила вывода касаются выводимости формул, содержащих кванторы. В этих правилах предполагается, что G(x) содержит свободные вхождения x. а F их не содержит.

1. Modus Ponens: Если выводима формула F и выводима формула F ® G, то выводима и формула G. Часто это правило записывают следующим образом:
F, F ® G ;
G

2. Правило одновременной подстановки: если терм t свободен для переменной x в формуле F, то можно подставить терм t вместо переменной x во всех вхождениях x в F.

3. Правило обобщения:
F ® G(x);
F ®"x G(x)

4. Правило конкретизации:
G(x) ® F ;
$x G(x)®F

5. Правило переименования. Из выводимости формулы G(x), содержащей свободное вхождение х, ни одно из которых не содержится в области действия кванторов "y и $y следует выводимость G(y).

Пример 6. Докажем правило переименования:

1. + G(x);

2. Из аксиомы 2 классической системы следует, что , где F – тавтология, не содержащая свободный вхождений x;

3. По правилу Modus Ponens следует, что ;

4. Используя правило обобщения, получаем: ;

5. По правилу Modus Ponens следует, что ;

6. Из аксиомы 2 логики предикатов и правила Modus Ponens следует, что .

Законы эквивалентных преобразований логики высказываний используются и в логике предикатов. Кроме них, существуют другие эквивалентные формулы, содержащие кванторы.

Пусть G есть формула, содержащая свободную переменную x. Пусть F есть формула, которая не содержит переменной x. Тогда следующие пары эквивалентных формул являются законами эквивалентных преобразований логики предикатов:

1. ("x) G(x)Ъ F=("x) (G(x)Ъ F);

2. ("x) G(x)Щ F=("x) (G(x)ЩF);

3. ($x) G(x)Ъ F=($x) (G(x)Ъ F);

4. ($x) G(x)Щ F=($x) (G(x)ЩF);

5. Ш(("x) G(x))=( $x) (ШG(x));

6. Ш(($x) G(x))=( "x) (ШG(x));

7. ("x) G(x)Щ ("x) F(x)=("x) (G(x)ЩF(x));

8. ($x) G(x)Ъ ($x) F(x)=($x) (G(x)Ъ F(x));

Правила 7 и 8 называются правилами выноса кванторов, которые позволяют распределять квантор всеобщности и квантор существования по операциям конъюнкции и дизъюнкции соответственно. Следует отметить, что нельзя распределять квантор всеобщности и квантор существования по операциям дизъюнкции и конъюнкции соответственно, то есть не эквивалентны следующие пары формул:

("x) G(x) Ъ ("x) F(x)<>("x) (G(x) ЪF(x));

($x) G(x) Щ ($x) F(x)<>($x) (G(x) Щ F(x));

В подобных случаях можно заменить связанную переменную x в формуле ("x) F(x) напеременную z, которая не встречается в G(x), так как связанная переменная является лишь местом для подстановки какой угодно переменной. Формула примет вид: ("x) F(x)= ("z) F(z). Пусть z не встречается в G(x). Тогда

($x) G(x) Щ ($x) F(x)= ($x) G(x) Щ ($z) F(z)

=($x) ($z)( G(x) Щ F(z)) по правилу 1.

Аналогично, можно написать

("x) G(x) Ъ ("x) F(x)= ("x) G(x) Ъ ("z) F(z)

=("x) ("z)( G(x) Ъ F(z)) по правилу 1.

В общем случае эти правила можно записать в следующем виде:

9.(K₁x) G(x) Ъ (K₂x) F(x)=(K₁x) (K₂z)( G(x) Ъ F(z));

10.(K₃x) G(x) Щ (K₄x) F(x)=(K₃x) (K₄z)( G(x) Щ F(z)),

где K₁, K₂, K₃, K₄ есть кванторы " или $, а z не входит в G(x).

Когда K₁= K₂=$ и K₃= K₄=", то необязательно переименовывать переменную x, можно прямо использовать правила 7 и 8.

Используя законы эквивалентных преобразований логики высказываний и логики предикатов, всегда можно преобразовать любую формулу в ПНФ.