This SEP article on definitions claims that the semantic and syntactic criteria it states for a valid definition are not equivalent. If we're working in standard first-order logic, I don't see how this could be. Could you help?
I've copied the relevant section below, with the claim highlighted:
Here's an attempted proof for the conservativeness criterion. Let $\Gamma \subseteq L$ be the theory under consideration, and $\Delta \subseteq L^+$ contain our definitions. Then:
- For all $\phi$ in $L$, if $\Gamma \cup \Delta \vdash \phi$ then $\Gamma \vdash \phi$ (Premise).
- Assume for an arbitrary $\phi$ in $L$ that $\Gamma \cup \Delta \models \phi$.
- Then, by strong completeness, $\Gamma \cup \Delta \vdash \phi$.
- From 1 and 3, $\Gamma \vdash \phi$.
- Then, by strong soundness, $\Gamma \models \phi$.
- From 2-5, if $\Gamma \cup \Delta \models \phi$ then $\Gamma \models \phi$.
- Thus, for all $\phi$ in $L$, if $\Gamma \cup \Delta \models \phi$ then $\Gamma \models \phi$.
The other direction is analogously proven to establish equivalence.
Similarly, a proof for the eliminability criterion can be generated:
- For all $\phi$ in $L^+$, there exists $\psi \in L$ such that $\Gamma \cup \Delta \vdash \phi \leftrightarrow \psi$ (Premise).
- Assume for an arbitrary $\phi$ in $L^+$ that some $\psi^* \in L$ is such that $\Gamma \cup \Delta \vdash \phi \leftrightarrow \psi^*$.
- Then, by string soundness, we have $\Gamma \cup \Delta \models \phi \leftrightarrow \psi^*$.
- Thus, for all $\phi$ in $L$ there exists $\psi \in L$ such that $\Gamma \cup \Delta \models \phi \leftrightarrow \psi$.
The other direction is analogously proven to establish equivalence.
I didn't figure it out but my best guess is that the difference is because the author assumes definitions are rules of inference, so adding them changes the deduction system. I instead assume they are non-logical axioms (not part of the deduction system), and adding them doesn't change the deduction system.