# How do you define definition symbol :=?

How is "$:=$" defined formally and why? "$\iff$", "$=$", ...?

-
:= := :=, if you know what I mean. ;-) –  Parth Kohli May 24 '13 at 5:35
After reading the answers I have arrived at a conclusion. Please tell me what you think about it. First of all ":=" is a symbol of the language. Hence the rules to use it are given in metalogic. I can think of: $\alpha := \beta \Longleftrightarrow \alpha \longleftrightarrow \beta$ if $\alpha$ and $\beta$ are formulas, and $\alpha := \beta \Longleftrightarrow \alpha = \beta$ if $\alpha$ and $\beta$ are terms in the language. –  Daniela Diaz May 24 '13 at 16:12

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.

-
Does is mean that it is a metamathical concept? –  Daniela Diaz May 24 '13 at 5:55
what about $\exists !x (\phi (x))$ then $Tip=:x$? –  Daniela Diaz May 24 '13 at 6:08
In my answer above, I deliberately simplified to make a point. One can extend a language "by definition." Every so often in formal logic, the notion is useful. –  André Nicolas May 24 '13 at 13:30
Thank you so much for your answer. Although this doesn't answer my quesion directly this guided me to find my answer: en.wikipedia.org/wiki/Extension_by_definitions –  Daniela Diaz Jun 23 '13 at 0:56
In a more general sense: en.wikipedia.org/wiki/Conservative_extension –  Daniela Diaz Jun 23 '13 at 0:56

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.

-