Disjunção

$${\vee }_1^{+}{\vee }_2^{+}{\vee }^{-}$$

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) (${\vee }_1^{+}$)

$${\vee }_1^{+}:p⊢p\vee q$$ ou $$\frac{\begin{array}{c}p\end{array}}{p\vee q}\left({\vee }_1^{+}\right)$$

Introdução da disjunção (direita) (${\vee }_2^{+}$)

$${\vee }_2^{+}:q⊢p\vee q$$ ou $$\frac{\begin{array}{c}q\end{array}}{p\vee q}\left({\vee }_2^{+}\right)$$

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\vee q$;
  • A sub-prova $p⊢r$, que é descartada com a aplicação da regra;
  • A sub-prova $q⊢r$, que também é descartada com a aplicação da regra;
• Uma sub-prova tem como hipótese um dos "casos" de $p\vee q$, o predicado $p$.
• A outra sub-prova tem como hipótese o outro "caso" de $p\vee 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\vee q$;
  • Portanto, $r$ pode ser escolhido sem restrições mas com o fim da prova em mente.

Eliminação da Disjunção (${\vee }^{-}$)

$${\vee }^{-}:\left\{p\vee q,\left[p⊢r\right],\left[q⊢r\right]\right\}⊢r$$ ou $$\frac{\begin{array}{ccc}p\vee q& \boxed{\begin{array}{cc}p& H\\ ⋮& \\ r& \end{array}}& \boxed{\begin{array}{cc}q& H\\ ⋮& \\ r& \end{array}}\end{array}}{r}\left({\vee }^{-}\right)$$

(Semi-)Propriedade Distributiva

$$\left(p\vee q\right)\wedge \left(p\vee r\right)⊢p\vee \left(q\wedge r\right)$$

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

A regra ${\vee }^{-}$ é aplicada duas vezes:

• Na linha 12:
  • A disjunção, $p\vee r$, está na linha 6;
  • Uma sub-prova, de $p\vee \left(q\wedge r\right)$, com hipótese $p$, em 7 - 8;
  • A outra sub-prova, também de $p\vee \left(q\wedge r\right)$, mas com hipótese $r$, em 9 - 11;
• Na linha 13:
  • A disjunção, $p\vee q$, está na linha 2;
  • Uma sub-prova, de $p\vee \left(q\wedge r\right)$, com hipótese $p$, em 5 - 6;
  • A outra sub-prova, também de $p\vee \left(q\wedge r\right)$, mas com hipótese $q$, em 5 - 12;

Pode parecer estranho porque é que $p\vee \left(q\wedge r\right)$ 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: $\left(p\vee q\right)\wedge \left(p\vee r\right)$.
  • Linha 3: $p$.
  • Linha 5: $q$.
  • Linha 7: $p$.
  • Linha 9: $r$.
• Na linha 12, quando é aplicada a regra ${\vee }^{-}$, são descratadas as hipóteses 7 e 9 e permanecem ativas:
  • Linha 1: $\left(p\vee q\right)\wedge \left(p\vee r\right)$.
  • 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.