The symbol ⊃ (called "horseshoe") was used a century ago for the conditional connective "if-then", and subsequently replaced by → or ⇒.
The sources are Giuseppe Peano and A.N.Whitehead & Bertrand Russell's Principia Mathematica.
For the "devious" evolution of the symbolism, we can see :
[§674] A theory of the meccanisme du raisonnement was offered by Joseph Diaz Gergonne in an Essai de dialectique rationnelle (1816-1817); there the symbol H stands for complete logical disjunction, X for logical product, I for "identity," C for "contains," and "Ɔ (inverted C)" for "is contained in."
[§685] Ernst Schröder, [into his Vorlesungen über die Algebra der Logik, Vol. I (Leipzig, 1890), see page 129], used ⊂ for "is included in" (untergeordnet) and ⊃ for "includes" (ubergeordnet).
[§690] (page 301 of 2nd vol) Some additional symbols are introduced [by Peano into Number 2 of Volume II of his Formulaire]. Thus "ɔ" becomes ⊃. By the symbolism p.⊃ x ... z. q is expressed "from p one deduces, whatever x ... z may be, and q."
In his monograph: Calcolo geometrico (The geometrical calculus according to the Ausdehnungslehre of H.Grassmann, preceded by the operations of
deductive logic, 1888), Peano stress the duality of interpretations of his symbolism, in terms of classes and propositions :
we shall indicate [the universal affirmative proposition] by the expression
A < B, or B > A,
which can be read "every A is a B," or "the class B contains A." [...]
Hence, if a,b,... are conditional propositions, we have:
a < b, or b > a, says that "the class defined by the condition a is part of that defined by b," or [...] "b is a consequence of a,"
"if a is true, then b is true."
In Peano, The principles of arithmetic (Arithmetices principia: nova methodo exposita, 1899), we have:
II. Propositions [page viii]
The sign C means is a consequence of [est consequentia]; thus b C a is read b is a consequence of the proposition a.
The sign Ɔ means one deduces [deducitur]; thus a Ɔ b means the same as b C a. [...]
IV. Classes [page xi]
The sign Ɔ means is contained in. Thus a Ɔ b means class a is contained in class b.
a, b ∈ K Ɔ (a Ɔ b) :=: (x)(x ∈ a Ɔ x ∈ b).
Finally, in his Formulaire (1901, 1st edition: 1895), page 1, Peano writes:
Soient a et b des Cls. a ⊃ b signifie "tout a est b".
Soient p et q des propositions contenant une variable x; p ⊃x q, signifie "de p on déduit, quel que soit x, la q", c'est-à-dire:
"les x qui satisfont à la condition p satisferont aussi à la q".
Bertrand Russell, in his The Principles of Mathematics (1903) criticized this dualism:
§13 [ page 12 ] The subject of Symbolic Logic consists of three parts, the calculus of propositions, the calculus of classes and the calculus of relations. Between the first two, there is, within limits, a certain parallelism, which arises as follows: In any symbolic expression, the letters may be interpreted as classes or as propositions, and the relation of inclusion in the one case may be replaced by that of formal implication in the other. [...] A great deal has been made of this duality, and in the later editions of the Formulaire, Peano appears to have sacrificed logical precision to its preservation. But, as a matter of fact, there are many ways in which the calculus of propositions differs from that of classes.
Russell and Whitehead borrowed the basic logical symbolism from Peano, but they freed it from the "dual" interpretation.
Thus, they adopted Schröder's ⊂ for class inclusion [ page 27 ] :
a ⊂ b :=: (x)(x ∈ a Ɔ x ∈ b) Df.
and restricted the use of the "horseshoe" to the connective "if-then".
Note W&R's decision was obvious, if we consider the following example from Cesare Burali-Forti, Logica Matematica, 1894, page 70:
a Ɔ b . b Ɔ c : Ɔ : a Ɔ c [...]
The first, second and fourth [occurrences] of the sign Ɔ mean is contained, the third one means one deduces.
In conclusion, there is no specific "intuition" behind the adoption of certain symbols; we have only a "shift of meaning" from previous symbols to new ones.
