Prove that two propositions $φ$ and $ψ$ are syntactically equivalent if and only if the proposition $φ↔ψ$ is a tautology

Question

$φ↔ψ$ is a tautology.

Does it mean $φ↔ψ$ is always true? If so, then we can derive $φ\rightarrowψ$ and $φ\leftarrowψ$. But we have to prove $φ⊢ψ$ and $ψ⊢φ$. What's the difference?

Answer 1

In propositional logic, we have that $\varphi \leftrightarrow \psi$ is a tautology (in symbols : $\vDash \varphi \leftrightarrow \psi$) iff it is true for every truth assignement.

We say that two formulas $\varphi$ and $\psi$ are syntactically equivalent iff $\varphi \leftrightarrow \psi$ is a theorem. In symbols : $\vdash \varphi \leftrightarrow \psi$

Thus, we have to "link" the semantical notion of tautology to the syntactical notion of theorem of the (propositional) calculus (Natural Deduction, Truth Trees, or other).

If we are working in Natural Deduction, the rule for $↔$-introduction allows use to conlcude with $\vdash \varphi \leftrightarrow \psi$ from :

$\vdash \varphi \rightarrow \psi$ and $\vdash \psi \rightarrow \varphi$.

Note: see Soundness and completeness of propositional calculus : $\vdash \sigma$ iff $\vDash \sigma$.