Logical equivalence of two expressions Suppose one is transforming the first order logic formula
$\exists x(\phi(x))$
into
$\phi(a)$
by Skolemization, where $a$ is a fresh constant.
I understand that this preserves consistency, i.e. if the first expression is true in at least one case then the second expression is also true in at least one case, but it does not necessarily preserve validity or satisfiability.
The question I am asking is are these two expressions logically equivalent? What is the definition of logical equivalence and what properties must be maintained for logical equivalence to hold?
I am not sure, but I think logical equivalence is equivalent to $\leftrightarrow$ in that if $\exists x(\phi(x))\leftrightarrow\phi(a)$ then the two expressions are logically equivalent. In which case these two expressions are logically equivalent. Is this reasoning correct?
With many thanks,
Froskoy.
 A: 
$\exists \phi(x), \quad  \phi(a),\quad$ where $a$ is a fresh constant. 

The question I am asking is are these two expressions logically equivalent? 
That is, it it the case that: $\exists x(\phi(x))\leftrightarrow\phi(a)\;$?

As Peter mentions, the two expressions are not logically equivalent in either the proof-theoretic or the semantic sense. To better illustrate why not:
Consider the following interpretation, e.g., suppose $x\in \mathbb{Z}$ and $a = 1 \in \mathbb{Z}$. Suppose $\varphi(x)$ denotes "$x$ is even". Then $\exists x \varphi(x)$ is true, but $\varphi(a)$ is false, under this interpretation: It is true that even numbers exist, but it is false that a is even. Hence, $\exists x(\phi(x)) \leftrightarrow \phi(a)$ is not true, in this interpretation, hence not true in all interpretations.

What is the definition of logical equivalence and what properties must be maintained for logical equivalence to hold?

The precise answer to this depends on whether you are asking for the definition of logical equivalence in the proof-theoretic sense, or the semantic sense, or both. 
A: No, the two expressions are not logically equivalent in either the proof-theoretic or the semantic sense (and indeed, you indicate the reasons yourself).


*

*You cannot deduce $\varphi(a)$ from $\exists x\varphi(x)$ (and note $\exists x(\phi(x))\leftrightarrow\phi(a)$ is not a theorem of first-order logic).

*There are interpretations which make $\exists x\varphi(x)$ true and $\varphi(a)$ false (and so $\exists x(\phi(x))\leftrightarrow\phi(a)$ is not true on all interpretations).

