# “Defined as” versus “Equivalent to”

This is a lazy question, but very often textbooks use the "$\equiv$" (equivalent to) sign and the "$:=$" (defined as) sign in the same places from book to book. I suppose equivalence to a previously defined concept is also a form of definition. Any rules/guidelines as to when to use which?

Related to this query, suppose I wished to indicate that a particular variable had a particular property without defining a set and using the inclusion "$\in$" notation - so, for example, if $A$ is a circle, I might want to write $A\equiv\bigcirc$" where $\bigcirc$ is somehow shorthand for the property of roundness. I know it sounds convoluted, but I am happy to elaborate my context if someone is interested. In particular, this sort of shorthand works well where a generic set definition is not easy to write.

Thanks.

-
If you will provide a bit more context I will be glad to give it a try. But first, do explain - how does that relate to set theory? –  Asaf Karagila Jun 22 '11 at 11:58
Nope, no set theory - will edit to fix. :) –  Praetoria Jun 22 '11 at 12:06
It would help if you supplied further context. Usually $:=$ denotes some form of parameter binding (not only for naming variables but also functions and higher-order objects). Rarely in mathematics is there any rigorous presentation of the denotation of such binding mechanisms. For that see e.g. the theory of denotational semantics of programming languages. On the other hand $\equiv$ is a much more overloaded symbol. For example, it can denote an arbitrary equivalence relation. It's denotation is highly context dependent. –  Bill Dubuque Jun 22 '11 at 16:23
@Bill, thanks for your reply. The terms you use are unfamiliar to me. Maybe something simple I can read to understand, say, what a "binding mechanism" is? I think I understand what you mean though. So here is the context - I can't promise it won't be confusing. Like one of the commentators said, I'd like to point out that my object has a certain property (like greenness) which might be difficult to quantify but (say) readily understood. The property of greenness is not a set - all objects having it is. I would like to have shorthand for "A is/inherits Green" by something like $A\equiv G$. –  Praetoria Jun 23 '11 at 2:57

When I write papers in logic, I often use notation such as $$\phi \equiv (\exists x) \psi(x)$$ to define a formula $\phi$. I use $\equiv$ because the "=" symbol that might appear inside a formula, and so I want to use a different symbol to say that $\phi$ is defined as the formula $(\exists x)\psi(x)$. In this sort of definition, $\equiv$ does not mean"logically equivalent", it means the same thing that $:=$ does: the left side is defined to be the right side. I use $\leftrightarrow$ or $\Leftrightarrow$ for logical equivalence within a formula, so the $\equiv$ symbol could not appear there either. I don't use the $:=$ notation.

I am not the only person who uses this set of conventions, but at the same time they may be limited to the area of logic I write in. I would be very surprised to see an analysis book use $\equiv$ in this way.

-

I've also seen this a lot, and I came to the conclusion that “$\equiv$” was simply misused as a definition symbol.

The notation $A\equiv B$ states that—in a certain sense—$A$ is “as mighty (or large) as” $B$, while you really seem to mean something like $A\in B$, like “$A$ belongs to the (set of) round objects”. Perhaps you could have a notation like $A\in\{\mathrm{round}\}\cap\{\mathrm{green}\}$ or $A\in\bigcirc\cap\color{green}{\spadesuit}$.

-

I can answer to your question only in the formal approach. In Coq I use “Definition” to introduce a name for a new notion and “<->” (logical biconditional, logical equivalence) to say that some already defined notions are equivalent. When to use what is pretty intuitive there.

Definition implies equivalence, e.g.:

Definition incompatible (a b:Prop) := ~(a/\b).
Theorem incompatible0 : forall a b:Prop, incompatible a b <-> ~(a/\b).
Proof. firstorder. Qed.


As for your example about roundness, I do not see how to use logical biconditional here. I would rather denote roundness with an 1-ary predicate. E.g. “x is a circle” is formally written $\operatorname{circle}(x)$.

-