Exportação (lógica) - Exportation (logic)

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

${\ displaystyle ((P \ land Q) \ to R) \ Leftrightarrow (P \ to (Q \ to R))}$

Onde " " é um símbolo metalógico que representa "pode ser substituído em uma prova por." ${\ displaystyle \ Leftrightarrow}$

Notação formal

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

{\ displaystyle ((P \ land Q) \ to R) \ dashv \ vdash (P \ to (Q \ to R))}

onde é um símbolo metalógica o que significa que é um equivalente sintático de em algum sistema lógico ; ${\ displaystyle \ dashv \ vdash}$ ${\ displaystyle (P \ to (Q \ to R))}$ ${\ displaystyle ((P \ land Q) \ to R)}$

ou em forma de regra :

{\ displaystyle {\ frac {(P \ land Q) \ to R} {P \ to (Q \ to R)}}}

,

{\ displaystyle {\ frac {P \ to (Q \ to R)} {(P \ land Q) \ to R}}.}

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

ou como a declaração de uma tautologia funcional de verdade ou teorema da lógica proposicional:

{\ displaystyle ((P \ land Q) \ to R) \ leftrightarrow (P \ to (Q \ to R))}

onde , e são proposições expressas em algum sistema lógico . ${\ displaystyle P}$ ${\ displaystyle Q}$ ${\ displaystyle R}$

Linguagem natural

Valores verdadeiros

A qualquer momento, se P → Q for verdadeiro, ele pode ser substituído por P → (P∧Q).
Um caso possível para P → Q é que P seja verdadeiro e Q seja verdadeiro; assim, P∧Q também é verdadeiro, e P → (P∧Q) é verdadeiro.
Outro caso possível define P como falso e Q como verdadeiro. Assim, P∧Q é falso e P → (P∧Q) é falso; falso → falso é verdadeiro.
O último caso ocorre quando P e Q são falsos. Assim, P∧Q é falso e P → (P∧Q) é verdadeiro.

Exemplo

Chove e o sol brilha indica que existe um arco-íris.
Assim, se chover, o sol brilhar significa que existe um arco-íris.

Se meu carro estiver ligado, quando mudo para D, o carro começa a andar. Se meu carro estiver ligado e eu mudei a marcha para D, o carro deve começar a andar.

Prova

A prova a seguir usa Implicação Material , negação dupla , Leis de De Morgan , a negação da declaração condicional, a propriedade associativa da conjunção, a negação de outra declaração condicional e negação dupla novamente, nessa ordem para derivar o resultado.


Proposição	Derivação
${\ displaystyle P \ rightarrow (Q \ rightarrow R)}$	Dado
${\ displaystyle \ neg P \ lor (Q \ rightarrow R)}$	Implicação material
${\ displaystyle \ neg P \ lor (\ neg Q \ lor R)}$	Implicação material
${\ displaystyle (\ neg P \ lor \ neg Q) \ lor R}$	Associatividade
${\ displaystyle \ neg (P \ land Q) \ lor R}$	Lei de Morgan
${\ displaystyle (P \ land Q) \ rightarrow R}$	Implicação material