The syntax of an equational logic is very simple. The basic kind of formulae you write is of the form:
where 
and 
are quantifier-free expressions, usually typed.
and may or may not have variables in them.
It's important that and are quantifier-free because
any variables that do appear in and are implicitly universally
quantified.
You can think of the = (equal) symbol as just a very special
predicate symbol in a predicate logic. We very well could
have introduced a word for this predicate, e.g., equal,
and have written 
instead of the equation above.
Here, we are appealing to your intuition by using the symbol = and
treating it as a binary infix operator rather than a prefix operator.
In a typed logic, the expressions on the right and left hand sides of = have to be of the same type for the whole expression to make sense. You can write
since for both equations the right and left hand sides both evaluate to integers but writing
is utter nonsense.
In a typed logic, we usually assume that for each type there is
a special = symbol but we don't usually introduce different
notation for each. In other words, I don't write 
and 
to distinguish between equality for integers and equality for colors.
There is often one important exception, and that is for boolean
expressions.
You will see that many people use the 
symbol (pronounced ``is equivalent
to'')
to denote equality
between boolean expressions.
So you can write things like
