Подскажите, пожалуйста, как доказать выводимость формулы в ИВ: $%\vdash ((A \to \bar{B}) \to (B \to \bar{A}))$%.

Можно пользоваться аксиомами, правилом вывода modus pones и теоремой о дедукции.

задан 9 Окт '17 19:37

10|600 символов нужно символов осталось
1

Такого рода вещи изложены в учебнике Мендельсона (я полагаю, что аксиомы A1-A3 подразумеваются именно эти). См. пункты Леммы 1.10.

Принимаем гипотезу A->not(B). Далее принимаем B. Применяем закон двойного отрицания B->not(not(B)). Его вывод дан в книжке. Далее по modus ponens выводимо not(not(B)). Теперь применяем закон контрапозиции к первой импликации -- он тоже обоснован в учебнике. Имеем (A->not(B))->(not(not(B))->not(A)). Дважды применяем modus ponens, и выводим not(A). Теперь два раза применяем теорему дедукции.

Можно не ссылаться на закон контрапозиции. Тогда достаточно not(not(A)) привести к противоречию, что в силу схемы аксиом A3 (рассуждение от противного) позволит вывести not(A). Принимаем not(not(A)), выводим A по закону двойного отрицания (это пункт a) из Леммы). Далее по MP имеем not(B). Это противоречит принятой гипотезе B.

Можно объяснить и чуть более формально, если есть такая необходимость, но я писал примерно в том же духе, как это делается в доказательстве Леммы.

ссылка

отвечен 9 Окт '17 20:45

10|600 символов нужно символов осталось
Ваш ответ

Если вы не нашли ответ, задайте вопрос.

Здравствуйте

Математика - это совместно редактируемый форум вопросов и ответов для начинающих и опытных математиков, с особенным акцентом на компьютерные науки.

Присоединяйтесь!

отмечен:

×514

задан
9 Окт '17 19:37

показан
682 раза

обновлен
9 Окт '17 20:45

Отслеживать вопрос

по почте:

Зарегистрировавшись, вы сможете подписаться на любые обновления

по RSS:

Ответы

Ответы и Комментарии

Дизайн сайта/логотип © «Сеть Знаний». Контент распространяется под лицензией cc by-sa 3.0 с обязательным указанием авторства.
Рейтинг@Mail.ru