The equality symbol in logic

Question

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.

Answer 1

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