A Theory Entailing a Logical Equivalence of Two Formulas in FOL In FOL we say two formulas $\phi$ and $\psi$ are logically equivalent iff  $\phi\vDash\psi$ and $\psi\vDash\phi$. 
My question is: What does it mean to say that a theory $T$ entails that $\phi$ and $\psi$ are logically equivalent? $T \vDash (\phi\vDash\psi \text{ and } \psi\vDash\phi)$
Can we say it means $T, \phi\vDash\psi$ and $T, \psi\vDash\phi$?
 A: Your last line is right: "$\varphi$ and $\psi$ are $T$-equivalent" (which I think is the clearest way to phrase it in natural language) means "$T,\varphi\models\psi$ and $T,\psi\models\varphi$." 
(Meanwhile, "$T\models (\varphi\models\psi \wedge\psi\models\varphi)$" doesn't actually mean anything - we can't "iterate $\models$.")
However, there are a couple other (equivalent) ways to formulate this:


*

*By the completeness theorem, that's equivalent to "$T,\varphi\vdash\psi$ and $T,\psi\vdash\varphi$" - that is, we can replace semantic entailment with proof.

*By the deduction theorem, that's equivalent to "$T\vdash\varphi\leftrightarrow\psi$."

*The deduction theorem also has a (much simpler to prove) semantic counterpart: it's easy to show that $T,\theta\models\eta$ iff $T\models\theta\rightarrow \eta$, and it follows that ($T,\theta\models\eta$ and $T,\eta\models\theta$) iff $T\models\theta\leftrightarrow\eta$. So finally, yet another equivalent way to express "$\varphi$ and $\psi$ are $T$-equivalent" - and in my opinion the snappiest really - is $$"T\models\varphi\leftrightarrow\psi."$$ Indeed,it's this last one that I consider the definition of "$\varphi$ and $\psi$ are $T$-equivalent," and I'd consider the equivalences with the other three versions to be (easily proved) theorems.
