Exportación (lógica)

Exportación​​​​ es una regla de reemplazo válida de la lógica proposicional. La regla establece que si $P$ implica $Q$, que a su vez implica $R$, entonces $P$ y $Q$ implica $R$ y viceversa. La regla permite sustituir sentencias condicionales que tengan antecedentes conjuntivos por declaraciones que tienen consecuentes condicionales y viceversa en pruebas lógicas. Esta es la representación simbólica de la regla:

$((P\land Q)\to R)\Leftrightarrow (P\to (Q\to R))$

Donde "$\Leftrightarrow$" es un símbolo metalógico que representa "puede ser reemplazado en una demostración con"

Notación formal

La regla de exportación puede escribirse en la notación subsiguiente:

$((P\land Q)\to R)\vdash (P\to (Q\to R))$

donde $\vdash$ es un símbolo metalógico significando que $(P\to (Q\to R))$ es consecuencia sintáctica de $((P\land Q)\to R)$ en algún sistema lógico;

o en forma de regla:

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

donde la regla es que cada vez que en las líneas de una demostración aparezcan las instancias de "$(P\land Q)\to R$", éstas pueden ser reemplazadas con "$P\to (Q\to R)$";

$(P\to Q)\leftrightarrow (P\to (P\land Q))$

y expresado como una tautología o teorema de la lógica proposicional.

$((P\land Q)\to R))\to (P\to (Q\to R)))$

donde $P$, $Q$, y $R$ son proposiciones expresadas en algún sistema lógico.

Lenguaje natural

Valores de verdad

En todo momento si P→Q es cierto, puede ser reemplazado por P→(P∧Q).
Uno de los casos posibles para P→Q es para P es verdadero y Q es verdadero; por lo tanto P∧Q también es verdad y P→(P∧Q) es verdadero.
Otro caso posible establece como falso P y Q como verdadero. Por lo tanto, P∧Q es falso y P→(P∧Q) es falso; falso→falso es verdadero.
El último caso se produce cuando tanto P y Q son falsas. Por lo tanto, P∧Q es falso y P→(P∧Q) es verdadero.

Ejemplo

Que llueva y el sol brille implica que hay un arcoíris.
Por lo tanto, si llueve, entonces el sol brilla implica que hay un arcoíris.

Relación a funciones

La exportación está asociada a la Currificación mediante la correspondencia de Curry-Howard.

Enlaces externos

• Datos: Q5421567