# How to write “let” in symbolic logic

How do I write let in symbolic logic? For example, if I am in the middle of a proof and there is a variable which I can assign to an arbitrary value, what would I write? My best guess is:

$$x := a$$

Would that be clear? Is there a better way to write "let $x$ equal $a$"?

-

There is no symbol in first-order logic that corresponds to "let", and formal proofs in first-order logic do not have a means to assign a value to a variable.

The phenomenon of setting a variable equal to a value is limited to natural-language proofs, in which it hard to improve on "Let $x$ equal $a$".

Of course these natural-language proofs can be formalized, and each formal deductive system has some way to deal with this type of reasoning, but none of the usual ones does so by literally allowing values to be assigned to variables.

-
Of course you can only write $x=a$ in a proof if $a$ is a term. So if we worked with e.g. the real numbers in the signature of fields, we would not be able to plug in most values in this way. –  Carl Mummert Jan 27 '12 at 14:46