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á.^[1] 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;