En lógica proposicional , la introducción bicondicional [1] [2] [3] es una regla de inferencia válida . Permite a uno inferir un bicondicional a partir de dos enunciados condicionales . La regla permite introducir un enunciado bicondicional en una demostración lógica . Si es cierto, y si es cierto, entonces se puede inferir que 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 solo si ' estoy vivo ". Introducción Bicondicional es el inverso de eliminación bicondicional . La regla se puede enunciar formalmente como:
donde la regla es que siempre que los casos de "" y ""aparecen en las líneas de una prueba","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 :
dónde es un símbolo metalogico que significa quees una consecuencia sintáctica cuando y están ambos en una prueba;
o como el enunciado de una tautología funcional de verdad o teorema de lógica proposicional:
dónde , y son proposiciones expresadas en algún sistema formal .