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 ${\displaystyle P\to Q}$ é verdade, e se ${\displaystyle Q\to P}$ é verdade, então pode-se inferir que ${\displaystyle 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:

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

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

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

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

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

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

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

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