Introducción del bicondicional

La introducción del bicondicional[1][2][3] es una regla de inferencia válida en lógica proposicional. Permite inferir un bicondicional a partir de dos sentencias condicionales. En otras palabras, esta regla permite introducir un enunciado bicondicional en una prueba lógica. Si ${\displaystyle P\to Q}$ es verdad, y si ${\displaystyle Q\to P}$ es verdad, entonces se puede inferir que ${\displaystyle P\leftrightarrow Q}$ es verdad. La introducción del bicondicional es la conversión de la eliminación del bicondicional.

Por ejemplo, de las declaraciones "si estoy respirando, entonces yo estoy vivo" y "si estoy vivo, entonces estoy respirando", se puede inferir que "estoy respirando si y sólo si estoy vivo".

La introducción del bicondicional puede escribirse formalmente como:

${\displaystyle {\frac {P\to Q,Q\to P}{\therefore P\leftrightarrow Q}}}$

donde la regla es que siempre que las instancias de "${\displaystyle P\to Q}$" y "${\displaystyle Q\to P}$" aparecen en las líneas de una prueba, "${\displaystyle P\leftrightarrow Q}$" puede ser colocado válidamente en una línea posterior.