# 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.

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".

• 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. Jan 27, 2012 at 14:46

Well, this an easy one! You, simply, do NOT write "let" in (symbolic) logic, as you do it in the vernacular (in your mother-tongue, for instance)!

Now, the so called "mathematical vernacular" [WOT, in Dutch] has been explained (and codified) long ago, by one of my Dutch math teachers, N. G. [ = Dick ] de Bruijn, of the Eindhoven Polytechnics [TUE], The Netherlands, in lectures (on "[De] Taal en Structuur van de Wiskunde" [= The language and structure of mathematics]), sometime during the late seventies, to be precise. (Cf., e.g., Euclides 55, 1979-1980.) --

There is even a nice book (in Dutch) on this, authored by one of his former PhD students and collaborators, Rob Nederpelt (Eindhoven) :

“De taal van de wiskunde, Een verkenning van wiskundig taalgebruik en logische redeneerpatronen” [The language of mathematics, An exploration of the mathematical use of language and the logical proof-patterns] (With an introduction by Dirk van Dalen), Versluis, Almere 1987.

Unfortunately, Rob's book has not been translated so far. But see his recent Cambridge-UP-monograph, co-authored with Herman Geuvers [Radboud Univ., Nijmegen], on "Automath" and the like: "Type Theory and Formal Proof. An Introduction", Cambridge University Press, Cambridge, 2014 [ISBN 978-1-107-03650-5, xxviii + 436 pages] etc.

Essentially, an Automath "language" / system (of proof checking mathematical texts) amounts to a very formal way of writing down a WOT- / "mathematical vernacular"-text, such as to be readable by a machine, a computer, say.

In Automath (and the like), the informal "let" goes either into

(1) a [meta] variable-declaration

or else into

(2) an explicit definition,

pointing out to two distinct -- rather tricky -- ways of manipulating textual substitutions in actual mathematics. (There is third way of doing "substitutions" in logic / mathematics, by applying the so-called CUT-rule of Gerhard Gentzen [1935]; this is just a way of codifying the usual practice of "proving by lemmas" in Euclid & so on.)

For the rest -- if (still) Dutchless and unable to read Rob's WOT-book of 1987 --, I'd suggest buying the recent monograph mentioned above: it is aimed at undergraduates and, as a bonus, it covers a lot of technical stuff you won't easily find elsewhere in print...