First use of exportation/importation in formal logic?

Question

Who is the logician who first used exportation/importation, namely, ((p ∧ q) → r) ⇔ (p → (q → r))?

Gödel used it in his 1939 Logic lecture, but it doesn’t seem to have been known from the Aristotelian tradition.

Answer 1

As Mauro Allegranza commented, Exportation is indeed in Cesare Burali-Forti’s Logica matematica (1894), on page 21:

9. ab Ͻ c : Ͻ : a . Ͻ . b Ͻ c

This translates as (a ∧ b) → c ⊢ a → (b → c), which is exportation.

Importation is on page 24:

9. a . Ͻ . b Ͻ c : Ͻ : ab Ͻ c

This translates as a → (b → c) ⊢ (a ∧ b) → c, which is importation.

Thanks to Mauro!

Answer 2

I wish to note some considerations upon the question departing from the material available to me.

The law of exportation is a methodologically significant theorem of propositional logic. So as to be a further explication, I have added into the Wikipedia article on exportation (logic) that in strict terminology, ((P∧Q)→R)⇒(P→(Q→R)) is the law of exportation, for it "exports" a proposition from the antecedent of (P∧Q)→R to its consequent. Its converse, the law of importation, (P→(Q→R))⇒((P∧Q)→R), "imports" a proposition from the consequent of (P→(Q→R)) to its antecedent.

We know by Jan Łukasiewicz's Aristotle's Syllogistic: From the Standpoint of Modern Formal Logic, this law fits seamlessly into the syllogistic theory. However, an explicit awareness of it and its recognition as a law of logic are quite different matters than that. The law of exportation demands also a conceptual made, for it can be viewed as a transition from categorical syllogism to hypothetical syllogism.

In her Dialectic and Its Place in the Development of Medieval Logic, Eleonore Stump gives a commentary on an 11th-century scholar, Garlandus Compotista (a.k.a. Garland the Computist). Garlandus argues for an inference which can be expressed as (p. 84)

[(a→b)∧(a→c)]→[(a→(b→c)]

It might seem a short step (see addendum) from the foregoing statement to the law of exportation. But in the chapter on Abelard, who was a next generation scholar after Garlandus, Stump discusses a case that Abelard's conception of hypothetical syllogism does not conform to the formal law of exportation where it should be, contrary to Abelard's own view of logic. As an illustration of the point, she considers a syllogism in Barbara (p. 105):

Every man is a stone and every stone is a donkey; therefore, every man is a donkey.

Put in hypothetical form

If every man is a stone, then if every stone is a donkey, every man is a donkey.

For the hypothetical statement to be true, according to Abelard, such a sequence of propositions, in essence, should be linked by their senses:

(a') every man is a stone,

(b') if every stone is a donkey, every man is a donkey,

(c') every stone is a donkey,

(d') every man is a donkey,

which is not the case, whereas the Barbara form and the hypothetical form must be equivalent by the law of exportation. Stump remarks (p. 106)

That he [Abelard] does take such a position suggests that he is moving away from the conception of logic as part of metaphysics (which seems to be Garlandus's conception) and toward an understanding of logic as formal by means of an intermediate step in which logical considerations are assimilated to considerations of meaning.

As for the present discussion, this is an indication of that Abelard had not taken that short step and it may have remained so for a long time afterwards.

---

Addendum

In the footnote 32, Stump gives some detail for Garlandus' argument:

In fact, what he says is that the third term must follow from the second by means of the first (147.12-13) and that the first term can never be without the second (148.3-4). His examples make it clear that by these criteria he means only (a→b)∧(a→c); certainly that is all he needs.

In this connection: It would be a fabulous contribution if someone uploaded L. M. de Rijk's Garlandus Compotista Dialectica: First Edition of the Manuscripts (Van Gorcum, 1959) to a free source platform like archive.org.