Exportação (lógica)

Exportação é uma regra de substituição válida na lógica proposicional. A regra permite que enunciados condicionais com  antecedentes conjuntivos  sejam substituídos por declarações com consequentes condicionais e vice-versa, em provas lógicas. A regra é que:

$((P\wedge Q)\to R)\iff (P\to (Q\to R))$

Onde "$\iff$" é um símbolo metalógico que representa "pode ser substituído em uma prova."

Notação Formal

A regra da exportação pode ser escrita em notação de sequentes:

$((P\wedge Q)\to R)⊣⊢(P\to (Q\to R))$

onde $⊣⊢$ é um símbolo metalógico que significa que $(P\to (Q\to R))$ é um equivalente sintático de $((P\wedge Q)\to R)$ em alguns sistemas lógicos;

ou na forma de regra:

$\frac{(P\wedge Q)\to R}{P\to (Q\to R)}$, $\frac{P\to (Q\to R)}{(P\wedge Q)\to R}.$

onde a regra é que, sempre que uma instância de "$(P\wedge Q)\to R$" é exibida em uma linha de uma prova, ela pode ser substituída por "$P\to (Q\to R)$" e vice-versa;

ou como uma afirmação de uma tautologia verofuncional ou teorema da lógica proposicional:

$((P\wedge Q)\to R))\leftrightarrow (P\to (Q\to R)))$

onde $P$, $Q$ e $R$ são proposições expressas em alguns sistemas lógicos.

Linguagem Natural

Valores de verdade

A qualquer momento, se P→Q é verdadeira, ela pode ser substituída por P→(P∧Q). Um possível caso em que P→Q é verdadeira, é P ser verdadeira e Q ser verdadeira, assim, P∧Q também é verdade, então P→(P∧Q) é verdadeira. Outro caso possível é P ser falsa e Q verdadeira. Assim, P∧Q é falsa e P→(P∧Q),  falso→falso, é verdadeiro. O último caso ocorre quando P e Q são falsas. Assim, P∧Q é falsa e P→(P∧Q) é verdadeira.

Exemplo

Chove e o sol brilha implica que há um arco-íris. Assim, se chove, então o sol brilha implica que há um arco-íris.

Relação com funções

A exportação é associada com "Currying" através da correspondência de Curry–Howard.