Who first discovered the concept corresponding to the symbol of class comprehension?

Question

Who first discovered the concept corresponding to the symbol of class comprehension $\{x/\varphi\}$ used today in set theory ?

Answer 1

The concept is found with different notation in Peano (1894, p. 20) (translated):

Let $p_x$ be a proposition containing a variable letter $x$, that is, a condition on $x$. By the notation $\overline{x\ \varepsilon}\,p_x$ we shall indicate the class of those $x$ that satisfy the condition $p_x$.

Von Neumann (1923, Einleitung) uses $M$ for Menge:

Let $E(x)$ be a property, $f(x)$ a function defined for all $x$ possessing the property $E(x)$. Then $$ M(f(x); E(x)) $$ shall be the set of all $f(x)$ as $x$ runs over all $x$ possessing the property $E(x)$.

Our notation $\{\ ..\mid\,...\}$ is in e.g. Lefschetz (1942, p. 2; 1949, p. 26; ...), Iwasawa (1945; 1949; ...), Segal (1946; 1947; ...), Kelley (1947; 1953; 1955), Mostow (1949; 1950; ...), Yamabe (1950), Nomizu (1950; 1954; ...), Godement (1952; ...), Loomis (1953; ...), etc. Kelley (1947, p. 683) seems to attribute it to Lefschetz; Bernays (1958, § I.1) writes:

Our logical symbols are (...)

3) The class operator $\{\mathfrak r\mid\mathfrak{A(r)}\}$¹⁾  « the class of the $\mathfrak r$ such that $\mathfrak{A(r)}$ »

(...)

The rules concerning the class terms are: the formula schema (“Church schema”) $$ c\in\{\mathfrak r\mid\mathfrak{A(r)}\}\ \leftrightarrow\ \mathfrak A(c), $$ expressing a conversion law, in the sense of A. Church (1932), and (...)

---

^{1) This symbol (used in some newer papers) is here taken, for the sake of easier print, instead of Russell’s class symbol $\hat{\mathfrak r}\mathfrak{A(r)}$, whose adoption was first intended.}

---

Added: Bernays’ name class operator for $\{\ ..\mid\,...\}$ came after Kelley’s classifier (1955, p. 251); set-builder seems to originate earlier in collective program books like Universal Mathematics (1955, p. I-9), Concepts and Structure of Mathematics (1954, p. 117) and Fundamental Mathematics (1948, p. 24) — the latter however using the different notation $\underset{\textstyle{..}}{\mathrm S}\,...$

Answer 2

Following G.Cantor ( see "Beiträge zur Begründung der transfiniten Mengenlehre" [Contributions to the founding of the theory of transfinite numbers], Mathematische Annalen (1895) ),the use of braces for sets was already present in E.Zermelo, “Untersuchungen über die Grundlagen der Mengenlehre,” Mathematische Annalen (1908) :

The set that contains only the elements $a, b, c, \ldots, r$ will often be denoted briefly by $\{ a, b, c, \ldots, r\}$.

The modern symbol for sets defined "via comprehension" evolved from Whitehead & Russell's Principia Mathematica (910-1913) :

$\hat x (\phi x)$,

meaning : the class of individuals satisfying the propositional function $\phi x$.

As referred in the answer above, Paul Bernays, in Axiomatic Set Theory (1958) says (page 46) :

The class operator $\{ \mathfrak x \mid \mathfrak A (\mathfrak x) \}$ «the class of the $\mathfrak x$ such that $\mathfrak A (\mathfrak x)$» [footnote : This symbol (used in some newer papers) is here taken, for the sake of easier print, instead of Russell's class symbol $\hat {\mathfrak x} \ \mathfrak A (\mathfrak x)$, whose adoption was first intended.]

The symbol were not used by Bernays in his previous work published in the Journ. of Symb. Log. (1937-1954).

---

Note : W&R's $\hat x$-notation for class-abstraction was also the source for Church's $\lambda$-notation.

See Alonzo Church,A Set of Postulates for the Foundation of Logic (1932) :

If $\text M$ is any formula containing the variable $x$, then $\lambda x [ \text M ]$ is the symbol for the function whose values are those given by the formula.

See Felice Cardone & J.Roger Hindley, History of lambda-calculus and combinatory logic (2006) :

By the way, why did Church choose the notation “$\lambda$”? In Church (1964) [unpublished letter] he stated clearly that it came from the notation “$\hat x$” used for class-abstraction by Whitehead and Russell, by first modifying “$\hat x$” to “$\land x$” to distinguish function abstraction from class-abstraction, and then changing “$\land$” to “$\lambda$” for ease of printing.

See also : J.B. Rosser, Highlights of the history of the lambda calculus, Annals of the History of Computing (1984), page 338.

---

---

IMO, the symbol slowly emerged during the 1950s.

Lefschez's Algebraic Topology (1942) has it (page 2) :

If $P$ is a property, the totality of all the elements $x$ which satisfy $P$ is denoted by $\{ x \mid x \text { has the property } P \}$.

Well-know set-theorists like A.Fraenkel do not used it; see Abraham Fraenkel, Abstract Set Theory (1953) and Abraham Fraenkel & Yehoshua Bar-Hillel, Foundations of Set Theory (1958).

But P.Suppes in Axiomatic set theory (1960) says (page 33) :

In many branches of modern mathematics it is customary to use the notation:

$\{ x : \varphi(x) \}$

to designate the set of all objects having the property $\varphi$.

Bourbaki's Theory of sets (1968) has

$\mathcal E_x(R)$ [for the term denoting] "the set of all $x$ such that $R$".

The 1970 second French edition has instead :

le symbole $\{x \mid R \}$ [par] «l'ensemble des $x$ tels que $R$».