Introducción bicondicional

En lógica proposicional, introducción bicondicional es una regla válida de inferencia. Permite a uno inferir un bicondicional de dos declaraciones condicionales. La regla permite introducir una declaración bicondicional en una prueba lógica. Si ${displaystyle Pto Q}$ es verdad, y si ${displaystyle Qto P}$ es cierto, entonces uno puede inferir que ${displaystyle Pleftrightarrow Q}$ es verdad. Por ejemplo, de las declaraciones "si estoy respirando, entonces 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 bicondicional es el contrario de la eliminación bicondicional. The rule can be stated formally as:

${displaystyle {frac {to Qto Qto P}{therefore Pleftrightarrow Q}}$

donde la regla es que dondequiera que sean instancias de "${displaystyle Pto Q}$"y"${displaystyle Qto P}$"parecen en líneas de una prueba, "${displaystyle Pleftrightarrow Q}$" se puede colocar válidamente en una línea posterior.

Notación formal

La regla de introducción bicondicional se puede escribir en notación secuencial:

${displaystyle (Pto Q),(Qto P)vdash (Pleftrightarrow Q)}$

Donde ${displaystyle vdash }$ es un símbolo metalógico que significa que ${displaystyle Pleftrightarrow Q}$ es una consecuencia sintáctica cuando ${displaystyle Pto Q}$ y ${displaystyle Qto P}$ ambos están en una prueba;

o como el enunciado de una tautología funcional veritativa o teorema de lógica proposicional:

${displaystyle (Pto Q)land (Qto P))to (Pleftrightarrow Q)}$

Donde ${displaystyle P}$, y ${displaystyle Q}$ son propuestas expresadas en algún sistema formal.