A question about definitions and also notation, illustrated with a trivial example:
Let $a,b,c\in\mathbb{N}$ and
$$a:=2,$$
and
$$b:=1$$
I postulate the the following formula holds
$$2c=6a+4b.$$
Now I can conclude that "$c=8$".
Why would I write $c=8$ and not $c:=8$? This expression seems to be a question of the history of the derivation, which the mathematican did, why is this encoded in the notation?
What is the nature of the definition symbol (it doesn't have to be "$:=$", it could be any addition notation for definition, which live besides "$=$")?
Is a definition symbol reecomended of needed? Would it be the exact same thing if I'd always use "$=$", i.e. in the above example define "$a=2$", "$b=1$"?
I think the symbol := is meant to be a form of an "assignment operator," which you might encounter in programming. This appears to be happening for the symbols $a$ and $b$ above. In the formula you seem to be asking, "Is 2c = 6a + 4b?"
In C family languages, the equals sign is really an assignment of a quantity to a symbol. The double-equals sign
==is the isequalto operator. If you write this in Cthen
2*c = 6*a + 4*bwould evaluate to
false, werecto be holding the value 8.