# What does the symbol “:=” mean in formal logic?

:=

What does the "colon-equal symbol" mean, and how is it used?

## 2 Answers

Answer

According to Wikipedia's article on logic symbols, := is used for definition. The truth of a proposition can be determined through empirical or rational means, but sometimes it is assigned axiomatically:

p = q means there is an equivalence of values
p := q means that p is equivalent to q by definition, assignment, or declaration, such as when a mathematician declares something like 'Let p be assigned q', for example.

It has been my experience that the more traditional way to express definition is the use of '≡', but in computer science, since the colon and equal sign are standard on a QWERTY keyboard, it often gains usage because of its syntactic assignment as an assignment operator to avoid confusion with the operation that checks for equality.

Addendum:

As per comments below, note well that other notations such as '≜' and '≝' have been and continue to be used in literature to differentiate definition and equality. As the user mlk notes below, the orthography of ':=' is such that '=:' can be used to indciate that the definition occurs on the left. That is 'p =: q' specifies that q is the definiendum and p is the definiens.

• Another common notation is "≜". Unicode also includes "≝", but I have never seen it used. The symbol "≡" is also not too common in my experience, but it might be biased. – Yuval Filmus Oct 25 '20 at 14:11
• ":=" also has the added benefit that it is not symmetric, which is another reason why many people (including me) prefer it. It makes it a bit clearer which side is newly defined and which side keeps its meaning and it allows using the reverse "=:", which in rare situations can make something more readable. – mlk Oct 25 '20 at 15:07
• I've seen it (and use it myself sometimes) in mathematics and (American-style) theoretical computer science. Perhaps someone should do a survey of notations and figure out who uses what notation. – Yuval Filmus Oct 25 '20 at 15:15
• The ≡ symbol is troublesome in that there is one (older?) convention which treats it as stronger than = — for example f(x)≡g(x) would mean functions f and g are equal everywhere whereas f(x)=g(x) is only saying they're equal in one point — and there is a second (newer?) convention which treats it as weaker than = — notably in modular arithmetic, 2 ≡ 7 (mod 5). The Unicode character name IDENTICAL TO adheres to the former convention, but in my experience the latter is more common. – Lars H Oct 26 '20 at 12:32
• 'equal by definition' would imply 'identical to', but not necessarily vice versa, so it makes sense to have separate symbols. This is probably most apparent with logical equivalence (another use for ≡ in older texts), as is it quite common that two well-formed formulae can be logically equivalent without one being defined as the other — just take any two tautologies! – Lars H Oct 26 '20 at 12:44

It means, "is equal by definition to" or "is defined to be equal to".