Is there a rigorous definition of mathematical expressions that can distinguish them from their values?

Question

I asked a similar question before, but I did not get a satisfactory response, and people misunderstood the question. In mathematics books and classes, the author or teacher is not looking merely for the correct value, but also the correct expression. So, in a calculus class, if we are asked to compute the derivative of $x$, we would be marked wrong by the teacher if we simply wrote "the derivative of $x$ is the derivative of $x$", even though it is still a true statement. Or, in a set theory class, if we are asked to compute the Cartesian product $\{1,2\} \times \{2,3\}$, we would probably be again marked wrong if we simply wrote $\{1,2\} \times \{2,3\}$ as the answer. Or, even more basically, if we are asked to compute $2 \times 4$, we would be marked wrong in elementary school class by just writing $2 \times 4$. So, with those examples in mind, is there a rigorous definition somewhere, in some math or logic or computer science textbook, that defines what a mathematical expression is, such that different expressions like $2 \times 4$ versus $8$ are indeed technically distinct objects? It has to be broad enough to allow pretty much all mathematical expressions, such as "the derivative of $x$", $\{1,2\} \times \{2,3\}$, $2 \times 4$, $8$, etc.

Answer 1

Here is one possible answer to this question:

When working in a particular subject, we usually have syntax associated to the objects in question. For instance, if we're asking questions about $\mathbb{Z}$, we might allow ourselves symbols like $+$, $\times$, $\leq$, as well as numerals like $0$, $1$, $-5$, or $42$.

There are consistent rules for how we can fit these symbols together into terms (which name a certain number) and formulas (which name a truth value about numbers).

For instance, $14 \times 3$ is a term (it represents a number), and $14 \leq 3 \times 2$ is a formula (it represents a statment about numbers, which is either true or false). If we allow variables, then we can make more complicated terms (like $3 + x$) and more complicated formulas, like $\forall x . x \leq x+1$. This won't be relevant for this post, since we'll be focusing on terms, but it's good for cultural growth.

Now. It's clear that multiple terms can represent the same element of $\mathbb{Z}$. For instance, $14 \times 3$, $37 + 5$, and $42$. A reasonable question is whether there's a canonical term representing some element of $\mathbb{Z}$. For many systems there are rewrite rules that tell you how to convert one term into another. For instance, if we're intersted in calculus, we might be interested in terms built from $+$, $\times$, $x$, etc. as well as a special symbol called $\frac{d}{dx}$. Then a rewrite rule might be something of the form

$$ \frac{d}{dx} x^5 \leadsto 5 \times x^{4} $$

now one can prove that every expression involving $\frac{d}{dx}$ can be converted, via these rewrite rules, into an expression that does not contain $\frac{d}{dx}$. Allowing for other rewrite rules that allow us to group like powers, etc. we can prove a theorem saying there is a unique canonical term in each rewrite equivalence class. This is called a normal form, or, if you're a programming language theorist, a value. (NB: In general, normal forms need not be unique, though in many systems arising in practice this will be the case. Some people say canonical form when they want uniqueness, though the exact distinction between normal forms, canonical forms, and values has always been slightly murky to me).

When we do a computation, one can argue that we're "really" applying rewrite rules until no more rewrite rules apply. This actually gives us a purely syntactic way of interpreting the structure we're trying to study (which is called operational semantics for our syntax). For many "nice" systems, there are theorems that tell us we can always reduce to a value -- these theorems are often called "Progress and Preservation" in the PL theory literature. Through this lens, the difference between $4 \times 2$ and $8$ is that the latter is a value, while the former is not. But we can convert from the former to the latter by applying a rewrite rule.

If you're interested in learning more about this, you'll likely be interested in Bob Harper's Practical Foundations for Programming Languages (which is where I learned about a lot of this stuff). The first two chapters already have a good chance of answering many of your questions. I've also heard good things about Klop's Term Rewriting Systems, but I admit I haven't read it myself.

---

I hope this helps ^_^