Condicional

Símbolo

$P \rightarrow Q$ (também $P \Rightarrow Q$, $P \supset Q$). A seta indica direção: de $P$ para $Q$.

Definição

Conectivo binário. A condicional é falsa apenas quando $P$ é verdadeira e $Q$ é falsa.

Nome

Chamamos $\rightarrow$ de condicional — o conectivo que forma se $P$, então $Q$. O termo implicação costuma ser reservado para a relação de consequência lógica ($P$ implica $Q$ quando $Q$ segue necessariamente de $P$); a condicional é a proposição, a implicação é o que se passa entre proposições.

Intuição

Se $P$, então $Q$. Funciona como uma promessa: você só a quebra se $P$ ocorre e $Q$ não. Se $P$ não ocorre, a promessa é vacuosamente cumprida — nunca foi acionada.

Equivalência fundamental

$P \rightarrow Q \equiv \neg P \vee Q$.

Registro computacional

Função do tipo $P$ para $Q$. Pelo isomorfismo de Curry-Howard, uma prova de $P \rightarrow Q$ é uma função que transforma evidência de $P$ em evidência de $Q$.

def implies(p: P) -> Q: ...

Conexão com conjuntos

$P \rightarrow Q$ tem a mesma estrutura de $P \subseteq Q$. Por isso $\varnothing \subseteq A$ para todo $A$ — a verdade vacuosa sai da contenção, não é convenção.

Exemplo

Se chover, levo guarda-chuva. A promessa é quebrada apenas se chover e você não levar. Em qualquer outro cenário, permanece cumprida.

Negação

$\neg(P \rightarrow Q) \equiv P \wedge \neg Q$. Cuidado para não confundir com $\neg(Q \rightarrow P) = Q \wedge \neg P$.