Шаг 1:
Наличие вывода
эквивалентно наличию вывода
Теперь покажем, если ещё не показаны, выводимости
,
и
и ещё вспомним теорему, что если
и
, то
. Теперь пользуемся всем этим, получаем результирующую выводимость и конструируем вывод, который её показывает, по деталям доказательства этих двух метатеорем и выводов производных правил.
-- Вт ноя 29, 2016 21:38:06 --Кажется, никаких требований не потерял.
Спасибо, попробую понять это.
Как доказывается знаю, но не понимаю, как её здесь применить.
Тогда что скажете про первый вопрос?
Выглядит очень очевидно, я понимаю, что это так. Но как доказать с помощью аксиом ИВ не понимаю, хоть и прочитал уже довольно много литературы на эту тему.