This question is for the propositional normal modal logic system K (although it may apply to other logics too).
I saw a couple of papers which mentioned algebraic equivalence of modal logic formulas without defining it, or referring to "two modal formulas that are provably-equivalent", i.e. $\phi$ equivalent to $\psi$ means $\vdash_K\phi$ iff $\vdash_K\psi$. But I see a problem here in that any two non-theorems would then be algebraically equivalent, which I don't believe is the intent.
So I'm thinking it may be defined as $\phi$ algebraically equivalent to $\psi$ iff $\vdash_K (\phi\leftrightarrow\psi)$, which means both $\vdash _K(\phi\rightarrow\psi)$ and $\vdash_K (\psi\rightarrow\phi)$. Then if $\vdash_K\phi$ by modus ponens $\vdash_K\psi$ and vice-versa, which seems to be the intent. This would also allow for (only) suitable pairs of non-theorems to be algebraically equivalent formulas.
Is this correct? If not, then what is the exact definition of algebraic equivalence between formulas in K?
And b.t.w., what would be the math symbol to use for algebraic equivalence? I cannot use = because some texts use = instead of $\leftrightarrow$ inside the very formulas. And I cannot use ~ because some texts use ~ for negation. (For example, Hughes and Cresswell.)
"$\phi$ is provably equivalent to $\psi$" in some logical system $K$ means that $\phi \vdash_K \psi$ and $\psi \vdash_K \phi$. If $K$ comes equipped with the usual notion of bi-implication ($\leftrightarrow$), then this will be the same as $\vdash_K \phi \leftrightarrow \psi$. I would write this as "$\phi \mathrel{\dashv\vdash}_K \psi$" (and rather illogically read this out as "$\phi$ and $\psi$ are equiprovable", even though that suggests the unintended reading that "$\vdash_K \phi$ iff $\vdash_K \psi$").