Exportação (lógica)
Exportação[1][2][3][4] é 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
[editar | editar código-fonte]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
[editar | editar código-fonte]Valores de verdade
[editar | editar código-fonte]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
[editar | editar código-fonte]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
[editar | editar código-fonte]A exportação é associada com "Currying" através da correspondência de Curry–Howard.
Referências
[editar | editar código-fonte]- ↑ Hurley, Patrick (1991). A Concise Introduction to Logic 4th edition. [S.l.]: Wadsworth Publishing. pp. 364–5
- ↑ Copi, Irving M.; Cohen, Carl (2005). Introduction to Logic. [S.l.]: Prentice Hall. p. 371
- ↑ Moore and Parker
- ↑ http://www.philosophypages.com/lg/e11b.htm