Нужно доказать следующую секвенцию:

$$ (\overline{(\overline{\overline{X}} \to Z}) \to \overline{\overline{(Y \to \overline{\overline{Z}})}}) \vdash ((\overline{\overline{\overline{X}} \to \overline{Y}}) \to Z) $$

При этом можно пользоваться только тремя аксиомами и секвенциями:

$$ A \to (B \to A) $$ $$ (A \to (B \to C)) \to ((A \to B) \to (A \to C)) $$ $$ (\bar{B} \to \bar{A}) \to ((\bar{B} \to A) \to B) $$

$$ 1. \space\space A \to B, B\to C \vdash A \to C $$ $$ 2. \space\space A \to (B \to C), B \vdash A \to C $$ $$ 3. \space\space \vdash(\bar{\bar{A}} \to A) $$ $$ 4. \space\space \vdash(A \to \bar{\bar{A}}) $$ $$ 5. \space\space \vdash (A \to (\bar{A} \to B)) $$ $$ 6. \space\space \vdash (\bar{B} \to \bar{A}) \to (A \to B) $$ $$ 7. \space\space \vdash (A \to B) \to (\bar{B} \to \bar{A}) $$ $$ 8. \space\space \vdash (A \to (\bar{B} \to \overline{A \to B})) $$ $$ 9. \space\space \vdash ((A \to B) \to ((\bar{A} \to B) \to B)) $$

Правило вывода одно - modus ponens.

Моё начало решения:
Переформулируем правую часть: $$ (\overline{\overline{X}} \wedge Y) \to Z $$

Вывод: $$ 1. \space\space \overline{(\overline{\overline{X}} \to Z}) \to \overline{\overline{(Y \to \overline{\overline{Z}})}} - гипотеза$$ $$ 2. \space\space \overline{\overline{X}} \wedge Y - гипотеза $$ $$ 3. \space\space \overline{\overline{X}} - свойство \space конъюнкции $$ $$ 4. \space\space Y - свойство \space конъюнкции $$ $$ 5. \space\space \overline{(Y \to \overline{\overline{Z}})} \to (\overline{\overline{X}} \to Z) - исходя \space из \space секвенции \space (6) $$

Из секвенции (9), получим: $$ ((Y \to \overline{\overline{Z}}) \to (\overline{\overline{X}} \to Z)) \to ((\overline{(Y \to \overline{\overline{Z}}}) \to (\overline{\overline{X}} \to Z)) \to (\overline{\overline{X}} \to Z)) $$

Теперь, если докажем, что $$ (Y \to \overline{\overline{Z}}) \to (\overline{\overline{X}} \to Z), $$ то через modus ponens доберёмся до Z, а завершим через теорему дедукции.

Как доказать последнюю написанную секвенцию?

задан 6 Июн '15 0:05

@falcao: вот продолжение вопроса. Однако, построив таблицу истинности для формулы, заключил, что при X и Y она верна тогда и только тогда, когда Z, которое я собираюсь доказать по этой формуле... Также при решении нельзя заменять подформулы эквивалентными формулами.

(6 Июн '15 0:06) gibsonman01

@gibsonman01: формула в самом конце не является тавтологией, то есть её просто так не вывести. У меня есть другой план доказательства, который я сейчас опишу.

(6 Июн '15 1:18) falcao
10|600 символов нужно символов осталось
0

Докажем несколько вспомогательных утверждений. Прежде всего, заметим, что справедливо такое утверждение 5': $%\vdash\bar{A}\to(A\to B)$%. Действительно, из 5 мы имеем $%\vdash\bar{A}\to(\bar{\bar{A}}\to B)$%. Принимая $%\bar{A}$% в качестве гипотезы, выводим $%\bar{\bar{A}}\to B$%. Теперь, считая $%A$% гипотезой, выводим $%\bar{\bar{A}}$% по 4, далее $%B$% по modus ponens, и дважды применяем теорему дедукции.

Проверим, что $%\overline{U\to V}\vdash U$%, а также $%\overline{U\to V}\vdash\bar{V}$%. Применим принцип доказательства от противного, основанный на Аксиоме 3. Предполагая $%\bar{U}$%, при помощи 5' выводим $%U\to V$%, что противоречит $%\overline{U\to V}$%. Формальная реализация принципа здесь простая, и я её опускаю.

Вторая часть также доказывается от противного. Принимаем отрицание $%\bar{V}$%, из 3 выводим $%V$%. Из Аксиомы 1 и modus ponens доказываем $%U\to V$%, что снова даёт противоречие.

Теперь нужное утверждение доказываем по стандартной схеме. Принимаем в качестве гипотезы посылку импликации, которую требуется вывести. В силу теоремы дедукции, достаточно доказать $%Z$%. Мы приняли $%\overline{\overline{\overline{X}} \to \overline{Y}}$%, то есть отрицание импликации. По предыдущему, отсюда выводятся $%\overline{\overline{X}}$% и $%\overline{\overline{Y}}$%, а потому $%X$% и $%Y$%. Доказывая $%Z$% от противного, примем $%\bar{Z}$%. Тогда 8 с двойным применением modus ponens даёт нам $%\overline{\overline{X}}\to Z$%. Это посылка импликации из условия. При помощи modus ponens выводим заключение импликации, то есть $%\overline{\overline{(Y \to \overline{\overline{Z}})}}$%. Снимаем двойное отрицание, применяя 3. Это даёт $%Y\to\overline{\overline{Z}}$%. Мы уже вывели $%Y$%, и тогда по modus ponens получается $%\overline{\overline{Z}}$%, что противоречит гипотезе $%{\overline{Z}}$%.

ссылка

отвечен 6 Июн '15 1:44

@falcao: то есть, в середине доказательства получим $$ \overline{\overline{\overline{X}} \to \overline{Z}} ?$$ Только не понятно, как формально описать метод от противного относительно $$\overline{Z}.$$ Смысл в том, чтобы доказать секвенцию, не прибегая к методу от противного в метаматематике, а использовать аксиомы самой теории.

(6 Июн '15 2:13) gibsonman01

@gibsonman01: метод от противного играет здесь ту же роль, что и теорема дедукции. Если рассматривать его в общем виде, то мы вместо прямого доказательства утверждения $%B$% приводим $%\bar{B}$% к противоречию, доказывая $%\bar{B}\to\bar{A}$% и $%\bar{B}\to A$% для некоторой формулы $%A$%. Тогда Аксиома 3 и двойное применение modus ponens дают нам $%B$%. Конечно, всё это реализуемо на языке только секвенций, если написать все длинные формулы. Но я думаю, что сам принцип, применяемый в этом виде, принципиально не отличается от ссылки на теорему дедукции.

(6 Июн '15 2:20) falcao
10|600 символов нужно символов осталось
Ваш ответ

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

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

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

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

отмечен:

×1,127

задан
6 Июн '15 0:05

показан
3262 раза

обновлен
6 Июн '15 2:20

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

по почте:

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

по RSS:

Ответы

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

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