12
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ In case you are not only interested in precisely this notation, let me mention that Bourbaki introduces $(B|x)A$ in a draft of E.I, dating from 1951 (état 6, page 3) and keeps it since then. The preceding version uses the $(Sub$ $x|B)A$ (état 5, page 2). $\endgroup$ – Fred Rohrer Jun 26 '16 at 11:21
  • 2
    $\begingroup$ @Fred, yes, I am aware of other notions, including $[x := t]$ and $[x \mapsto t]$. I am more interested in figuring out that how this particular notation was originally used. I have searched a bit to see if Russel and Whitehead or Hilbert or Frege have used it but I haven't find any evidence so far. $\endgroup$ – Kaveh Jun 26 '16 at 11:38
  • 2
    $\begingroup$ A similar notation is for valuations, used in defining the satisfaction relation. In this case, Vaught and other Berkeley logicians (presumably also Tarski) used $M\models\varphi[{x\atop a}]$, where $x$ is a variable symbol and $a$ is an object in $M$. $\endgroup$ – Joel David Hamkins Jun 26 '16 at 13:21
  • 1
    $\begingroup$ When I was taught, we used $\int_t^x\varphi$ to denote this substitution. What @Joel describes was used to describe assignments of values. $\endgroup$ – Asaf Karagila Jun 27 '16 at 13:33
  • $\begingroup$ It seem a more common and older notation for dealing with substitution is the function notations: first indicate the formula with its variables like $\varphi(x)$ and then the result of substituting $t$ for $x$ is represented as $\varphi(t)$ without a symbol for the substitution operation. $\endgroup$ – Kaveh Jun 28 '16 at 16:19
16
$\begingroup$

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

See:

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:

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 :

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

$\endgroup$
8
$\begingroup$

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

$\endgroup$
4
$\begingroup$

(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$.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.