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?

  • 3
    $\begingroup$ 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. $\endgroup$
    – Kuba
    Oct 6, 2015 at 10:20
  • $\begingroup$ 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?? $\endgroup$
    – skyfire
    Oct 6, 2015 at 10:22
  • $\begingroup$ 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. $\endgroup$
    – skyfire
    Oct 6, 2015 at 10:27
  • $\begingroup$ 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)$. $\endgroup$ Oct 6, 2015 at 12:54

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


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .