"Defined as" versus "Equivalent to"

Question

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.

Answer 1

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}$.

Answer 2

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.

Answer 3

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)$.