Definition:Provable Equivalence

From ProofWiki
Jump to: navigation, search

Definition

Let $\mathcal P$ be a proof system for a formal language $\mathcal L$.

Let $\phi, \psi$ be $\mathcal L$-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



Sources