[Math] 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$.