18

Билет №18
Производные правила вывода: правило одновременной подстановки, правило сложного заключения, правило силлогизма, правило контрпозиции, правила снятия двойного отрицания.
Производные правила вывода позволяют получать новые доказуемые формулы и они получаются из правил подстановки и заключения.
Правило одновременной подстановки: пусть А - доказуемая (˫) формула исчисления высказываний, x1, х2, хn - переменные, В1, В2, Вn - любые формулы. Тогда результат одновременной подстановки в А вместо x1, х2, хn формул В1, В2, Вn является доказуемой.
(˫ А)/(˫∫_(x1, х2, ...,хn )^(В1, В2,..., Вn)▒〖(А)〗)
Правило сложного заключения. Это правило применяется к формулам вида А1, А2, Аn А1 -> (А2 -> ( A3 ->...->(An -> L)...))) (*). Если данные формулы доказуемы, то доказуема и формула L. Применим правило заключения к формулам А1 и (*), тогда ˫(А2 -> ( A3 ->...->(An -> L)...)); применим к формуле А2 и(*) и так далее до тех пор пока не выяснится, что доказуема L.
Схематически правило сложного заключения записывается как: (˫ А1, А2,...,˫Аn→˫A1→(A2→(A3→(...(An→L)...)))/(˫L)
Правило силлогизма. Если доказуемы формулы A -> B, B -> C, то доказуемо A->C.
(˫A→ B, ˫ B→C)/(˫A→C)
В аксиому 1.2 сделаем подстановки
∫_(x,y,z)^(A,B,C)▒〖(1.2)〗
˫ (А→(B→C))→((A→B)→(A→C)) , где A→C=L (1)
2.
∫_(x, y)^(B→C, A)▒〖(1.1)〗
˫ (B→C)→(A→(B→C)) (2)
˫ A→B (3)
˫B→C (4)
˫ A→(B→C) (5)
Из формул (1), (3), (5) по правилу сложного заключения следует, что A→C доказуема.
Правило контр - позиции. Если доказуема A→B, то доказуема и ˫ ¬В→ ¬A
(˫A→B)/(˫¬В→ ¬A)
Для доказательства этого правила подставим вместо x, y - A, B
∫_(x,y)^(A,B)▒〖(4.1)〗
˫ (A→B)→(¬B→¬A) (1)
˫ (A→B) (2)
˫ ¬B→¬A (3)
Правило снятия двойного отрицания. Если ˫ A -> ¬(¬B), то ˫ А -> B
Если ˫ ¬(¬A) -> B, то ˫ A -> B
Для доказательства в аксиому 4.2 подставим вместо х - А, а в 4.3 вместо х - В.
∫_(х, у)^(А,В)▒〖(4.2, 4.3)〗
˫A -> ¬(¬A) (1)
˫ ¬(¬B) -> B (2)
По условию А ˫А->B (3), а по условию В ˫ ¬(¬A) -> B (4), тогда из (3) и (2) следует ˫A -> B (5), а из (1) и (4) следует ˫A -> B (6)