Exportación (lógica)

Exportación[4]​ es una regla de reemplazo válida de la lógica proposicional. La regla establece que si implica , que a su vez implica , entonces y implica 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:

Donde "" 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:

donde es un símbolo metalógico significando que es consecuencia sintáctica de 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 "", éstas pueden ser reemplazadas con "";

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

donde , , y son proposiciones expresadas en algún sistema lógico.

Other Languages