# The equality symbol in logic

I am writing about first order logic and have confused myself regarding the $=$ symbol. This is what I have written:

As an example, we define the standard model of arithmetic, $\mathfrak N$. Our domain here is $N=\{0,1,2,\ldots\}$. Interpret the constant symbol $0$ as $0\in N$; say that $<^\mathfrak{N}$ is the set of $(n,m)\in N^2$ such that $n<m$ in $N$; and define the functions as $\prime^\mathfrak{ N}(n)=n+1$ (read the 'successor of $n$', and write $n^\prime$), $n+^\mathfrak{ N}m=n+m$, and $n\cdot^\mathfrak{ N}m=n\cdot m$.

Is the equality symbol used in the final sentence a different equality symbol to the one used in formal logical sentences (for example $t_1=t_2$ for terms $t_1,t_2$)? If so, is it worth distinguishing between the two symbols? I do remember hearing there are different equalities floating around in this context, and that (formally) one should distinguish: I cannot find any reading on this, though.

• Well if you have to terms $t_1, t_2$, the formula $t_1 = t_2$ does not "mean" anything, in particular it doesn't mean that $t_1$ and $t_2$ are the same, whereas the last equality in the quoted text is a "real" equality, i.e. those two objects are literally the same (by definition). So one is a symbol, and the other one denotes an actual thing. That's why a book on logic I had used $\simeq$ for formulas, you would write e.g. $t_1 \simeq t_2$ for terms $t_1, t_2$, to write a formula Mar 14, 2017 at 20:22
• @Max I like that notation, thanks Mar 14, 2017 at 20:27

Yes, there are two different equals signs here. There's equality at the meta-level (where we're talking about structures, interpretations, formulas and so forth), and the equality symbol that can appear in a formula.

Unfortunately it is common not to distinguish visually between the two kinds of equals signs and instead let the reader figure out from the context which of them makes sense.

In your particular quote it looks to me like all of the equals sign are at the metalevel.

I would say it is probably not worth trying to distinguish typographically. The meta-level equals sign should be an ordinary equals sign -- for example saying "$N=\{0,1,2,\ldots\}$" is an ordinary equality at the metalevel, and it seems to make little sense to insist that this equals sign cannot be written as we usually do when we're creating a mathematical model of something-or-other.

It could make some sense to use a special equals sign to denote textual equality between terms (which is where there is a danger of confusion), as @Max suggests -- or perhaps generally for things defined as symbol strings.

Personally I would find it more principled to use a special equals sign inside formulas, such as $\mathtt{=}$ -- that is, \mathtt{=} -- but that may be because I come from a computer science tradition where we often use typewriter font for pieces of object language and ordinary mathematical symbols for reasoning about them.

(An alternative would be to stringently use quotes each time you write down object formulas, but that just ends up being horrible).