Disjunção

$$\Huge \ndIDisjL \qquad \ndIDisjR \qquad \ndEDisj $$

As regras da disjunção são menos diretas do que as anteriores:

1. Existem dois casos para a introdução: esquerdo e direito. Tal como as regras de eliminação da conjunção.
2. A regra da eliminação descarta duas sub-provas.

Introdução da Disjunção

Introdução da disjunção (esquerda) ($\ndIDisjL$)

$$\Large \ndIDisjL: p \vdash p \lor q $$ ou $$\Large \ndrule{p}{p \lor q}{\ndIDisjL} $$

Introdução da disjunção (direita) ($\ndIDisjR$)

$$\Large \ndIDisjR: q\vdash p \lor q $$ ou $$\Large \ndrule{q}{p \lor q}{\ndIDisjR} $$

Nestas regras a conclusão inclui um predicado que não ocorre nas hipóteses — $q$ na regra esquerda e $p$ na direita:

• Este predicado pode ser um qualquer, o que dá uma grande liberdade para a construção da prova.
• Porém, se esse predicado não for bem escolhido em nada contribui para a conclusão a que se pretende escolher.

Eliminação da Disjunção

Esta regra é, talvez, a mais complexa da Dedução Natural Proposicional:

• As hipóteses são:
  • Uma disjunção, $p \lor q$;
  • A sub-prova $p \vdash r$, que é descartada com a aplicação da regra;
  • A sub-prova $q \vdash r$, que também é descartada com a aplicação da regra;
• Uma sub-prova tem como hipótese um dos “casos” de $p \lor q$, o predicado $p$.
• A outra sub-prova tem como hipótese o outro “caso” de $p \lor q$, o predicado $q$.
• Em cada uma das sub-provas a conclusão, $r$:
  • É comum às sub-provas;
  • Não ocorre na disjunção $p \lor q$;
  • Portanto, $r$ pode ser escolhido sem restrições mas com o fim da prova em mente.

Eliminação da Disjunção ($\ndEDisj$)

$$\Large \ndEDisj: \cbr{p \lor q, \sbr{p \vdash r}, \sbr{q \vdash r} } \vdash r $$ ou $$\Large \ndrule{ p \lor q & \ndsub{p & H\cr \vdots \cr r} & \ndsub{q & H\cr \vdots \cr r} }{r}{\ndEDisj} $$

(Semi-)Propriedade Distributiva

$$\del{p \lor q} \land \del{p \lor r} \vdash p \lor \del{q \land r}$$

As sub-provas foram indentadas para facilitar a leitura. Esta indentação é opcional e nem sempre será aplicada.

A regra $\ndEDisj$ é aplicada duas vezes:

• Na linha 12:
  • A disjunção, $p \lor r$, está na linha 6;
  • Uma sub-prova, de $p \lor \del{q \land r}$, com hipótese $p$, em 7 - 8;
  • A outra sub-prova, também de $p \lor \del{q \land r}$, mas com hipótese $r$, em 9 - 11;
• Na linha 13:
  • A disjunção, $p \lor q$, está na linha 2;
  • Uma sub-prova, de $p \lor \del{q \land r}$, com hipótese $p$, em 5 - 6;
  • A outra sub-prova, também de $p \lor \del{q \land r}$, mas com hipótese $q$, em 5 - 12;

Pode parecer estranho porque é que $p \lor \del{q \land r}$ aparece cinco vezes como conclusão, nas linhas 4, 8, 11, 12 e 13.

Nas últimas três foram descartadas hipóteses temporárias, para sub-provas. Até ao descarte essas hipóteses estão “ativas” e teriam de aparecer na lista de hipóteses “final”:

• Na linha 11 as hipóteses ativas são:
  • Linha 1: $\del{p \lor q} \land \del{p \lor r}$.
  • Linha 3: $p$.
  • Linha 5: $q$.
  • Linha 7: $p$.
  • Linha 9: $r$.
• Na linha 12, quando é aplicada a regra $\ndEDisj$, são descratadas as hipóteses 7 e 9 e permanecem ativas:
  • Linha 1: $\del{p \lor q} \land \del{p \lor r}$.
  • Linha 3: $p$.
  • Linha 5: $q$.
• Na linha 13, depois de aplicada a regra, são descartadas as hipóteses 3 e 5 e permanece ativa a linha 1.