Хм, пока я особо в них не вглядывался…
Вот возьмём в пример доказательство
. Для этого покажем всяческие
и покажем, что из всех их это следует.
1‒2.
. Теоремой о дедукции получаем
, что верно, потому что
.
3.
. Теоремой о дедукции получаем
. Тут так просто не отделаешься. Посмотрим на аксиому (8). С любезной помощью теоремы о дедукции она превращается в выводимость
, так что если мы покажем
,
, то получим
, то есть, через теорему о дедукции,
. У нас есть способ доказательства с дизъюнкцией в гипотезах! Применим его.
(а)
. Тут нам поможет факт
[*].
(б)
. Это верно уже ясно почему.
Раз (а) и (б), то и с 3 мы разобрались.
4.
. Теоремой о дедукции получаем
. Почему это верно, уже разобрано.
Теперь нам надо показать, что 1‒4 вообще имеют какое-то отношение к
. Для этого сначала покажем
. Это можно показать, имея
[**] и ту штуку, которую мы получили в 3 из аксиомы (8).
Теперь ясно, что если мы можем показать
и
, то получим и
. Если
— переменная, только и встречающаяся в
, этого достаточно (и, если доказать первые два в какой-то комбинации не получается, мы параллельно можем попытаться доказать
,
, чтобы убедиться, что и не получится; но почему это должно быть убедительным, вопрос отдельный). Если же в
встречается две переменные, тогда имеем
и, если все четыре вывода у нас есть, в конце мы получим
. Если переменных больше, «собираем» их аналогично до победного конца.
[*] и [**] сейчас доказвать не хочу, так что можете попробовать сами.
-- Сб апр 18, 2015 23:45:29 --(Оффтоп)
Надеюсь, понятно, зачем я вообще полез за аксиомой (8). Если нет, стоит вообще приглядеться к аксиомам и добиться представления того, «о чём они»; что они не просто тождественно истинные формулы, но и отражают некоторые типы простых логических рассуждений.