8
$\begingroup$

Some people use $\stackrel{\mathrm{def}}{=}$, $:=$ or $\stackrel{\Delta}{=}$ for definitions. In more informal contexts, I have also seen $\stackrel{?}{=}$, for "I wish to prove this equality, which implies the thesis", used when working backwards, or even the less common $\stackrel{!}{=}$ (for which it is difficult to infer a precise meaning, but it's something like "we are imposing this equality", or "this is an Ansatz").

It seems like the use of these symbols is not common in papers (apart from maybe the first ones for definitions); however, they seem useful to me as a way to convey more meaning than the usual equality symbols. For instance, in some sense the "?" superscript changes the set of "allowed operations": from $a=c$ and $b=d$ it follows that $a+b=c+d$, but the same implications wouldn't hold with $\stackrel{?}{=}$ signs.

Q1: has the use of these symbols ever been properly formalized?

Q2: are there contexts in which they are used in papers? Are they standard in your field? Are they used in lectures/seminars/papers?

Improve this question
$\endgroup$
11
  • 2
    $\begingroup$ Related: mathoverflow.net/questions/11077/what-does-above-mean $\endgroup$
    – Waldemar
    Commented Nov 6, 2013 at 11:04
  • 2
    $\begingroup$ You write "from $a = c$ and $b = d$ it follows that $a+c = b+d$". That's not true. $\endgroup$
    – KConrad
    Commented Nov 6, 2013 at 12:59
  • 4
    $\begingroup$ Some people use $\equiv$ for definitions (as opposed to congruence); see en.wikipedia.org/wiki/List_of_mathematical_symbols $\endgroup$
    – user25199
    Commented Nov 6, 2013 at 14:02
  • 4
    $\begingroup$ The use of $:=$ seems quite standard, and has the advantage over some of the others of not breaking the line. $\endgroup$
    – Sam Hopkins
    Commented Nov 6, 2013 at 15:06
  • 2
    $\begingroup$ @Waldemar I very much like the first example you give but not the second. The first one is questioning are they equal, which is fine by me. In the second however... when we solve say $x^2+x=0$ we are not questioning which values of $x$ solve the equation. Instead we should begin by assuming $x$ is a solution so that $x^2+x=0$ and deducing $x=0$ or $-1$. I agree with non-standard but I could say worse. $\endgroup$
    – JP McCarthy
    Commented Nov 8, 2013 at 0:21

2 Answers 2

Reset to default
13
$\begingroup$

One context in which the distinction between "equal by definition" and "equal because we proved it" has a precise mathematical meaning is intensional dependent type theory. This includes formalizing mathematics in a computer proof assistant based on ITT, such as Coq or Agda, but mathematics in ITT can also be done "unformalized" such as in the homotopy type theory book.

As for notation:

  • Coq uses $=$ for propositional equality (i.e. "we proved it" equality) and $:=$ for definitional equality (more precisely, for definitions currently being made).

  • Agda uses $=$ for definitions being made, and (at least in the standard library) $\equiv$ for propositional equality.

  • The HoTT book uses $=$ for propositional equality, $\equiv$ for an equality that holds by definition but is not something currently being defined, and $:\equiv$ for something currently being defined.

    We spent a long time deciding on this; we wanted to use $=$ for "ordinary" equality, and we wanted to use something symmetric like $\equiv$ for equalities-by-previous-definition and something asymmetric like $:=$ for current-definitions so as to indicate visually that the left side is what's being defined. But $:=$ for a current-definition would suggest that it's a propositional equality that results rather than a definitional one, which led us to invent the symbol $:\equiv$. (We then actually ended up using $:=$ later for a "propositional equality being currently defined to hold", which happens under some versions of higher inductive types.)

Improve this answer
$\endgroup$
6
$\begingroup$

In a slightly different direction, $\overset{\mbox{(2.3)}}{\ge}$ (the overset should be in a smaller font using \tiny, but for some reason that wouldn't render here) is a nice way to indicate that the inequality uses $(2.3)$ - this is especially convenient with a long string of inequalities in display-math where it's otherwise hard work to figure out which inequality uses which previous calculation.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .