title: Exportación (lógica)
text: # 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.
  
  