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$"?

Solution 1:

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.

Solution 2:

Do you want to know how to write "let" exactly or basically write "the same" content as how we usually interpret "let"?

I don't know your particular proof, but you might achieve the same effect by considering conditionals. In other words, "let x equal a" turns into a conditional "if x equals a, then ...", at least in a system which has the material conditional at work. You could write ((x=a)->...) or with (x=a) as a proposition p, (p->...). If you don't have the material condtiional, I'd guess you'd want to use one of its respective equivalents... such as in a deductive system with only disjunction and negation, instead of saying "if a, then b" you would have "either not a or b".