Цепочка следований от противного в мат. логике

[gangstervano]

Добрый вечер.

Когда что-то доказывают от противного, то доказательство основывается на формуле:

$A \to B \equiv \neg B \to \neg A $

Но ведь не всегда метод от противного происходит в один шаг.

Допустим мы хотим доказать, что $A \to D$, для этого мы доказываем промежуточные утверждения
$A \to B, \; B \to C, \; C \to D $, из этого следует, что $A \to D $, т.е как я понимаю верна формула

$((A \to B) \land (B \to C) \land (C \to D)) \to (A \to D) \; \; \; \eqno(1)$

Метод от противного будет заключаться в том, чтобы доказать $\neg D \to \neg A$.

Правильно ли я понимаю, что в этом случае формула $ \eqno(1)$ будет иметь вид:

$((\neg D \to \neg C) \land (\neg C \to \neg B) \land (\neg B \to \neg A )) \to (\neg D \to \neg A) \; \; \; \eqno(2)$ ?

И правильно ли я понимаю, что формула $ \eqno(1)$ будет эквивалентна формуле $ \eqno(2)$ ?

Как можно доказать, что формула $ \eqno(1)$ эквивалентна формуле $ \eqno(2)$ ?

[Sender]

gangstervano в сообщении #1345967 писал(а):

Как можно доказать, что формула $ \eqno(1)$ эквивалентна формуле $ \eqno(2)$ ?

Например, получить одну из них из другой с помощью эквивалентных преобразований. Собственно, как вы получили формулу $ \eqno(2)$?

[iifat]

Как вариант, составить таблицы истинности. Для четырёх переменных всего-то шешнадцать строчек.

[arseniiv]

gangstervano в сообщении #1345967 писал(а):

Допустим мы хотим доказать, что $A \to D$, для этого мы доказываем промежуточные утверждения
$A \to B, \; B \to C, \; C \to D $, из этого следует, что $A \to D $

gangstervano в сообщении #1345967 писал(а):

Метод от противного будет заключаться в том, чтобы доказать $\neg D \to \neg A$.

И, внимание, не обязательно используя $A\to B, B\to C, C\to D$. В самом деле, если у нас эти три импликации выведены, то никакого доказательства от противного нам и не потребуется — прямое почти всегда яснее, вот его и слепим.

Кроме того, доказательство от противного имеет вид не совсем-таки «если $\neg Y\vdash\neg X$, то $X \vdash Y$» (я здесь специально использую выводимость вместо импликаций, потому что прямой формализацией таких вещей будет именно выводимость), а скорее «если $X, \neg Y\vdash\bot$, то $X\vdash Y$». Чтобы показать, что из $X$ получается $Y$, мы предполагаем $\neg Y$ вдобавок к $X$ и сводим это к противоречию ($\bot$). И тут не обязательно такое противоречие получается, потому что мы вывели $\neg X$, и не обязательно мы в выводе не пользуемся $X$, потому-то ваш вариант недостаточно хорош.

[epros]

gangstervano в сообщении #1345967 писал(а):

Когда что-то доказывают от противного, то доказательство основывается на формуле:
$A \to B \equiv \neg B \to \neg A $

Это называется законом контрапозиции. Метод от противного - это другое. Кстати, в конструктивной логике закон контрапозиции общезначим (правда в форме $(A \to B) \to (\neg B \to \neg A)$), а вот метод доказательства от противного применим не всегда.