biconditional-introduction (math concept)
See also
python declaration class | python inclusion class | python sample
Definition
biconditional-introduction is the inference-rule:
\[\left( \left( \boldsymbol{P} \implies \mathbf{Q} \right), \left( \mathbf{Q} \implies \boldsymbol{P} \right) \right) \vdash \left( \mathbf{Q} \iff P \right)\]
Where:
\(\boldsymbol{P} \implies \mathbf{Q}\) is a formula-statement
\(\mathbf{Q} \implies \boldsymbol{P}\) is a formula-statement
\(\boldsymbol{P}\) is a propositional formula
\(\mathbf{Q}\) is a propositional formula
In straightforward language, if \(\mathbf{Q}\) follows from \(\boldsymbol{P}\) and \(\boldsymbol{P}\) follows from \(\mathbf{Q}\), it follows that \(\boldsymbol{P}\) is true if and only if \(\mathbf{Q}\) is true.
Sources
[War18, p. 114]