Вот! Так намного лучше. (Надеюсь, у вас есть где-нибудь рядом вывод
, а то я его не помню, а он тут нужен.)
Как прийти к доказательству? Т. к. правило у нас пока только одно — Modus ponens — мы можем вывести только то, что есть в правой части какой-нибудь импликации в аксиомах. Там, в этих правых частях, есть всё, что может попасться в довольно сложной формуле. Так что надо выбрать какую-нибудь аксиому и попробовать с ней вывести.
Например, последняя аксиома вряд ли нам бы принесла что-то полезное, хотя при желании можно было бы составить вывод и с её использованием. Давайте попробуем восьмую:
. Неформально, она говорит, что если из каждой альтернативы дизъюнкции что-то следует, то и из целой дизъюнкции оно следует. А у нас как раз надо вывести, что из дизъюнкции
следует
. Может, мы сможем переписать эту аксиому так, чтобы
могло быть выведено? Да, можем: надо только заменить
на
. Получится такая аксиома:
Как с помощью неё можно было бы вывести то, что надо? Есть только Modus ponens, и он говорит, что если
, то
. И что потом если
, то и
. А это как раз цель.
Можем ли мы вывести
? Да, притом гипотеза тут не используется (это я предоставляю вам). Можем ли мы вывести
? Да: доказательством этого будет одна строка — собственно, использование гипотезы, которая одновременно и то, что надо получить.
Теперь, используя аксиому 8 в форме
, два имеющихся доказательства
и
, попробуйте собрать доказательство
. Не получится — кто-нибудь поправит. Пробуйте!
(Кстати, это так повезло с тем, что формула «близко» к аксиомам и её можно в них как бы увидеть. В принципе, и более сложные можно так разглядывать, но обычно для этого вводят новые правила вывода. Каждый вывод
порождает правило вывода
— его использование всё равно что вставка доказательства
в использующее доказательство. Например, можно доказать
и использовать потом как правило введения конъюнкции. Достаточно сложные формулы с такими правилами выводятся (если они выводимы вообще) почти автоматически.)
(.)
Только не
, а
(
\vee или
\lor).