# Is there a proof of exportation/importation from more obviously true implications such as Modus ponens?

Is there a proof of exportation/importation, namely, ((p ∧ q) → r) ⇔ (p → (q → r)), from more obviously true implications such as the Modus ponens, Transposition, de Morgan etc.

I don’t believe that there is, but maybe I am wrong.

α → β here reads α implies β, defined as follows:

α → β if and only if the conditional “If α, then β” is true.

And I am not asking for the “proof” based on the material implication since it relies on the obviously false equivalence (α → β) ⇔ (¬α ∨ β). So, α → β here is not to be taken as equivalent to ¬α ∨ β.

• It is true by truth table. This is how we know what exportation is equivalent to. There is a way to derive it as well from a basic set of rules. Oct 5, 2022 at 13:32
• There's a Fitch or Gentzen proof tree way, or if you deem it's too mathy then just read out both sides using your if-then definition and then also treat left side as "if" and right side as "then" constituent recursively and vice versa, after a while it should make sense just using the conventional natural language semantic "if-then" and "and" rules... Oct 6, 2022 at 2:17

The question of whether the Import-Export principle can be derived from, or is even compatible with, varieties of logic with conditionals other than material implication has been quite a live topic in the logic of conditionals in recent years. So, this is an interesting question.

First, to make the symbols clearer, I'll use → for material implication and > for some as-yet-undetermined conditional that more closely reflects the meaning of 'if' in English. I'll use ↔ for the material biconditional. I will say that the > conditional collapses into material implication if it is possible to prove both that A > B entails A → B and also A → B entails A > B. The general version of Import-Export can then be stated as:

``````⊨ (A > (B > C)) ↔ ((A ∧ B) > C)
``````

The Import-Export principle, when used with some other simple logical principles causes any conditional to collapse into material implication. For example, Allan Gibbard showed that we get collapse if we accept Modus Ponens, Import-Export, and a principle called Left Logical Equivalence, which holds that A ↔ B entails (A > C) ↔ (B > C). Several logicians have proposed weaker logics in order to avoid this conclusion. Vann McGee has argued for exceptions to Modus Ponens; a bunch of logicians have argued against Left Logical Equivalence; and a bunch more have argued that Import-Export is not correct in the general case.

Mandelkern (2020) shows that if have Import-Export and a classical understanding of conjunction, then again we get collapse. In Mandelkern (2021) he shows that we also get collapse if we combine Import-Export with the Identity Principle, ⊨ A > A, a reductio type principle he calls Triviality: {A > B, A > ¬B} ⊨ ¬A and another he calls Very Weak Monotonicity. Mandelkern's conclusion is that Import-Export is not compatible with a non-material implication understanding of conditionals and so Import-Export should not be considered valid.

It should perhaps not surprise us that Import-Export does not work universally. If we substitute A for C, then (A ∧ B) > A is not equivalent to A > (B > A). The former is a logical truth, while the latter is doubtful in some cases. Also, Import-Export does not always hold for counterfactual conditionals. Consequently, Import-Export does not hold in accounts of conditionals such as the variably strict account of Stalnaker.

The upshot is that it is more difficult than one might suppose to avoid material implication. Classical logic is a coherent whole, and changing the conditional requires either a change in the rules of inference, including Import-Export, or a change in the meaning of the other connectives: and, or, not, which leads in the direction of a non-classical logic. This is not to say I am defending material implication. I'm not: it is an extremely crude approximation to the meaning of 'if'. But working around it is a lot of work, and might even require a distinctly different logic from classical.

Allan Gibbard, “Two Recent Theories of Conditionals”, in Harper, Stalnaker, and Pearce (eds.), IFS: Conditionals, Belief, Decision, Chance and Time, pp. 211–247 (1980).

Matthew Mandelkern, "Import-Export and 'And'", Philosophy and Phenomenological Research, 100, pp. 118-135 (2020).

Matthew Mandelkern, "If p, then p!", Journal of Philosophy 118, pp. 645-679 (2021).

• Thanks for a very good answer. This is very helpful. I am usually very critical of your answers but you are also often informative and here you indeed are. Thanks again. Oct 7, 2022 at 16:49

1.(P&Q)->R
Hyp for ->intro

2.P
Hyp for ->intro

3.Q
Hyp for ->intro

4.P&Q
2,3 &intro

5.R
1,4 ->elim

6.Q->R
3-5 ->intro

7.P->(Q->R)
2-6 ->intro

8.((P&Q)->R)->(P->(Q->R)) 1-7 ->intro

9.P->(Q->R)
Hyp for ->intro

10.P&Q
Hyp for ->intro

11.P
10 &elim

12.Q->R
9,11 ->elim

13.Q
10 &elim

14.R
12,13 ->elim

15.(P&Q)->R
10-14->intro

16.(P->(Q->R))->((P&Q)->R) 9-15->intro

17.(P->(Q->R))<->((P&Q)->R) 8,16<->intro