# Why aren't definitions well formed formulas?

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?

• Wait, did you just say "there is an integer y such that for any x, x+y=0"? You should take a look at that.
– Kuba
Oct 6, 2015 at 10:20
• Yeah I know -just pick y=-x :/ guess I overlooked that. So definitions cannot be complete sentences, but why? Where in the name of logic permits this?? Oct 6, 2015 at 10:22
• Is the definition simply "for any y, y is an additive inverse iff for every x, x+y=0"? Suppose that makes a complete sentence. Oct 6, 2015 at 10:27
• Regarding your example, you are (quite) right : we have to define a (binary) predicate : $Add_i(x,y) \leftrightarrow (x+y=0)$. In order to say "the additive inverse of $x$" we have to prove uniqueness (i.e. $\forall y_1 \forall y_2 [Add_i(x,y_1) \land Add_i(x,y_2) \to y_1=y_2]$. If so, we can introduce a new function symbol $A_i(x) = y \leftrightarrow Add_i(x,y)$. Oct 6, 2015 at 12:54

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)$$.