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 $(P\leftrightarrow Q)$ é verdadeiro, logo $(P\to Q)$ é verdadeiro, e $(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:

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

e

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

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

Notação formal

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

$(P\leftrightarrow Q)⊢(P\to Q)$

e

$(P\leftrightarrow Q)⊢(Q\to P)$

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

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

$(P\leftrightarrow Q)\to (P\to Q)$

$(P\leftrightarrow Q)\to (Q\to P)$

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