Equations vs Expressions

Factual Questions
1

I’ve been thinking about this, and I’m pretty sure I’ve stumbled into areas of math beyond my training. The “standard” answer of course, is that “=” denotes an equation

x + 2 = 3 <-- Equation
x + 2 <-- Expression

However, it seems to me that “equation” is a special class of expressions, sort of like how the set of primes is a special class of integers. The driving example in this for me is Iverson brackets. As most people qualified to answer this question probably know, the Iverson bracket notation is an expression/function used a lot in probability (e.g. in the categorical distribution) and computer science. Probably in other fields too but that’s what I’m familiar with. Its meaning is

I[ condition ] ={1 if condition is true; 0 otherwise}. Roughly I’d call it a function such that

I: {T,F} -> {1,0}; or a function with the domain in the boolean variables True,False that maps them to the numbers in Z/R/C/<insert superset here> 1 or 0. Frequently this is used with equality, e.g. I[ f(x) = g(y) ].

In this case, while f(x) = g(y) is an equation, it’s also being used as an expression. So

x in S1
f: S1 -> D

y in S2
g: S2 -> D

= : (D x D) -> {T,F}

Where S1,S2 are arbitrary domains and D is a shared arbitrary codomain of f and g.

So the expression above would be (pardon the slightly wonky notation)

I’: ((S1 -> D) x (S2 -> D)) -> {T,F} -> {1,0}

This seems to suggest that an equation is an expression, as noted by its use as a subexpression.

One possible counterargument is that this is just an overloading of the “=” notation. While normally “=” denotes an “equation”, in this case we’re really using the function “Eq” that happens to have a shorthand that looks like “=”. Just like pi can be used for a constant or as the standard letter for a policy function.

Perhaps a counterargument to that is its implicit use as a function in proofs by contradiction. When we say “assume x=y”, we’re saying, “assume Eq(x,y) evaluates to True”, the contradiction arises where that doesn’t hold. But then we’re just moving the goalposts, that’s just saying “assume Eq(x,y) = T” and you’re back where you started with the equation/expression dynamic.

I don’t know, clearly I’m overthinking this, I’m just wondering if “equation” is just a linguistic anomaly or extremely well defined. Clearly both “Eq” and “=” are pieces of notation that do something sensitive to equivalence relations between their subexpressions, but it seems whether they’re the same or different should be something basic enough to be well defined.

2

This is the correct answer. We use = both to denote the equality of two expressions, and in other contexts as an assignment operator. It’s exactly the difference between := and == in some programming languages.

3

I have seen some contexts where an equation is considered a kind of expression. Ultimately, though, it’s just a matter of terminology, and doesn’t say anything fundamental whether they are or not.

4

In a wider sense, an equation is a specific sort of expression. Once you have the tools the whole thing can be manipulated in useful ways. Including all the usual manipulations on the equations.

Another use of = is in denoting binding. Both with the notion of bound and unbound variables in expressions, which changes the way the manipulation rules can be applied, and in computer languages, where binding of variables is an important notion, albeit one mostly ignored in mainstream coding (until it bites someone).

5

I think a useful distinction is that an expression resolves to a number, while an equation doest not. (Unless you start doing funny things like assigning 1 to “true” and 0 to “false” and then attaching meaning to the arithmetic you might do with those values).

However it is certainly possible to define expressions of the atoms “true” and “false” combined with logical operators. Perhaps that is the resolution to your difficulty. There are then three types of objects:

(1) Mathematical expressions, which always resolve to a number.

(2) Mathematical equations, which state that two math expressions are equal to one another, and which can be defined to resolve to a boolean value of “true” or “false.”

(3) Logical expressions, which are constructed of boolean values some of which may be represented by mathematical equations, connected by logical operators, some of which may be represented by math operators.

Put that way, there is a clear heirarchy: logical expressions may contain math equations, but a math expression cannot contain a math equation. The confusion arises because we can say “expression” without clarifying whether it’s a logical or mathematical expression.

6

Equality is intimately tied up with your chosen foundation and the answer to the OP’s question is “it depends”.

In HOL there is no distinction between the equality used to assert that 3 = x + 0 and f(x) = x. The “=” constant is the same, a polymorphic equality constant in bool. Function definitions are just equalities between a left hand side and a right hand side like any other boolean term and any equality can be used in any context where one would normally use a boolean expression (e.g. in an if-then-else or other case splitting form, in a conjunction or implication, in the body of a universal quantification, and so on).

In ITT, there is a distinction between the equalities 3 ≡ x + 0 and f(x) = x, with the former being a propositional equality and the latter function definition being a definitional equality. For the latter, for all x, f(x) and x become indistinguishable to the typing judgement (i.e. they are convertible terms, and the typing judgement includes a rule that takes this convertibility into account) — that is, the latter has an effect on the global context whilst the former is just a term (and can be a subterm) like any other.

7

Note that in many computer languages, an assignment statement returns the value assigned. So, for example, “bar = 3” returns “3”, so then “foo = bar = 3” means that foo gets assigned 3 as well. Normal “equations” like “foo == bar” return true/false (or their equivalents).

In the language definitions they are all considered expressions. To many programmers, there is no reason to make a distinction.