Exportación (lógica)

La exportación ^{[ 1 ] [ 2 ] [ 3 ] [ 4 ]} es una regla válida de reemplazo en lógica proposicional . Esta regla permite reemplazar enunciados condicionales con antecedentes conjuntivos por enunciados con consecuentes condicionales y viceversa en demostraciones lógicas . La regla establece que:

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

Dónde "${\displaystyle \Leftrightarrow }$" es un símbolo metalógico que representa "puede ser reemplazado en una prueba por". En terminología estricta,${\displaystyle ((P\land Q)\to R)\Rightarrow (P\to (Q\to R))}$es la ley de exportación, porque "exporta" una proposición del antecedente de${\displaystyle (P\land Q)\to R}$a su consecuente. Su recíproco, la ley de importación ,${\displaystyle (P\to (Q\to R))\Rightarrow ((P\land Q)\to R)}$, "importa" una proposición del consecuente de${\displaystyle P\to (Q\to R)}$a su antecedente.

La regla de exportación puede escribirse en notación secuencial :

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

dónde${\displaystyle \dashv \vdash }$es un símbolo metalógico que significa que${\displaystyle (P\to (Q\to R))}$es un equivalente sintáctico de${\displaystyle ((P\land Q)\to R)}$en algún sistema lógico ;

o en forma de regla :

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

donde la regla es que dondequiera que haya una instancia de "${\displaystyle (P\land Q)\to R}$" aparece en una línea de una prueba, puede ser reemplazado por "${\displaystyle P\to (Q\to R)}$", y viceversa.

Importación-exportación es un nombre que se le da a la afirmación como un teorema o tautología veritativo-funcional de la lógica proposicional:

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

dónde${\displaystyle P}$,${\displaystyle Q}$, y${\displaystyle R}$son proposiciones expresadas en algún sistema lógico .

La siguiente demostración utiliza una cadena de equivalencias clásicamente válida. Las reglas utilizadas son la implicación material , la ley de De Morgan y la propiedad asociativa de la disyunción .

Debido al uso de la implicación material en los dos primeros pasos, esta no es una prueba válida desde un punto de vista intuicionista.

La exportación está asociada con el curry a través de la correspondencia Curry-Howard .