Introdução bicondicional

Em lógica proposicional, introdução bicondicional é uma regra de inferência válida. Ele permite inferir uma bicondicional de duas declarações condicionais. A regra torna possível introduzir uma declaração bicondicional em uma prova lógica. Se $P\to Q$ é verdade, e se $Q\to P$ é verdade, então pode-se inferir que $P\leftrightarrow Q$ é verdade. Por exemplo, da declaração "se eu estou respirando, então eu estou vivo" e "se eu estou vivo, então eu estou respirando", pode-se inferir que "eu estou respirando se e somente se eu estiver vivo". Introdução bicondicional é o inverso de eliminação bicondicional. A regra pode ser indicada formalmente como:

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

onde a regra é que sempre que as instâncias de "$P\to Q$" e "$Q\to P$" aparecer nas linhas de prova, "$P\leftrightarrow Q$" pode substituí-la na linha seguinte.

Notação formal

A regra da introdução bicondicional pode ser escrita em notação sequente:

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

onde $⊢$ é um símbolo da metateoria da lógica que significa que $P\leftrightarrow Q$ é um acarretamento quando $P\to Q$ e $Q\to P$ estão ambos em uma prova;

ou como uma declaração de uma verdade tautologica ou teorema da lógica proposicional:

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

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