Introducción del bicondicional
# Introducción del bicondicional

La introducción del bicondicional 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 $P\to Q$ es verdad, y si $Q\to P$ es verdad, entonces se puede inferir que $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:

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

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

## Notación formal

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

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

donde $\vdash$ es un símbolo metalógico lo que significa que $P\leftrightarrow Q$ es una consecuencia sintáctica cuando $P\to Q$ y $Q\to P$ están ambos en una prueba;

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

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

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

