Formal definition of equation and unknowns I was just wondering about the formal definition of equation, I mean in terms of logic and the theory of sets. Suppose for example I wanted to define an equation on $\mathbb{R}$, of course it might be anything instead. I know every number is a set, and also I know that equality of sets has been defined previously. So I often hear people say something like "A linear equation is an object of the form $a_{1}x_{1}+a_{2}x_{2}+ \cdots + a_{n}x_{n}=b$".  But how do you justify the part of "$x_{i}$ is an unknown". Because in that case I would also say that $3(2)+4(5)=0 $ is an equation. 
 A: You won't find a formal definition of "equation" and "unknown", because they are partially informal concepts. The formula on the paper is what it is: two expressions, usually containing variables, joined by an equals sign. But there's no fixed rule that will tell you, from looking at the formula, which of the variables (if any) are unknowns.
Being an "unknown" is not a property of a variable or a formula. It expresses something about what you, the human mathematician looking at it intend to do with the equation. The roles of unknowns and constants can change simply by virtue of you changing your mind.
For example, if we're looking at the formula
$$ x^2+y^2=1 $$
we can choose to "solve for $x$", that is, treat the variable $x$ as an unknown and everything else as constants -- and we'd end up with $x=\pm\sqrt{1-y^2}$ -- or we could have made a different choice end with $y=\pm\sqrt{1-x^2}$ instead. Neither approach to the formula is objectively right or wrong. One of them may lead us closer to whatever our eventual goal is, but the formula itself doesn't know what that eventual goal is.
In particular when we say "treat $x$ as an unknown", there is no implied "... even though it really isn't". Nothing is an unknown in and of itself; variables are unknowns when and if we choose to treat them like one.
Also note that the formal rules of what one is allowed to do to a formula doesn't distinguish between knowns and unknowns. We can always replace $(p+q)^2$ with $p^2+q^2+pq+qp$, no matter whether $p$ and $q$ are knowns, unknowns, or some complex things built from several of each.
A: I would pick a set $x$ which is different from all the numbers we want to use, and regard it as an unknown in the formalism.
Then, for an $n\in\Bbb N$, $\ x_n:=\langle x,n\rangle$ (ordered pair).
Then, define terms as finite sequences, using these variables, perhaps the numbers, and the operation symbols (for these, a new, so far unused sets can be used).
Then, an equation would be an ordered pair $\langle\tau,\sigma\rangle$ of terms. Its meaning is defined then straightforwardly.
A: I would say that an equation is a logical predicate. That is, an open dictum whos truth value is determined by some input e.g.
$$P(x) \ : \ x + 2 = 4$$
where $x$ belongs to some domain. To solve an equation is to find the (possibly infinitely long) truth table for this predicate.
