4.2.2.3. Правила заключения

а ) если F₁ и (F₁F₂) выводимые фор­мулы в исчислении предикатов, то F2 также выводима.

Это - правило modus ponens (m.p): F₁; (F₁F₂)

F₂.

b) если F₂ и (F₁F₂) выводимые формулы в исчислении предикатов, то F₁ также выводима. Это - правило modus tollens (m.t):

F₂; (F₁F₂)

F1.

Эти правила формируют схему вывода и позволяют, используя правила подстановки, введения и удаления кванторов, делать вывод об истинности заключения.

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

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

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

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

_y(P₃(y)P₄(y)_x(P₁(x)P₂(x,y)));

_y(P₃(y)P₅(y));

 _y(P₃(y)P₄(y)P₅(y));

_x(P₁(x)P₅(x)).

• F₁=_y(P₃(y)P₅(y)) - посылка;

• F₂=P₃(a)P₅(a) - заключение по F₁ и правилу П4 ИП;

• F₃= P₃(a) - заключение по F₂ и правилу П2 ИВ;

• F₄= P₅(a) - заключение по F₂ и правилу П2 ИВ;

• F₅=_y(P₃(y)P₄(y)P₅(y)) - посылка;

• F₆=P₃(t)P₄(t)P₅(t) - заключение по F₅ и правилу П2 ИП;

• F₇=P₃(t)P₄(t)P₅(t) - заключение по F₆ и ее эквивалентным преобразованиям;

• F₈=P₄(a) - заключение по F₇ при t=a;

• F₉=_y(P₃(y)P₄(y)_x(P₁(x)P₂(x,y))) - посылка;

• F₁₀=_y_x(P₃(y)P₄(y)(P₁(x)P₂(x,y))) - заключение по F₉ и правилу П6 ИП;

• F₁₁=P₃(a)P₄(a)P₁(t)P₂(t,a) - заключение по F₁₀ и правилу П2 ИП;

• F₁₂= P₃(a)P₄(a) - заключение по F₃ и F₈ и правилу введения логической связки конъюнкции П1. ИВ;

• F₁₃=(P₁(t)P₂(t,a)) - заключение по F₁₁ и F₁₂ и правилу modus ponens;

• F₁₄= P₁(t) - заключение по F₁₃ и правилу удаления логической связки конъюнкции П2. ИВ;

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

• F₁₆= P₁(t)P₅(t) - заключение по F₁₄ и F₁₅ и правилу введения логической связки конъюнкция П1. ИВ;

• F₁₇=_x(P₁(x)P₅(x)) - заключение по F₁₆ и правилу введения квантора существования П3. ИП.

Для демонстрации процесса вывода на рис. 4.8 приведен граф.

Так доказана истинность формулы _x(P₁(x)P₅(x)) при заданном наборе посылок и правил вывода.

Пример: доказать истинность заключения

 _x(_y(P₁.(x, y)P₂(y))_y((P₃(y) P₄.(x, y))); _x(P₃(x))

_x(P₃(x))_x_y(P₁.(x, y)(P₂(y))).

• F₁=_x(_y(P₁.(x, y)P₂(y))_y((P₃(y) P₄.(x, y))) - посылка;

• F₂= _x(P₃(x)) - посылка;

• F₄=P₃(t) - заключение по F₃ и правилу П2;

• F₅=P₃(t)P₄.(x, t) - заключение по F₄;

• F₆=_y(P₃(y)(P₄ (x, y))) - заключение по F₅ и правилу П1;

• F₇=_y(P₃(y)P₄(x; y)) - заключение по F₆ и правилу П5;

• F₃=_x(P₃(x)) - заключение no F₂ и правилу П5;

• F₈=_y(P₁.(t, y)P₂(y))_y(P₃(y)P₄.(t, y)) - заключение по F₁ и правилу П2;

• F₉=y(P₁.(t, y)P₂(y)) - заключение пo F₇ и F₈ при t=x и правилу m. t.;

• F₁₀=_y(P₁.(t, y)P₂(y)) - заключение по F₉ и правилу П5;

• F₁₁=_y(P₁.(t; y)(P₂(y))) - заключение по F₁₀;

• F₁₂=_x_y(P₁.(x; y)(P₂(y)) - заключение по F₁₁ и правилу П1;

• F₁₃=_x(P₃(x))_x_y(P₁.(x, y)(P₂(y))) – заключение по F₂ и F₁₂ и правилу m. p.

Так доказана истинность _x(P₃(x))_x_y(P₁.(x, y)(P₂(y))) при заданном наборе посылок и правил вывода.