Метод дедуктивного вывода

В исчисление предикатов дедуктивный вывод определяется так же, как в исчислении высказываний. Все правила вывода исчисления высказываний включены в множество правил исчисления предикатов.

Пример. Таможенные чиновники обыскивают каждого, кто въезжает в страну, кроме высокопоставленных лиц. Некоторые люди способствуют провозу наркотиков. Никто из высокопоставленных лиц не способствует провозу наркотиков. Следовательно, некоторые из таможенников способствуют провозу наркотиков?

Пусть P ₁(x)=«x – таможенный чиновник», P ₂(x, y)=«x обыскивает y», P ₃(y)=«y въезжает в страну», P ₄(y)=«y – высокопоставленное лицо», P ₅(y)=«y способствует провозу наркотиков». Тогда суждение можно формализовать так:

1) F ₁= $ y (P ₃(y)Ù P ₅(y)) – посылка;

2) F ₂= P ₃(a)Ù P ₅(a) – заключение по формуле F ₁ и правилу удаления квантора существования;

3) F ₃= P ₃(a) – заключение по формуле F ₂ и правилу удаления логической связки конъюнкции;

4) F ₄= P ₅(a) – заключение по формуле F ₂ и правилу удаления логической связки конъюнкции;

5) F ₅=" y (P ₃(y)Ù P ₄(y)® ) – посылка;

6) F ₆= P ₃(t)Ù P ₄(t)® – заключение по формуле F ₅ и правилу удаления квантора всеобщности;

7) F ₇= Ú Ú – заключение по формуле F ₆ и ее эквивалентным преобразованиям;

8) F ₈= – заключение по формуле F ₇ при t = a для =0 и =0;

9) F ₉=" y (P ₃(y)Ù ®" x (P ₁(x)Ù P ₂(x,y))) – посылка;

10) F ₁₀=" y " x (P ₃(y)Ù )® (P ₁(x)Ù P ₂(x,y))) – заключение по формуле F ₉ и правилу приведения к ПНФ;

11) F ₁₁= P ₃(a)Ù ® P ₁(t)Ù P ₂(t,a) – заключение по формуле F ₁₀ и правилу удаления квантора всеобщности;

12) F ₁₂= P ₃(a)Ù – заключение по формулам F ₃ и F ₈ и правилу введения логической связки конъюнкции исчисления высказываний;

13) F ₁₃=(P ₁(t)Ù P ₂(t,a)) – заключение по формулам F ₁₁ и F ₁₂ и правилу modus ponens;

14) F ₁₄= P ₁(t) – заключение по формуле F ₁₃ и правилу удаления логической связки конъюнкции исчисления высказываний;

15) F ₁₅= P ₅(a)= P ₅(t) – заключение по формуле F ₄ и замене предметной постоянной термом;

16) F ₁₆= P ₁(t) Ù P ₅(t) – заключение по формулам F ₁₄ и F ₁₅ и правилу введения логической связки конъюнкция исчисления высказываний;

17) F ₁₇=$ x (P ₁(x) Ù P ₅(x)) – заключение по формуле F ₁₆ и правилу введения квантора существования. Так доказана истинность формулы $ x (P ₁(x) Ù P ₅(x)).