Why aren't definitions well formed formulas?

Question

Why aren't definitions well formed formulas? For instance, the definition of an additive inverse is: "Let $x \in \Bbb Z$. Then the additive inverse of $x$ is $y \in \Bbb Z$ such that $x+y=0$".

Why not just say "there is $y \in \Bbb Z$ such that $\forall x, \ x+y=0$. This $y$ is the additive inverse of $x$"?

The bigger issue seems to me that every step in a proof needs to be a complete sentence (i.e. a well formed formula) but a definition does not seem to do that? Why? And is my own definition of additive inverse equivalent?

Answer 1

In a formal treatment of a mathematical theory, definitions are well formed formulae.

See Theory of definitions and Semantics and Logical structure in Definitons.

A definition in the first order language of arithmetic (with : $0, S, +, \times$) introduces a new symbol, like :

$1$ (a constant), or

$\le$ (a binary predicate).

We can define $\le$ with the formula :

$x \le y \leftrightarrow \exists z (y=x+z)$.