Definition:Provable Equivalence

Definition

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 if and only if:

$\phi \vdash_{\mathscr P} \psi$ and $\psi \vdash_{\mathscr P} \phi$

that is, if and only if 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$

Also see

• Definition:Provable Consequence

• Definition:Logical Equivalence
• Definition:Semantic Equivalence

Sources

• 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.2.4$: Provable equivalence: Definition $1.25$