eliminación bicondicional

La eliminación bicondicional es el nombre de dos reglas válidas de inferencia de la lógica proposicional . Permite inferir una condicional a partir de una bicondicional . Si${\displaystyle P\leftrightarrow Q}$Si es cierto, entonces se puede inferir que${\displaystyle P\to Q}$es cierto, y también que${\displaystyle Q\to P}$es cierto. ^{[ 1 ]} Por ejemplo, si es cierto que respiro si y solo si estoy vivo, entonces es cierto que si respiro, estoy vivo; de igual modo, es cierto que si estoy vivo, respiro. Las reglas se pueden enunciar formalmente como:

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

y

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

donde la regla es que dondequiera que haya una instancia de "${\displaystyle P\leftrightarrow Q}$" aparece en una línea de una prueba, ya sea "${\displaystyle P\to Q}$" o "${\displaystyle Q\to P}$" puede colocarse en una línea posterior.

La regla de eliminación bicondicional puede escribirse en notación de secuencias :

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

y

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

dónde${\displaystyle \vdash }$es un símbolo metalógico que significa que${\displaystyle P\to Q}$, en el primer caso, y${\displaystyle Q\to P}$en el otro son consecuencias sintácticas de${\displaystyle P\leftrightarrow Q}$en algún sistema lógico ;

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

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

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

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

• bicondicional lógico