How is "$:=$" defined formally and why? "$\iff$", "$=$", ...?
- Anybody can ask a question
- Anybody can answer
- The best answers are voted up and rise to the top
There is no need of a formal definition of a definition. A definition is just an abbreviation. For example, in formal arithmetic (number theory) we write $x\mid y$ ($x$ divides $y$) as an abbreviation for $\exists z (y=x\times z)$. Whenever $s\mid t$ is used, it can be replaced in principle by the "long" form.
I do not know of any formal meaning of the definition symbol $:=$. I have not seen it used in mathematical logic (although I'm sure someone somewhere has used it in some formal system.)
In ordinary mathematics, the definition symbol has an informal meaning, namely to signal that the current sentence serves as a definition of what follows the symbol. Sometimes you can substitute $=$ for $:=$ and sometimes you can substitute $\iff$, so long as you add some words to make it clear that you are defining something.
For example, the sentence "$f(x) := x^2+1$" means "we define the function $f$ by $f(x) = x^2+1$" as opposed to "$f(x)$ turns out to equal $x^2+1$ even though the function $f$ was defined previously in some other way." And the sentence "$P(x) := x > 1$" could be used to mean "we define the property $P$ by $P(x) \iff x>1$.
I think it is usually better to use words rather than the $:=$ symbol to make it clear that you are defining something.