Condicional

term: Condicional symbol: P \rightarrow Q etymology: 'Do latim condicio — "condição". A condicional liga uma condição (antecedente) a uma consequência (consequente). Símbolo →: seta de direção, de antecedente a consequente.' summary: 'Conectivo → ("se... então"). A condicional P → Q é falsa apenas quando P é verdadeira e Q é falsa.' relatedModules: [propositional-logic] seeAlso: [bicondicional, contrapositiva, conversa, inversa, modus-ponens, verdade-vacuosa]

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$.