Eliminação bicondicional

Eliminação bicondicional são duas regras de inferência validas da lógica proposicional. Ela permite inferir um condicional de um bicondicional. Se ${\displaystyle (P\leftrightarrow Q)}$ é verdadeiro,^[1] logo ${\displaystyle (P\to Q)}$ é verdadeiro, e ${\displaystyle (Q\to P)}$ também será. Por exemplo, se é verdade que eu estou respirando se e somente se estou vivo, então é verdade que se estou respirando, estou vivo; Igualmente, é verdade que se estou vivo, estou respirando. As regras podem ser estabelecidas formalmente como mostrado a seguir:

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

e

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

Onde a regra é que sempre que uma instância de "${\displaystyle (P\leftrightarrow Q)}$" aparecer em uma linha da prova, ambos "${\displaystyle (P\to Q)}$" ou "${\displaystyle (Q\to P)}$" podem ser colocados na linha subsequente;

A regra da eliminação bicondicional pode ser escrita na notação de sequentes:

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

e

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

onde ${\displaystyle \vdash }$ é o símbolo da metalógica que significa que ${\displaystyle (P\to Q)}$, no primeiro caso, e ${\displaystyle (Q\to P)}$ nos outros são consequência sintática de ${\displaystyle (P\leftrightarrow Q)}$ em algum sistema lógica;

ou como a afirmação da verdade funcional tautologia ou teorema da lógica proposicional:

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

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

onde ${\displaystyle P}$, e ${\displaystyle Q}$ são proposições expressas em algum sistema formal.

Referências