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

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

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

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

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

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

Из правил вывода исчисления высказываний в исчислении предикатов действует только правило 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.

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

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

1. Правило переименования. Из выводимости формулы 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 следует, что .

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

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

Пусть 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.

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