Eliminación del bicondicional
# Eliminación del bicondicional

La eliminación del bicondicional es el nombre de dos reglas de inferencia válidas de la lógica proposicional. Esto nos permite inferir un condicional de un bicondicional. Si $(P\leftrightarrow Q)$ es verdadero, entonces $(P\to Q)$ es verdadero y $(Q\to P)$ también lo será. Por ejemplo, si bien es cierto que estoy respirando si y sólo si estoy vivo, entonces es verdad que si estoy respirando, estoy vivo; Asimismo, es verdad que si estoy vivo, estoy respirando. Las reglas pueden ser establecidas formalmente como sigue:

    ${\frac {(P\leftrightarrow Q)}{\therefore (P\to Q)}}$

y

    ${\frac {(P\leftrightarrow Q)}{\therefore (Q\to P)}}$

donde la regla es que cada vez que una instancia "$(P\leftrightarrow Q)$" aparezca en una línea de prueba, tanto "$(P\to Q)$" como "$(Q\to P)$" puede colocarse en la línea siguiente;

## Notación formal

La regla de eliminación del bicondicional puede escribirse en notación subsiguiente:

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

y

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

donde $\vdash$ es el símbolo metalógico lo que significa que $(P\to Q)$ en el primer caso, y $(Q\to P)$ en otros son consecuencia sintáctica de $(P\leftrightarrow Q)$ en algún sistema lógico;

o como una declaración de verdadera tautología funcional o teorema de la lógica proposicional:

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

donde $P$ y $Q$ son proposiciones expresadas en algún sistema formal.

