Exportation is a valid rule of replacement in propositional logic. The rule allows conditional statements having conjunctive antecedents to be replaced by statements having conditional consequents and vice-versa in logical proofs. It is the rule that:
The exportation rule may be written in sequent notation:
or in rule form:
where the rule is that wherever an instance of "" appears on a line of a proof, it can be replaced with "";
where , , and are propositions expressed in some logical system.
At any time, if P→Q is true, it can be replaced by P→(P∧Q).
One possible case for P→Q is for P to be true and Q to be true; thus P∧Q is also true, and P→(P∧Q) is true.
Another possible case sets P as false and Q as true. Thus, P∧Q is false and P→(P∧Q) is false; false→false is true.
The last case occurs when both P and Q are false. Thus, P∧Q is false and P→(P∧Q) is true.
It rains and the sun shines implies that there is a rainbow.
Thus, if it rains, then the sun shines implies that there is a rainbow.
Relation to functions
- Hurley, Patrick (1991). A Concise Introduction to Logic 4th edition. Wadsworth Publishing. pp. 364–5.
- Copi, Irving M.; Cohen, Carl (2005). Introduction to Logic. Prentice Hall. p. 371.
- Moore and Parker