# First use of exportation/importation in formal logic?

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.

• Of course they are present and proved into W&R's Principia Mathematica (1910): laws 3.3 and 3.31 (page 110) and called respectively Exp and Imp. Oct 5, 2022 at 10:49
• According to W&R, the names are due to Peano (see Peano (1897)) and we can found them (without name) into Cesare Burali-Forti, Logica matematica (1894). Oct 5, 2022 at 12:07
• What you are referring to is MATHEMATICAL LOGIC. Aristotelian logic predates Mathematical logic by a thousand years. Aristotelian logic did not use symbolization or mathematical concepts. The two logical systems are not identical nor equivalent. This is why it was not KNOWN prior to the invention of Mathematical logic in the 19th century. There was no such thing prior to that. You make it seem that all logic is logic. Oct 5, 2022 at 13:29
• @Logikal "What you are referring to is MATHEMATICAL LOGIC." I didn't refer to mathematical logic. I only referred to a logical equivalence. 2. "Aristotelian logic did not use symbolization" he did. See Prior Analytics. 3. "are not identical nor equivalent" I didn't say or imply that they were. 4. "This is why it was not KNOWN prior to the invention of Mathematical logic in the 19th century. There was no such thing prior to that." Substitute modus ponens, or modus tollens, or hypothetical syllogism, for exportation, to see that your assertion here is obviously false. Oct 5, 2022 at 15:35
• @Logikal The logic of 'and' 'or' 'not' and 'if' goes all the way back to the Stoic philosophers in the third century BC, about 100 years after Aristotle. It is not a 19th century invention. Though as far as we know, the stoics did not formulate the import/export rule. Oct 5, 2022 at 20:17

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

1. ab Ͻ c : Ͻ : a . Ͻ . b Ͻ c

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

Importation is on page 24:

1. a . Ͻ . b Ͻ c : Ͻ : ab Ͻ c

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

Thanks to Mauro!

• You are welcome :-) Oct 6, 2022 at 10:35
• Well what is the name of the subject matter to you if this is NOT mathematical logic? What is it called? Aristotelian logic did not use the 5 famous connectives: and, or, not, equivalent and if . . . Then at all in syllogisms. Why is this so hard for people to acknowledge? Oct 6, 2022 at 12:08
• @Logikal "name of the subject matter" Very easy, this: formal logic. You know, the thing started by Aristotle? 2. "Aristotelian logic did not use (...) and, (...) and if . . . Then" Aristotle's syllogisms had two premises, which Aristotle meant of course as both true, so this was a conjunction. A conjunction in all but name. And the logic of any syllogism is fundamentally a conditional. 3. "Why is this so hard for people to acknowledge?" Because it is not true. Oct 6, 2022 at 15:47
• You do recognize there are different types of logic. Aristotelian logic is one type which is distinct from Mathematical logic (with your logical connectives such as /\, \/, <->, ->, ~). Those are Mathematical logic whether you want to say so or not. There are multiple texts written with MATHEMATICAL LOGIC as the title you cannot deny those book titles exist. The formal name of the logic you keep saying is FORMAL is CALLED MATHEMATICAL LOGIC. The name is not FORMAL LOGIC. Can you give me an instance of a type of logic that is NOT formal in any way? All logic is formal ! I await a single counter Oct 6, 2022 at 16:20
• @Logikal "Can you give me an instance of a type of logic that is NOT formal?" Sure, logic itself. Formal logic systems are obviously formal but logic itself is not. This is a mental faculty or a property of brains. Oct 6, 2022 at 16:26

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.