History of the notation for substitution

Question

One of the very common notations for syntactic substitution is $[\ /\ ]$. However, there seems to be an inconsistency in the literature about its usage.

• Many write $[t/x]$ for "substitute $t$ for $x$" (Girard, Buss, ...).
• Others use $[x/t]$ for "replace $x$ with $t$" (van Dalen, Troelstra, Martin-Löf, ...).

I am wondering about the history of this notation. In particular, who was the first person to use this notation for syntactic substitution in logic?

Answer 1

Some early examples of the form $[t/x]$ are due to Haskell Curry.

See:

• Haskell Curry & Robert Feys & William Craig, Combinatory Logic. Volume I (1958), page 54:

Let $a$ and $b$ be obs and let $x$ be a variable; it is required to define the ob $b^*$ which is obtained by substitution of $a$ for $x$ in $b$. [...]

We shall adopt the notation

$$[a/x] b$$

for the $b^*$ so defined.

See also:

• Haskell Curry, Foundations of Mathematical Logic (1963), page 114:

In general, if there are no bound variables to restrict the substitution, we define the result of substituting an ob $M$ for $x$, symbolized as

$$[M/x]X$$

as that ob $X^*$ whose construction is obtained from a construction of $X$ by replacing subconstructions leading to $x$ by constructions of $M$.

---

For $[x/t]$, see :

• Alfred Tarski, A simplified formalization of predicate logic with identity, (1964) page 62:

Let $\varphi(\alpha/\beta)$ be the formula obtained from the formula $\varphi$ by proper substitution of the variable $\beta$ for the variable $\alpha$.

We may suppose that Tarski has "simplified" the notation used by Kurt Gödel in 1930, with

$$\text {Subst } a (^v_b)$$

and Alonzo Church in 1932 (and see: The calculi of lambda-conversion (1941)):

$$S^x_NM|.$$

A "variant" of Tarski's form is used by e.g. Enderton, with: $\alpha_t^x$.

Answer 2

You will not find any substitution notation in Frege, altough he does have a rule of substitution in his Grundgesetze-system (namely, rule 9 of its § 48). For an early example of substition notation in logic, see Russell's paper Mathematical Logic as based on the Theory of Types (1908). For instance, on its page 238 you can read:

If p is a proposition, and a a constituent of p, let "p/a;x" denote the proposition which results from substituting x for a wherever a occurs in p.

Gödel, as cited above by Mauro Allegranza, probably takes his notation from Von Neumann, who in his remarkable paper Zur Hilbertschen Beweistheorie (1927) writes

$$\mathrm{Subst}\bigl(\begin{smallmatrix} x_p \\ b \end{smallmatrix} \bigr)a$$

Von Neumann may in turn have taken this notation from his fellow countryman Julius König's book Neue Grundlagen der Logik, Arithmetik, und Mengenlehre (1904). König explains his substitution notation,

$$\mathrm{S}\bigl(\begin{smallmatrix} x \\ V \end{smallmatrix} \bigr)F$$

on pages 92ff.

The source of König's notation may be the notation exemplified by

$$\begin{pmatrix} 1&2&3&4 \\ 2&4&1&3 \end{pmatrix} $$

for what are nowadays usually called permutations, but which Cauchy, who introduced this notation in a paper from 1815, called, precisely, substitutions.

Substitution notation is of course also used in the calculus. Thus, Cauchy in his Cours d'Analyse (1821) suggests

$$\int f(x)\,dx\,\bigl[\begin{smallmatrix} x=x_0 \\ x=X \end{smallmatrix} \bigr]$$

as one possible notation for the integral. (The now standard notation $\int_{x_0}^Xf(x)\,dx$ was introduced by Fourier.) The relevant extracts from Cauchy's texts can be found, in the original and translated, in Jacqueline Stedall's source book Mathematics Emerging.

I should note that I have learned most of the information reported here from Per Martin-Löf (the reference to König is due to Göran Sundholm).

Answer 3

(To the title question, and @AnstenKlev’s answer:)

Sarrus (1848) introduced maybe the earliest signe de substitution : $\style{font-family:sans-serif;font-style:italic}1\,^t_x$.