Difference between $:=$ and $=$

I am sorry if this is quite elementary question. But I always think, that why we use $:=$ at some places, instead of $=$. Is there any fundamental difference between these two? Before reading Terry Tao's blog (4 months ago), I had never seen a symbol like this (:=).

Solution 1:

Some authors like to distinguish the assertion "A is equal to B" from "define A as an object equal to B".

In math, the first one is always $A=B$ (I've never seen anything else, at least). But for definitions, I've seen

1. $A \triangleq B$
2. $A \equiv B$
3. $A \stackrel{\mathrm{def}}{=} B$
4. $A := B$

Often the triple equal sign is used for strong notions of equivalence (such as in binary relations) or with the "mod" symbol.

In computer programming, we are typographically limited of course. The assignment operator is usually distinguished from the comparison operator, and this is done in different ways depending on the language. For example in Pascal you assign x := 5 and compare x = 5. However in C you assign x = 5 and compare x == 5. (It should be noted that in C this syntax has caused untold confusion and a few famous bugs.)

My favorite (meaning "most awful") example is in PHP and javascript where one can do a "strict compare" with x === 5. Finally, some languages have ridiculous vagaries like distinguishing which comparision operator is used based on the type of variable (usually strings being different from numerics), with syntaxes like .eq. and related.

Solution 2:

The notation := was used in some early programming languages. The meaning of x := 3 was "assign 3 to the variable x". So, the assignment could be distinguished from the the test if (x = 3) .... In mathematics the obvious meaning is "Let x be 3".

Modern programming languages use x = 3 for the assignment, and == for the equality test if (x == 3) ....

Solution 3:

The equality symbol = denotes an operator that is part of the object theory. The definition symbol $\triangleq$ (and its variants) denotes a syntactic replacement, and is part of the metatheory.

This distinction is emphasized in the formal syntax of TLA+, whose axioms are those of Zermelo-Fraenkel set theory + Hilbert's $\varepsilon$, and functions. The theory has some axiom schemata for equality, as is usually the case with theories that include equality. In order to refer to symbols, they first have to be declared. For example:

CONSTANT a
VARIABLE x

THEOREM (a \in 1..2 /\ x = a) => (x \in 1..2)

Symbol a is declared to be a constant, and x as a variable (constants stay unchanged though a behavior, variables can change). The above theorem holds due to the indiscernibility of identicals (i.e., equal things "look the same").

A symbol can be defined, instead of declared. For example:

CONSTANTS a, b

Foo == a \/ b

The symbol Foo literally stands for a \/ b. The definition symbol == (typeset as $\triangleq$) is not an operator of the object theory, as \in, =, +, and other symbols are. It is metatheoretic notation that says that the string Foo abbreviates the expression a \/ b. So wherever Foo appears later, it is syntactically replaced by the expression a \/ b before any reasoning takes place.

Interestingly, there is another way of writing the last example:

CONSTANTS a, b

CONSTANT Foo
AXIOM Foo = (a \/ b)

What we have done is declare the identifier Foo as a constant, so some value in the object theory (here some set), and added an axiom that it so happens that the value of Foo is the same as the value of a \/ b (\/ denotes disjunction).

A defined symbol can be formally understood as shorthand for an extension by definition. The last example resembles an extension by definition that would correspond to the middle example. A clear introduction to the concept of extending a theory with definitions is given in Kunen's "Foundations of mathematics", Sec. II.15 on pages 148--152.

The theorem prover TLAPS has several examples of how definitions and declarations are used in its library of modules.

As a side note, $a \equiv b$ in TLA+ means $(a \in \mathrm{BOOLEAN}) \wedge (b \in \mathrm{BOOLEAN}) \wedge (a = b)$, and := means assignment in the algorithm language PlusCal, which translates to TLA+.