Q:

Confusing symbol in papers on hybrid logic

In literature about hybrid logic I'm reading for my thesis I've come across the following symbol:
::=

Now, I've never seen this notation before. I can also not find it explained anywhere (for instance here). Mostly I've worked under the assumption it is equal to $:=$, which its usage seems to suggest. Am I correct in assuming that $::= \ \equiv  \ :=$ (talk about a nicely confusing formulation...).
Since the concepts of hybrid logic are not the main focus of the thesis, but its explanation and correctness of fundamental importance I wan't to make sure I'm understanding everything correctly.
Also note that it is NOT a typo, as I've seen it on more than one occasion, in different papers on the subject.

A:

Yes, $:=$ and $::=$ have similar meanings. A lot of times that notation is used to mean "equal by definition or by stipulation". So for instance, you might say, "Define the formula $\varphi ::= \forall x \exists y R(x,y)$," or you might say, "Let "$\varphi \vee \psi$" be an abbreviation for "$\neg (\neg\varphi \wedge \neg\psi)$", i.e. let $\varphi \vee \psi ::= \neg(\neg\varphi \wedge \neg\psi)$." You wouldn't say "Therefore, $(x^2 + 1) ::= y^4$", since if there is an equality involved in this case, it's not really equality by stipulation or definition, but rather some derived equality. You can basically read it as "is equal to" but it's more emphatic, in that it's equality by definition or stipulation, rather than some derived equality.

