Introducción bicondicional

En lógica proposicional , la introducción bicondicional ^{[1] [2] [3]} es una regla de inferencia válida . Permite inferir un bicondicional a partir de dos enunciados condicionales . La regla hace posible introducir un enunciado bicondicional en una prueba lógica . Si es verdadero, y si es verdadero, entonces se puede inferir que es verdadero. Por ejemplo, de los enunciados "si estoy respirando, entonces estoy vivo" y "si estoy vivo, entonces estoy respirando", se puede inferir que "estoy respirando si y solo si estoy vivo". La introducción bicondicional es la inversa de la eliminación bicondicional . La regla se puede enunciar formalmente como: ${\displaystyle P\to Q}$${\displaystyle Q\to P}$${\displaystyle P\leftrightarrow Q}$

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

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

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

${\displaystyle (P\to Q),(Q\to P)\vdash (P\leftrightarrow Q)}$

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

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

${\displaystyle ((P\to Q)\land (Q\to P))\to (P\leftrightarrow Q)}$

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