ExportaçãoMoore and Parkerhttp://www.philosophypages.com/lg/e11b.htm é 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:
Onde "" é 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:
onde é um símbolo metalógico que significa que é um equivalente sintático de em alguns sistemas lógicos;
ou na forma de regra: , onde a regra é que, sempre que uma instância de "" é exibida em uma linha de uma prova, ela pode ser substituída por "" e vice-versa;
ou como uma afirmação de uma tautologia verofuncional ou teorema da lógica proposicional:
onde , e 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.
Referências
Categoria:Regras de inferência