\begin{definition}[Definition:Provable Equivalence]
Let $\mathscr P$ be a proof system for a formal language $\LL$.
Let $\phi, \psi$ be $\LL$-WFFs.
Then $\phi$ and $\psi$ are '''$\mathscr P$-provably equivalent''' {{iff}}:
:$\phi \vdash_{\mathscr P} \psi$ and $\psi \vdash_{\mathscr P} \phi$
that is, {{iff}} they are $\mathscr P$-provable consequences of one another.
The '''provable equivalence''' of $\phi$ and $\psi$ can be denoted by:
:$\phi \dashv \vdash_{\mathscr P} \psi$
\end{definition}