, que a su vez implica
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:
" es un símbolo metalógico que representa "puede ser reemplazado en una demostración con" La regla de exportación puede escribirse en la notación subsiguiente: donde
es un símbolo metalógico significando que
en algún sistema lógico; o en forma de regla: donde la regla es que cada vez que en las líneas de una demostración aparezcan las instancias de "
"; y expresado como una tautología o teorema de la lógica proposicional.
son proposiciones expresadas en algún sistema lógico.
Otro caso posible establece como falso P y Q como verdadero.
El último caso se produce cuando tanto P y Q son falsas.
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.
La exportación está asociada a la Currificación mediante la correspondencia de Curry-Howard.