Dilema destrutivo
# Dilema destrutivo

Dilema destrutivo, é uma regra de inferência válida da lógica proposicional. É a inferência que diz, se P implica Q e R implica S, e Q ou S é falsa, então P ou R deve ser falsa. Em suma, se duas condicionais são verdade, e pelo menos um de seus consequentes for falso, então um dos antecedentes tem que ser falso. Dilema destrutivo é a versão disjuntiva de modus tollens, já o dilema construtivo é a versão disjuntiva de modus ponens. Formalmente:
    ${\frac {P\to Q,R\to S,\neg Q\lor \neg S}{\therefore \neg P\lor \neg R}}$
ou seja: sempre que instâncias de "$P\to Q$", "$R\to S$", e "$\neg Q\lor \neg S$" aparecerem em linhas de alguma prova, $\neg P\lor \neg R$ pode ser colocado em uma linha subsequente.

## Notação Formal

A regra do dilema destrutivo, pode ser escrita na notação sequente:
    $(P\to Q),(R\to S),(\neg Q\lor \neg S)\vdash (\neg P\lor \neg R)$
onde $\vdash$ é um símbolo metalógico significando que $\neg P\lor \neg R$ é consequência lógica de, $P\to Q$, $R\to S$, e $\neg Q\lor \neg S$ em um Sistema lógico. e expresso como uma tautologia ou teorema da lógica proposicional:
    $(((P\to Q)\land (R\to S))\land (\neg Q\lor \neg S))\to (\neg P\lor \neg R)$
Onde $P$, $Q$, $R$ e $S$ são proposições expressas em algum sistema lógico.

## Variação em Português

Se P então Q. Se R então S. P ou R. logo, Q ou S.

## Exemplo em linguagem natural

Suponha que se esteja dentro de uma casa.
    Se chover, vamos ficar em casa.
    Se estiver ensolarado, vamos ir caminhar.
    Senão, não vamos ficar em casa, ou não vamos ir caminhar, ou ambos.
    Logo, não vai chover ou não vai ser ensolarado, ou ambos.

## Prova

| Proposição | Derivação |
| $(A\rightarrow B)\land (C\rightarrow D)$ | Dado |
| $\neg B\lor \neg D$ | Dado |
| $B\rightarrow \neg D$ | Implicação material |
| $\neg D\rightarrow \neg C$ | Transposição (regra de inferência) |
| $B\rightarrow \neg C$ | Silogismo hipotético |
| $A\rightarrow B$ | Simplificação |
| $A\rightarrow \neg C$ | Silogismo hipotético |
| $\neg A\lor \neg C$ | Implicação material |