А, та моя цитата немного о другом. Вот вы фактически получили
. Я говорил о том, что теперь если у нас есть вывод
, мы показываем
, приклеивая к первому выводу второй сразу после (ну, почти приклеивая). Ведь исходно нужно доказать, что одно выводится ттт, когда выводится второе, а не то, что оба выводятся из друг друга. Ну, это формальные заморочки.
Теперь про коммутативность. Мне кажется, начинать нужно с вывода
и дальше применить формулу (1). Верно?
Да. Вообще я надеялся на то, что вы будете использовать высокоуровневые теоремы о выводимости
типа дедукции. Смотрите, как можно управиться с коммутативностью:
, потому что
(акс.) и по теореме дедукции;
, потому что
(акс.) и по теореме дедукции;
, потому что
и теорема дедукции два раза;
осталось поприменять теорему о транзитивности выводимости, и получим
(а потом сделаем замену
— фокус, с ассоциативностью, увы, не проходящий).
Вывод, существование которого будет доказываться всеми этими теоремами, будет практически такой, как у вас получился — длинный и правильный, но не выписывать его явно, по-моему, приятно. Так же можно будет разделаться с ожидаемым
. Так как у вас дальше аналогичные штучки с дизъюнкцией, я бы посоветовал этот путь.
-- Чт май 04, 2017 17:50:45 --такой, как у вас получился — длинный и правильный
Правильность, правда, лучше бы поручать проверять не мне, а какой-нибудь программе…