Exportación (lógica)

, que a su vez implicaLa 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: dondees un símbolo metalógico significando queen 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.