Eliminación del bicondicional

Plantilla:Reglas de transformación 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:

$\begin{array}{cc}& P\leftrightarrow Q\\ \therefore & P\to Q\end{array}$

y

$\begin{array}{cc}& P\leftrightarrow Q\\ \therefore & Q\to P\end{array}$

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)⊢(P\to Q)$

y

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

donde $⊢$ 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.