Biconditional

Define

A binary logical connective, denoted

\[\begin{equation*}
  P \iff Q \qor P \equiv Q,
\end{equation*}
\]

and read

that is ‘true’ if and only if

which is equivalent to

\[\begin{equation*}
  (P \implies Q) \> \land \> (Q \implies P).
\end{equation*}
\]

(Levin, 2021, sec. 0.2; Poole & Mackworth, 2017, sec. 5.1)

Name

• Logical equivalence
• Equivalence
• If and only if
• Iff

Explore

Construct the truth table for the statement

\[\begin{align*}
  P \iff Q \>
  & \equiv \> (P \implies Q) \land (Q \implies P) \\
  & \equiv \> (\lnot P \lor Q) \land (\lnot Q \lor P).
\end{align*}
\]

<<scheme/org-truth-table>>
(org-truth-table (lambda (p q)
                   (and (or (not p) q)
                        (or (not q) p)))
                 '("P" "Q"
                   "P \\iff Q"))