What is the formal definition of an equation?

Solution 1:

Per the comments, let me say a bit about how one can - in $\mathsf{ZFC}$, for example - talk about (say) first-order sentences in a rigorous way. I'm not going to fill in all the details because ... whoo boy ... but I'll hopefully make the situation clear.

Our first step is to define the term non-logical symbol. Here's where the ugly happens:

• "$x$ is an $n$-ary function symbol" will be shorthand for "$x=\langle 0, n, a\rangle$ for some set $a$." (I'm thinking of constant symbols as nullary function symbols.)

• "$x$ is an $n$-ary relation symbol" will be shorthand for "$x=\langle 1,n,a\rangle$ for some set $a$."

• "$x$ is a non-logical symbol" will be shorthand for "for some $n\in\omega$, either $x$ is an $n$-ary function symbol or $x$ is an $n$-ary relation symbol."

We then brute-force carve out some logical symbols:

• "$x$ is the $=$ symbol" will be shorthand for "$x=\langle 2,0\rangle$."

• Etc. (the idea should be clear).

Finally we have the variables:

• Our variables will be sets of the form $\langle 3,a\rangle$ for some set $a$.

Terms, formulas, sentences, and proofs can now be represented by sets in a well-defined, if incredibly tedious, way. E.g. "Every formula has as many $($s as $)$s" can be made precise via the above approach and proved in $\mathsf{ZFC}$ or indeed much less. Similarly we can directly talk about structures: if $\Sigma$ is a set of non-logical symbols, a $\Sigma$-structure is a pair $(A,b)$ where $A$ is a (usually nonempty) set and $b$ is a function with domain $\Sigma$ satisfying [usual list of properties]. Defining $\models$ is a bit harder, but see this old answer of mine. Note that here we actually do have to "do some math," and (satisfyingly (pun intended)) what saves the day is the perhaps-at-first-glance-circular-and-certainly-crtiticizable-on-philosophical-grounds-if-nothing-else Tarskian definition of truth.

Putting all this together, we have a perfectly straightforward - if, again, incredibly annoying - way to implement our usual model-theoretic arguments in $\mathsf{ZFC}$.

Solution 2:

The term "equation" doesn't need a set-theoretic definition, because the "=" symbol is already part of the underlying first-order logic. We informally call a sentence an equation if it has the form $A=B$ or $\forall x (A(x)=B(x))$ or any of a variety of other forms that in spirit "state an equality". The axiom of extensionality specifies a relationship between $=$ and $\in$.