Contradiction Characterization of Equivalence (Propositional Logic)

Definition

Contradiction Characterization of Equivalence (Propositional Logic)

Two formulas $P$ and $Q$ are equivalent if and only if the negation of their biconditional, $\neg (P\leftrightarrow Q)$, is unsatisfiable:

$$P\equiv Q⟺\neg (P\leftrightarrow Q)\text{ unsatisfiable}.$$

Reason

Two dualities composed

By the biconditional characterization, $P\equiv Q$ holds exactly when $P\leftrightarrow Q$ is valid; by the validity–unsatisfiability duality, that holds exactly when $\neg (P\leftrightarrow Q)$ is unsatisfiable:

$$P\equiv Q⟺(P\leftrightarrow Q)\text{ valid}⟺\neg (P\leftrightarrow Q)\text{ unsatisfiable}.$$